N3 for unrestricted Boolean polynomial multiplication

noncomputable def UnrestrictedBooleanMul.targetSum : ANF 6

Sum of the five output coefficients for three-term multiplication.

Equations

• UnrestrictedBooleanMul.targetSum = ∑ i : Fin 5, UnrestrictedBooleanMul.Mul 3 i

noncomputable def UnrestrictedBooleanMul.rationalBasis : Fin 10 → ANF 6

Affine inputs followed by the three rational-place evaluations for three-term products.

Equations

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

noncomputable def UnrestrictedBooleanMul.ambientBasis : Fin 12 → ANF 6

Affine inputs followed by the five output coefficients for three-term products.

Equations

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

noncomputable def UnrestrictedBooleanMul.rationalRep (c : Fin 10 → F₂) : ANF 6

The ANF represented by a coefficient vector in the rational-place basis.

Equations

• UnrestrictedBooleanMul.rationalRep c = ∑ i : Fin 10, c i • UnrestrictedBooleanMul.rationalBasis i

noncomputable def UnrestrictedBooleanMul.ambientRep (c : Fin 12 → F₂) : ANF 6

The ANF represented by a coefficient vector in the affine-plus-target basis.

Equations

• UnrestrictedBooleanMul.ambientRep c = ∑ i : Fin 12, c i • UnrestrictedBooleanMul.ambientBasis i

def UnrestrictedBooleanMul.solveProductCoeff : Lean.ParserDescr

Extract coefficients bilinearly, then normalize the resulting scalar polynomial.

Equations

• UnrestrictedBooleanMul.solveProductCoeff = Lean.ParserDescr.node `UnrestrictedBooleanMul.solveProductCoeff 1024 (Lean.ParserDescr.nonReservedSymbol "solve_product_coeff" false)

theorem UnrestrictedBooleanMul.product_coeff_c3 (a b : Fin 10 → F₂) : (rationalRep a * rationalRep b).coeff { vars := {0, 1, 4} } = N3Certificate.c3 a b

theorem UnrestrictedBooleanMul.product_coeff_c20 (a b : Fin 10 → F₂) : (rationalRep a * rationalRep b).coeff { vars := {0, 4, 5} } = N3Certificate.c20 a b

theorem UnrestrictedBooleanMul.product_coeff_c25 (a b : Fin 10 → F₂) : (rationalRep a * rationalRep b).coeff { vars := {0, 1} } = N3Certificate.c25 a b

theorem UnrestrictedBooleanMul.product_coeff_c30 (a b : Fin 10 → F₂) : (rationalRep a * rationalRep b).coeff { vars := {4, 5} } = N3Certificate.c30 a b

theorem UnrestrictedBooleanMul.product_coeff_c31 (a b : Fin 10 → F₂) : (rationalRep a * rationalRep b).coeff { vars := {0, 4} } + (rationalRep a * rationalRep b).coeff { vars := {1, 3} } = N3Certificate.c31 a b

theorem UnrestrictedBooleanMul.product_coeff_c32 (a b : Fin 10 → F₂) : (rationalRep a * rationalRep b).coeff { vars := {0, 5} } + (rationalRep a * rationalRep b).coeff { vars := {1, 4} } = N3Certificate.c32 a b

theorem UnrestrictedBooleanMul.product_coeff_c34 (a b : Fin 10 → F₂) : (rationalRep a * rationalRep b).coeff { vars := {1, 5} } + (rationalRep a * rationalRep b).coeff { vars := {2, 4} } = N3Certificate.c34 a b

theorem UnrestrictedBooleanMul.product_coeff_g0 (a b : Fin 10 → F₂) : (rationalRep a * rationalRep b).coeff { vars := {0, 4} } + (rationalRep a * rationalRep b).coeff { vars := {0, 5} } = N3Certificate.g0 a b

theorem UnrestrictedBooleanMul.product_coeff_g1 (a b : Fin 10 → F₂) : (rationalRep a * rationalRep b).coeff { vars := {0, 5} } + (rationalRep a * rationalRep b).coeff { vars := {1, 5} } = N3Certificate.g1 a b

noncomputable def UnrestrictedBooleanMul.rationalSpace : Submodule F₂ (ANF 6)

Affine functions together with the three rational-place product evaluations.

Equations

• UnrestrictedBooleanMul.rationalSpace = Submodule.span UnrestrictedBooleanMul.F₂ (Set.range UnrestrictedBooleanMul.rationalBasis)

noncomputable def UnrestrictedBooleanMul.ambientSpace : Submodule F₂ (ANF 6)

The span of affine functions and every three-term product coefficient.

Equations

• UnrestrictedBooleanMul.ambientSpace = Submodule.span UnrestrictedBooleanMul.F₂ (Set.range UnrestrictedBooleanMul.ambientBasis)

theorem UnrestrictedBooleanMul.mem_rationalSpace_iff {p : ANF 6} : p ∈ rationalSpace ↔ ∃ (c : Fin 10 → F₂), rationalRep c = p

theorem UnrestrictedBooleanMul.mem_ambientSpace_iff {p : ANF 6} : p ∈ ambientSpace ↔ ∃ (c : Fin 12 → F₂), ambientRep c = p

def UnrestrictedBooleanMul.ambientAnchor : Fin 12 → Monomial 6

Monomials whose coefficients recover coordinates in the affine-plus-target basis.

Equations

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

def UnrestrictedBooleanMul.ambientProjection : ANF 6 →ₗ[F₂] Fin 12 → F₂

Extract the twelve anchor coefficients of a six-variable ANF.

Equations

• UnrestrictedBooleanMul.ambientProjection = UnrestrictedBooleanMul.coefficientProjection UnrestrictedBooleanMul.ambientAnchor

def UnrestrictedBooleanMul.solveAmbientProjection : Lean.ParserDescr

Check a concrete basis vector by its twelve anchor coefficients.

Equations

• UnrestrictedBooleanMul.solveAmbientProjection = Lean.ParserDescr.node `UnrestrictedBooleanMul.solveAmbientProjection 1024 (Lean.ParserDescr.nonReservedSymbol "solve_ambient_projection" false)

@[simp]

theorem UnrestrictedBooleanMul.ambientProjection_one : ambientProjection 1 = (Pi.basisFun F₂ (Fin 12)) 0

@[simp]

theorem UnrestrictedBooleanMul.ambientProjection_X_zero : ambientProjection (X 0) = (Pi.basisFun F₂ (Fin 12)) 1

@[simp]

theorem UnrestrictedBooleanMul.ambientProjection_X_one : ambientProjection (X 1) = (Pi.basisFun F₂ (Fin 12)) 2

@[simp]

theorem UnrestrictedBooleanMul.ambientProjection_X_two : ambientProjection (X 2) = (Pi.basisFun F₂ (Fin 12)) 3

@[simp]

theorem UnrestrictedBooleanMul.ambientProjection_X_three : ambientProjection (X 3) = (Pi.basisFun F₂ (Fin 12)) 4

@[simp]

theorem UnrestrictedBooleanMul.ambientProjection_X_four : ambientProjection (X 4) = (Pi.basisFun F₂ (Fin 12)) 5

@[simp]

theorem UnrestrictedBooleanMul.ambientProjection_X_five : ambientProjection (X 5) = (Pi.basisFun F₂ (Fin 12)) 6

@[simp]

theorem UnrestrictedBooleanMul.ambientProjection_mul_zero : ambientProjection (Mul 3 0) = (Pi.basisFun F₂ (Fin 12)) 7

@[simp]

theorem UnrestrictedBooleanMul.ambientProjection_mul_one : ambientProjection (Mul 3 1) = (Pi.basisFun F₂ (Fin 12)) 8

@[simp]

theorem UnrestrictedBooleanMul.ambientProjection_mul_two : ambientProjection (Mul 3 2) = (Pi.basisFun F₂ (Fin 12)) 9

@[simp]

theorem UnrestrictedBooleanMul.ambientProjection_mul_three : ambientProjection (Mul 3 3) = (Pi.basisFun F₂ (Fin 12)) 10

@[simp]

theorem UnrestrictedBooleanMul.ambientProjection_mul_four : ambientProjection (Mul 3 4) = (Pi.basisFun F₂ (Fin 12)) 11

theorem UnrestrictedBooleanMul.ambientProjection_basis (i : Fin 12) : ambientProjection (ambientBasis i) = (Pi.basisFun F₂ (Fin 12)) i

theorem UnrestrictedBooleanMul.ambientBasis_linearIndependent : LinearIndependent F₂ ambientBasis

theorem UnrestrictedBooleanMul.ambientSpace_finrank : Module.finrank F₂ ↥ambientSpace = 12

noncomputable def UnrestrictedBooleanMul.freeBasis : Fin 7 → ANF 6

The constant function and six input variables available without AND gates.

Equations

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

theorem UnrestrictedBooleanMul.affine_six_eq_span_freeBasis : affine 6 = Submodule.span F₂ (Set.range freeBasis)

theorem UnrestrictedBooleanMul.affine_six_finrank_le : Module.finrank F₂ ↥(affine 6) ≤ 7

theorem UnrestrictedBooleanMul.rationalBasis_mem (i : Fin 10) : rationalBasis i ∈ rationalSpace

theorem UnrestrictedBooleanMul.ambientBasis_mem (i : Fin 12) : ambientBasis i ∈ ambientSpace

theorem UnrestrictedBooleanMul.affine_le_rationalSpace : affine 6 ≤ rationalSpace

theorem UnrestrictedBooleanMul.ambientSpace_eq_mulAmbient : ambientSpace = mulAmbient 3

theorem UnrestrictedBooleanMul.targetSum_mem_ambientSpace : targetSum ∈ ambientSpace

theorem UnrestrictedBooleanMul.rationalSpace_le_ambientSpace : rationalSpace ≤ ambientSpace

def UnrestrictedBooleanMul.solveAmbientCoeff : Lean.ParserDescr

Evaluate a selected coefficient of an ANF in the affine-plus-target span.

Equations

• UnrestrictedBooleanMul.solveAmbientCoeff = Lean.ParserDescr.node `UnrestrictedBooleanMul.solveAmbientCoeff 1024 (Lean.ParserDescr.nonReservedSymbol "solve_ambient_coeff" false)

theorem UnrestrictedBooleanMul.algebraic_cert (a b : Fin 10 → F₂) (z : Fin 12 → F₂) (h : rationalRep a * rationalRep b = ambientRep z) : z 8 = z 9 ∧ z 9 = z 10

def UnrestrictedBooleanMul.rationalOfAmbient (z : Fin 12 → F₂) : Fin 10 → F₂

Rational-place coordinates when the three middle target coefficients agree.

Equations

• UnrestrictedBooleanMul.rationalOfAmbient z = ![z 0, z 1, z 2, z 3, z 4, z 5, z 6, z 7 + z 8, z 11 + z 8, z 8]

theorem UnrestrictedBooleanMul.ambientRep_mem_rationalSpace (z : Fin 12 → F₂) (h₈₉ : z 8 = z 9) (h₉₁₀ : z 9 = z 10) : ambientRep z ∈ rationalSpace

theorem UnrestrictedBooleanMul.rational_mul_mem_of_mem_ambient {f g : ANF 6} (hf : f ∈ rationalSpace) (hg : g ∈ rationalSpace) (hfg : f * g ∈ ambientSpace) : f * g ∈ rationalSpace

theorem UnrestrictedBooleanMul.mul_three_one_not_mem_rationalSpace : Mul 3 1 ∉ rationalSpace

theorem UnrestrictedBooleanMul.finalWire_finrank_le_twelve (C : Circuit 6 5) : Module.finrank F₂ ↥C.finalWire ≤ 12

theorem UnrestrictedBooleanMul.ambientSpace_le_finalWire (C : Circuit 6 5) (computes : C.Computes (Mul 3)) : ambientSpace ≤ C.finalWire

theorem UnrestrictedBooleanMul.finalWire_eq_ambientSpace (C : Circuit 6 5) (computes : C.Computes (Mul 3)) : C.finalWire = ambientSpace

theorem UnrestrictedBooleanMul.five_gate_impossible (C : Circuit 6 5) : ¬C.Computes (Mul 3)

theorem UnrestrictedBooleanMul.mul_three_dimension_lower (r : ℕ) (h : HasCircuit (Mul 3) r) : 5 ≤ r

theorem UnrestrictedBooleanMul.mul_three_lower (r : ℕ) (h : HasCircuit (Mul 3) r) : 6 ≤ r

theorem UnrestrictedBooleanMul.mc_mul_three : MC(Mul 3) = 6