Documentation

LeanPool.BooleanMultiplication.N4.Main

Exact unrestricted Boolean multiplicative complexity for four-term products #

The structural contradiction rules out eight gates. Together with the algebraic seven-gate obstruction and the explicit nine-gate construction, this closes the n = 4 theorem.

source
theorem UnrestrictedBooleanMul.N4.normalizedEight_contradiction {C : Circuit 8 8} (h : NormalizedEight C) :
False

The normalized eight-gate state is inconsistent: gate six is useful by the flag ledger and non-useful by first-jet saturation.

source
theorem UnrestrictedBooleanMul.N4.no_eight_gate_circuit :
¬HasCircuit (Mul 4) 8

There is no unrestricted eight-AND circuit for four-term Boolean multiplication.

source
theorem UnrestrictedBooleanMul.N4.mul_four_lower (r : ℕ) (hCircuit : HasCircuit (Mul 4) r) :
9 ≤ r

Every unrestricted circuit for Mul 4 has at least nine AND gates.

source
theorem UnrestrictedBooleanMul.N4.mc_mul_four :
MC(Mul 4) = 9

The unrestricted Boolean multiplicative complexity of four-term multiplication is exactly nine.