First-entry replacement and the normalized eight-gate interface

The actual gate rewiring is captured at the semantic wire-space level: when a new target direction first enters a one-vector extension, it can replace that vector without changing the state. This is exactly what later gates see in the semantic circuit model.

theorem UnrestrictedBooleanMul.N4.span_first_entry_replacement {m : ℕ} (V : Submodule F₂ (ANF m)) (g t : ANF m) (ht : t ∈ V ⊔ F₂ ∙ g) (htV : t ∉ V) : V ⊔ F₂ ∙ g = V ⊔ F₂ ∙ t

Basis replacement in a one-vector extension over F₂.

theorem UnrestrictedBooleanMul.N4.circuit_first_entry_replacement {m r : ℕ} (C : Circuit m r) (j : Fin r) (t : ANF m) (ht : t ∈ circuitFlag C (↑j + 1)) (htFirst : t ∉ circuitFlag C ↑j) : circuitFlag C (↑j + 1) = circuitFlag C ↑j ⊔ F₂ ∙ t

Circuit form of first-entry replacement.

noncomputable def UnrestrictedBooleanMul.N4.rZeroANF : ANF 8

The product target corresponding to evaluation at zero.

Equations

• UnrestrictedBooleanMul.N4.rZeroANF = UnrestrictedBooleanMul.N4.targetANF UnrestrictedBooleanMul.N4.rZeroCoeff

noncomputable def UnrestrictedBooleanMul.N4.rOneANF : ANF 8

The product target corresponding to evaluation at one.

Equations

• UnrestrictedBooleanMul.N4.rOneANF = UnrestrictedBooleanMul.N4.targetANF UnrestrictedBooleanMul.N4.rOneCoeff

noncomputable def UnrestrictedBooleanMul.N4.rInfinityANF : ANF 8

The product target corresponding to the leading coefficient.

Equations

• UnrestrictedBooleanMul.N4.rInfinityANF = UnrestrictedBooleanMul.N4.targetANF UnrestrictedBooleanMul.N4.rInfinityCoeff

noncomputable def UnrestrictedBooleanMul.N4.rationalTargetSpace : Submodule F₂ (ANF 8)

The span of the product evaluations at zero, one, and infinity.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def UnrestrictedBooleanMul.N4.rationalLowSpace : Submodule F₂ (ANF 8)

Affine functions together with the rational-place product targets.

Equations

• UnrestrictedBooleanMul.N4.rationalLowSpace = UnrestrictedBooleanMul.affine 8 ⊔ UnrestrictedBooleanMul.N4.rationalTargetSpace

theorem UnrestrictedBooleanMul.N4.targetANF_rationalCoeffRep (α : Fin 3 → F₂) : targetANF (rationalCoeffRep α) = α 0 • rZeroANF + α 1 • rOneANF + α 2 • rInfinityANF

theorem UnrestrictedBooleanMul.N4.mem_rationalTargetSpace_iff (p : ANF 8) : p ∈ rationalTargetSpace ↔ ∃ (α : Fin 3 → F₂), p = targetANF (rationalCoeffRep α)

structure UnrestrictedBooleanMul.N4.NormalizedEight (C : Circuit 8 8) : Prop

The state constructed by the eight-gate normalization theorem, recording the rational prefix, seed defect, and useful suffix for the contradiction.

• computes : C.Computes (Mul 4)
• gate_zero : C.gate 0 = rZeroANF
• gate_one : C.gate 1 = rOneANF
• gate_infinity : C.gate 2 = rInfinityANF
• seed_nonUseful : ¬UsefulAt C (mulTarget 4) 3
• suffix_useful (j : Fin 8) : 4 ≤ ↑j → UsefulAt C (mulTarget 4) j
• defect_one : flagDefectRank C.finalWire (mulTarget 4) = 1

theorem UnrestrictedBooleanMul.N4.NormalizedEight.prefixGates_three {C : Circuit 8 8} (h : NormalizedEight C) : prefixGates C.gate 3 = {rZeroANF, rOneANF, rInfinityANF}

theorem UnrestrictedBooleanMul.N4.NormalizedEight.wireSpace_seed_eq {C : Circuit 8 8} (h : NormalizedEight C) : wireSpace C.gate 3 = rationalLowSpace

theorem UnrestrictedBooleanMul.N4.NormalizedEight.seed_left_mem_rationalLow {C : Circuit 8 8} (h : NormalizedEight C) : C.left 3 ∈ rationalLowSpace

theorem UnrestrictedBooleanMul.N4.NormalizedEight.seed_right_mem_rationalLow {C : Circuit 8 8} (h : NormalizedEight C) : C.right 3 ∈ rationalLowSpace

def UnrestrictedBooleanMul.N4.SeedFactorData (C : Circuit 8 8) : Prop

Algebraic factor data exposed by the normalized seed.

Equations

• One or more equations did not get rendered due to their size.

theorem UnrestrictedBooleanMul.N4.NormalizedEight.seedFactorData {C : Circuit 8 8} (h : NormalizedEight C) : SeedFactorData C

theorem UnrestrictedBooleanMul.N4.NormalizedEight.gateFive_useful {C : Circuit 8 8} (h : NormalizedEight C) : UsefulAt C (mulTarget 4) 4

theorem UnrestrictedBooleanMul.N4.NormalizedEight.gateSix_useful {C : Circuit 8 8} (h : NormalizedEight C) : UsefulAt C (mulTarget 4) 5