Construction of the rational three-gate prefix

The normalization is performed by algebraic basis replacement and legal gate commutation. No circuits are enumerated. The only finite calculation below is the three-coordinate proof that the rational place words are independent.

theorem UnrestrictedBooleanMul.N4.rationalPlaceCoeff_linearIndependent : LinearIndependent F₂ rationalPlaceCoeff

theorem UnrestrictedBooleanMul.N4.targetANF_not_mem_affine_sup_span {c : TargetCoeff} {S : Set TargetCoeff} (hc : c ∉ Submodule.span F₂ S) : targetANF c ∉ affine 8 ⊔ Submodule.span F₂ (targetANF '' S)

A target coefficient outside a coefficient span remains outside after the span is embedded as target ANFs and affine functions are adjoined.

theorem UnrestrictedBooleanMul.N4.rOneANF_not_mem_affine_rZero : rOneANF ∉ affine 8 ⊔ F₂ ∙ rZeroANF

theorem UnrestrictedBooleanMul.N4.rInfinityANF_not_mem_affine_rZero_rOne : rInfinityANF ∉ affine 8 ⊔ Submodule.span F₂ {rZeroANF, rOneANF}

theorem UnrestrictedBooleanMul.N4.wireSpace_one_eq_of_gate_zero {C : Circuit 8 8} (hzero : C.gate 0 = rZeroANF) : wireSpace C.gate 1 = affine 8 ⊔ F₂ ∙ rZeroANF

theorem UnrestrictedBooleanMul.N4.wireSpace_two_eq_of_gate_zero_one {C : Circuit 8 8} (hzero : C.gate 0 = rZeroANF) (hone : C.gate 1 = rOneANF) : wireSpace C.gate 2 = affine 8 ⊔ Submodule.span F₂ {rZeroANF, rOneANF}

theorem UnrestrictedBooleanMul.N4.exists_rational_prefix (C : Circuit 8 8) (hC : C.Computes (Mul 4)) : ∃ (D : Circuit 8 8), D.Computes (Mul 4) ∧ D.finalWire = C.finalWire ∧ D.gate 0 = rZeroANF ∧ D.gate 1 = rOneANF ∧ D.gate 2 = rInfinityANF

Every eight-gate circuit for four-bit multiplication can be transformed, without changing its final wire space, so that its first three gates are the three rational-place products.

theorem UnrestrictedBooleanMul.N4.rationalLowSpace_le_targetAmbient : rationalLowSpace ≤ targetAmbient 8 (mulTarget 4)

theorem UnrestrictedBooleanMul.N4.prefixGates_three_eq_of_rational_prefix {C : Circuit 8 8} (hzero : C.gate 0 = rZeroANF) (hone : C.gate 1 = rOneANF) (hinfinity : C.gate 2 = rInfinityANF) : prefixGates C.gate 3 = {rZeroANF, rOneANF, rInfinityANF}

theorem UnrestrictedBooleanMul.N4.wireSpace_three_eq_of_rational_prefix {C : Circuit 8 8} (hzero : C.gate 0 = rZeroANF) (hone : C.gate 1 = rOneANF) (hinfinity : C.gate 2 = rInfinityANF) : wireSpace C.gate 3 = rationalLowSpace

theorem UnrestrictedBooleanMul.N4.inf_sup_span_eq_left_of_le_of_not_mem (V A : Submodule F₂ (ANF 8)) (g : ANF 8) (hVA : V ≤ A) (hg : g ∉ A) : (V ⊔ F₂ ∙ g) ⊓ A = V

If a state already lies in the target ambient, adjoining a vector outside that ambient does not change its intersection with the ambient.

theorem UnrestrictedBooleanMul.N4.useful_gate_mem_targetAmbient_of_prefix_le (C : Circuit 8 8) (j : Fin 8) (hprefix : circuitFlag C ↑j ≤ targetAmbient 8 (mulTarget 4)) (huse : UsefulAt C (mulTarget 4) j) : C.gate j ∈ targetAmbient 8 (mulTarget 4)

theorem UnrestrictedBooleanMul.N4.flagTargetRank_mono_of_affine_le {V W T : Submodule F₂ (ANF 8)} (hAffV : affine 8 ≤ V) (hVW : V ≤ W) : flagTargetRank V T ≤ flagTargetRank W T

theorem UnrestrictedBooleanMul.N4.flagDefectRank_eq_zero_of_le {V T : Submodule F₂ (ANF 8)} (hV : V ≤ targetAmbient 8 T) : flagDefectRank V T = 0

theorem UnrestrictedBooleanMul.N4.rational_prefix_seed_not_useful (C : Circuit 8 8) (hC : C.Computes (Mul 4)) (hzero : C.gate 0 = rZeroANF) (hone : C.gate 1 = rOneANF) (hinfinity : C.gate 2 = rInfinityANF) : ¬UsefulAt C (mulTarget 4) 3

In a rationally prefixed multiplier the fourth gate is the unique defect gate: if it were useful, its output would lie in the target ambient, and the low-product bridge would make it redundant.

theorem UnrestrictedBooleanMul.N4.rational_prefix_suffix_useful (C : Circuit 8 8) (hC : C.Computes (Mul 4)) (hzero : C.gate 0 = rZeroANF) (hone : C.gate 1 = rOneANF) (hinfinity : C.gate 2 = rInfinityANF) (hseed : ¬UsefulAt C (mulTarget 4) 3) (j : Fin 8) : 4 ≤ ↑j → UsefulAt C (mulTarget 4) j

Once the rational prefix and its non-useful seed account for the unique defect, the four remaining gates must each buy exactly one target dimension.

theorem UnrestrictedBooleanMul.N4.exists_normalized_eight (C : Circuit 8 8) (hC : C.Computes (Mul 4)) : ∃ (D : Circuit 8 8), NormalizedEight D

Closed normalized-eight-gate construction used by the structural proof.