Exact small cases and explicit upper-bound circuits

theorem UnrestrictedBooleanMul.submodule_add_mem {m : ℕ} {S : Submodule F₂ (ANF m)} {x y : ANF m} (hx : x ∈ S) (hy : y ∈ S) : x + y ∈ S

def UnrestrictedBooleanMul.TargetCoordinates.oneAnchor : Fin 1 → Monomial 2

Anchor monomials recovering the 1-term product coefficients.

Equations

• UnrestrictedBooleanMul.TargetCoordinates.oneAnchor = ![{ vars := {0, 1} }]

def UnrestrictedBooleanMul.TargetCoordinates.twoAnchor : Fin 3 → Monomial 4

Anchor monomials recovering the 2-term product coefficients.

Equations

• UnrestrictedBooleanMul.TargetCoordinates.twoAnchor = ![{ vars := {0, 2} }, { vars := {0, 3} }, { vars := {1, 3} }]

def UnrestrictedBooleanMul.TargetCoordinates.threeAnchor : Fin 5 → Monomial 6

Anchor monomials recovering the 3-term product coefficients.

Equations

• UnrestrictedBooleanMul.TargetCoordinates.threeAnchor = ![{ vars := {0, 3} }, { vars := {0, 4} }, { vars := {0, 5} }, { vars := {1, 5} }, { vars := {2, 5} }]

def UnrestrictedBooleanMul.TargetCoordinates.oneProjection : ANF 2 →ₗ[F₂] Fin 1 → F₂

Extract the anchor coefficients for a 1-term product.

Equations

• UnrestrictedBooleanMul.TargetCoordinates.oneProjection = UnrestrictedBooleanMul.coefficientProjection UnrestrictedBooleanMul.TargetCoordinates.oneAnchor

def UnrestrictedBooleanMul.TargetCoordinates.twoProjection : ANF 4 →ₗ[F₂] Fin 3 → F₂

Extract the anchor coefficients for a 2-term product.

Equations

• UnrestrictedBooleanMul.TargetCoordinates.twoProjection = UnrestrictedBooleanMul.coefficientProjection UnrestrictedBooleanMul.TargetCoordinates.twoAnchor

def UnrestrictedBooleanMul.TargetCoordinates.threeProjection : ANF 6 →ₗ[F₂] Fin 5 → F₂

Extract the anchor coefficients for a 3-term product.

Equations

• UnrestrictedBooleanMul.TargetCoordinates.threeProjection = UnrestrictedBooleanMul.coefficientProjection UnrestrictedBooleanMul.TargetCoordinates.threeAnchor

theorem UnrestrictedBooleanMul.TargetCoordinates.oneAnchor_degree (i : Fin 1) : (oneAnchor i).vars.card = 2

theorem UnrestrictedBooleanMul.TargetCoordinates.twoAnchor_degree (i : Fin 3) : (twoAnchor i).vars.card = 2

theorem UnrestrictedBooleanMul.TargetCoordinates.threeAnchor_degree (i : Fin 5) : (threeAnchor i).vars.card = 2

theorem UnrestrictedBooleanMul.TargetCoordinates.oneProjection_kills_affine : affine 2 ≤ oneProjection.ker

theorem UnrestrictedBooleanMul.TargetCoordinates.twoProjection_kills_affine : affine 4 ≤ twoProjection.ker

theorem UnrestrictedBooleanMul.TargetCoordinates.threeProjection_kills_affine : affine 6 ≤ threeProjection.ker

theorem UnrestrictedBooleanMul.TargetCoordinates.oneProjection_Mul (i : Fin 1) : oneProjection (Mul 1 i) = (Pi.basisFun F₂ (Fin 1)) i

theorem UnrestrictedBooleanMul.TargetCoordinates.twoProjection_Mul (i : Fin 3) : twoProjection (Mul 2 i) = (Pi.basisFun F₂ (Fin 3)) i

theorem UnrestrictedBooleanMul.TargetCoordinates.threeProjection_Mul (i : Fin 5) : threeProjection (Mul 3 i) = (Pi.basisFun F₂ (Fin 5)) i

One term

noncomputable def UnrestrictedBooleanMul.UpperCircuits.oneLeft : Fin 1 → ANF 2

Left AND-gate inputs of the explicit 1-gate circuit for 1-term multiplication.

Equations

• UnrestrictedBooleanMul.UpperCircuits.oneLeft = ![UnrestrictedBooleanMul.aVar 1 0]

noncomputable def UnrestrictedBooleanMul.UpperCircuits.oneRight : Fin 1 → ANF 2

Right AND-gate inputs of the explicit 1-gate circuit for 1-term multiplication.

Equations

• UnrestrictedBooleanMul.UpperCircuits.oneRight = ![UnrestrictedBooleanMul.bVar 1 0]

noncomputable def UnrestrictedBooleanMul.UpperCircuits.one : Circuit 2 1

An explicit 1-gate circuit for 1-term Boolean polynomial multiplication.

Equations

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

theorem UnrestrictedBooleanMul.UpperCircuits.one_computes : one.Computes (Mul 1)

Two terms (Karatsuba)

noncomputable def UnrestrictedBooleanMul.UpperCircuits.twoLeft : Fin 3 → ANF 4

Left AND-gate inputs of the explicit 3-gate circuit for 2-term multiplication.

Equations

• UnrestrictedBooleanMul.UpperCircuits.twoLeft = ![UnrestrictedBooleanMul.aVar 2 0, UnrestrictedBooleanMul.aVar 2 1, UnrestrictedBooleanMul.aVar 2 0 + UnrestrictedBooleanMul.aVar 2 1]

noncomputable def UnrestrictedBooleanMul.UpperCircuits.twoRight : Fin 3 → ANF 4

Right AND-gate inputs of the explicit 3-gate circuit for 2-term multiplication.

Equations

• UnrestrictedBooleanMul.UpperCircuits.twoRight = ![UnrestrictedBooleanMul.bVar 2 0, UnrestrictedBooleanMul.bVar 2 1, UnrestrictedBooleanMul.bVar 2 0 + UnrestrictedBooleanMul.bVar 2 1]

noncomputable def UnrestrictedBooleanMul.UpperCircuits.two : Circuit 4 3

An explicit 3-gate circuit for 2-term Boolean polynomial multiplication.

Equations

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

noncomputable def UnrestrictedBooleanMul.UpperCircuits.twoRecombine : Fin 3 → ANF 4

Recover the 2-term product coefficients by XORs of the circuit outputs.

Equations

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

theorem UnrestrictedBooleanMul.UpperCircuits.two_formula : Mul 2 = twoRecombine

theorem UnrestrictedBooleanMul.UpperCircuits.two_computes : two.Computes (Mul 2)

Three terms (six products)

noncomputable def UnrestrictedBooleanMul.UpperCircuits.threeLeft : Fin 6 → ANF 6

Left AND-gate inputs of the explicit 6-gate circuit for 3-term multiplication.

Equations

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

noncomputable def UnrestrictedBooleanMul.UpperCircuits.threeRight : Fin 6 → ANF 6

Right AND-gate inputs of the explicit 6-gate circuit for 3-term multiplication.

Equations

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

noncomputable def UnrestrictedBooleanMul.UpperCircuits.three : Circuit 6 6

An explicit 6-gate circuit for 3-term Boolean polynomial multiplication.

Equations

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

noncomputable def UnrestrictedBooleanMul.UpperCircuits.threeRecombine : Fin 5 → ANF 6

Recover the 3-term product coefficients by XORs of the circuit outputs.

Equations

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

theorem UnrestrictedBooleanMul.UpperCircuits.three_formula : Mul 3 = threeRecombine

theorem UnrestrictedBooleanMul.UpperCircuits.three_computes : three.Computes (Mul 3)

Four terms (two-level Karatsuba--Ofman)

noncomputable def UnrestrictedBooleanMul.UpperCircuits.fourLeft : Fin 9 → ANF 8

Left AND-gate inputs of the explicit 9-gate circuit for 4-term multiplication.

Equations

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

noncomputable def UnrestrictedBooleanMul.UpperCircuits.fourRight : Fin 9 → ANF 8

Right AND-gate inputs of the explicit 9-gate circuit for 4-term multiplication.

Equations

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

noncomputable def UnrestrictedBooleanMul.UpperCircuits.four : Circuit 8 9

An explicit 9-gate circuit for 4-term Boolean polynomial multiplication.

Equations

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

noncomputable def UnrestrictedBooleanMul.UpperCircuits.fourRecombine : Fin 7 → ANF 8

Recover the 4-term product coefficients by XORs of the circuit outputs.

Equations

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

theorem UnrestrictedBooleanMul.UpperCircuits.four_formula : Mul 4 = fourRecombine

theorem UnrestrictedBooleanMul.UpperCircuits.four_computes : four.Computes (Mul 4)

theorem UnrestrictedBooleanMul.mul_zero_upper : HasCircuit (Mul 0) 0

theorem UnrestrictedBooleanMul.mul_one_upper : HasCircuit (Mul 1) 1

theorem UnrestrictedBooleanMul.mul_two_upper : HasCircuit (Mul 2) 3

theorem UnrestrictedBooleanMul.mul_three_upper : HasCircuit (Mul 3) 6

theorem UnrestrictedBooleanMul.mul_four_upper : HasCircuit (Mul 4) 9

theorem UnrestrictedBooleanMul.mul_one_dimension_lower (r : ℕ) (h : HasCircuit (Mul 1) r) : 1 ≤ r

theorem UnrestrictedBooleanMul.mul_two_dimension_lower (r : ℕ) (h : HasCircuit (Mul 2) r) : 3 ≤ r

theorem UnrestrictedBooleanMul.mc_mul_zero : MC(Mul 0) = 0

theorem UnrestrictedBooleanMul.mc_mul_one : MC(Mul 1) = 1

theorem UnrestrictedBooleanMul.mc_mul_two : MC(Mul 2) = 3