Binary polynomial multiplication targets

noncomputable def UnrestrictedBooleanMul.aVar (n : ℕ) (i : Fin n) : ANF (2 * n)

The variable a_i among the 2n multiplication inputs.

Equations

• UnrestrictedBooleanMul.aVar n i = UnrestrictedBooleanMul.X ⟨↑i, ⋯⟩

noncomputable def UnrestrictedBooleanMul.bVar (n : ℕ) (j : Fin n) : ANF (2 * n)

The variable b_j among the 2n multiplication inputs.

Equations

• UnrestrictedBooleanMul.bVar n j = UnrestrictedBooleanMul.X ⟨n + ↑j, ⋯⟩

@[simp]

theorem UnrestrictedBooleanMul.aVar_mem_affine (n : ℕ) (i : Fin n) : aVar n i ∈ affine (2 * n)

@[simp]

theorem UnrestrictedBooleanMul.bVar_mem_affine (n : ℕ) (j : Fin n) : bVar n j ∈ affine (2 * n)

noncomputable def UnrestrictedBooleanMul.mulCoefficient (n s : ℕ) : ANF (2 * n)

Coefficient s of the product of two n-term binary polynomials.

Equations

• UnrestrictedBooleanMul.mulCoefficient n s = ∑ i : Fin n, ∑ j : Fin n, if ↑i + ↑j = s then UnrestrictedBooleanMul.aVar n i * UnrestrictedBooleanMul.bVar n j else 0

noncomputable def UnrestrictedBooleanMul.Mul (n : ℕ) : Fin (2 * n - 1) → ANF (2 * n)

Binary n-term polynomial multiplication in Boolean ANF.

Equations

• UnrestrictedBooleanMul.Mul n s = UnrestrictedBooleanMul.mulCoefficient n ↑s

noncomputable def UnrestrictedBooleanMul.mulTarget (n : ℕ) : Submodule F₂ (ANF (2 * n))

The linear target space spanned by all multiplication coordinates.

Equations

• UnrestrictedBooleanMul.mulTarget n = Submodule.span UnrestrictedBooleanMul.F₂ (Set.range (UnrestrictedBooleanMul.Mul n))

noncomputable def UnrestrictedBooleanMul.mulAmbient (n : ℕ) : Submodule F₂ (ANF (2 * n))

Affine functions plus the multiplication target.

Equations

• UnrestrictedBooleanMul.mulAmbient n = UnrestrictedBooleanMul.affine (2 * n) ⊔ UnrestrictedBooleanMul.mulTarget n

theorem UnrestrictedBooleanMul.Mul_mem_target (n : ℕ) (s : Fin (2 * n - 1)) : Mul n s ∈ mulTarget n

def UnrestrictedBooleanMul.coefficientProjection {m d : ℕ} (anchor : Fin d → Monomial m) : ANF m →ₗ[F₂] Fin d → F₂

Coefficient projection onto a chosen finite family of squarefree monomials.

Equations

• UnrestrictedBooleanMul.coefficientProjection anchor = { toFun := fun (p : UnrestrictedBooleanMul.ANF m) (i : Fin d) => p.coeff (anchor i), map_add' := ⋯, map_smul' := ⋯ }

theorem UnrestrictedBooleanMul.coefficient_eq_zero_of_mem_affine {m : ℕ} {p : ANF m} (hp : p ∈ affine m) (s : Monomial m) (hs : s.vars.card = 2) : p.coeff s = 0

theorem UnrestrictedBooleanMul.coefficientProjection_kills_affine {m d : ℕ} (anchor : Fin d → Monomial m) (degree_two : ∀ (i : Fin d), (anchor i).vars.card = 2) : affine m ≤ (coefficientProjection anchor).ker