Algebraic exclusion of seven gates

A seven-gate circuit computing Mul 4 would have no defect: its final wire space contains the sixteen-dimensional space Aff + T, while seven gates can raise the affine dimension by at most seven. Thus every intermediate wire lands in Aff + T. The rational-prefix closure theorem then traps every gate in Aff + R, contradicting the presence of a non-rational target direction.

This argument uses neither circuit enumeration nor a truth-table search.

theorem UnrestrictedBooleanMul.N4.targetAmbient_le_finalWire {r : ℕ} (C : Circuit 8 r) (hC : C.Computes (Mul 4)) : targetAmbient 8 (mulTarget 4) ≤ C.finalWire

theorem UnrestrictedBooleanMul.N4.finalWire_eq_targetAmbient_of_seven (C : Circuit 8 7) (hC : C.Computes (Mul 4)) : C.finalWire = targetAmbient 8 (mulTarget 4)

Seven gates leave no room for a direction outside Aff + T.

theorem UnrestrictedBooleanMul.N4.wireSpace_le_rationalLow_of_prefix {r j : ℕ} (C : Circuit 8 r) (hgate : ∀ (i : Fin r), ↑i < j → C.gate i ∈ rationalLowSpace) : wireSpace C.gate j ≤ rationalLowSpace

theorem UnrestrictedBooleanMul.N4.no_seven_gate_circuit : ¬Nonempty { C : Circuit 8 7 // C.Computes (Mul 4) }

The purely algebraic seven-gate lower bound used by normalization.

theorem UnrestrictedBooleanMul.N4.eight_gate_defect_is_one_algebraic (C : Circuit 8 8) (hC : C.Computes (Mul 4)) : flagDefectRank C.finalWire (mulTarget 4) = 1

The defect budget of eight gates is attained. If it were zero, the same rational-prefix trap used above would contain the entire target space.

theorem UnrestrictedBooleanMul.N4.eight_gate_all_nonredundant (C : Circuit 8 8) (hC : C.Computes (Mul 4)) (i : Fin 8) : NonredundantAt C i

Attaining target rank seven and defect one forces every one of the eight gate outputs to be a genuinely new wire-space direction.