Affine restrictions of binary-field multiplication

A nonzero component ℓ(xy) of multiplication is a quadratic form on the 2n-dimensional input space. It is affine on a + U exactly when U is totally isotropic for its polar form B((x, y), (x', y')) = ℓ(xy' + x'y). This form is nondegenerate, because t ↦ ℓ(xt) is nonzero whenever x ≠ 0. Totally isotropic subspaces therefore have dimension at most n, so no nonzero component is affine on a flat with 2^(n+1) points.

noncomputable def Algebraic.Aggregate.Geometry.FieldMul.firstFactor {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} (b : Module.Basis (Fin n) (ZMod 2) K) : (Fin (n + n) → ZMod 2) →ₗ[ZMod 2] K

The first factor encoded by the first n prime-field inputs.

Equations

• Algebraic.Aggregate.Geometry.FieldMul.firstFactor b = ↑b.equivFun.symm ∘ₗ LinearMap.funLeft (ZMod 2) (ZMod 2) (Fin.castAdd n)

noncomputable def Algebraic.Aggregate.Geometry.FieldMul.secondFactor {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} (b : Module.Basis (Fin n) (ZMod 2) K) : (Fin (n + n) → ZMod 2) →ₗ[ZMod 2] K

The second factor encoded by the last n prime-field inputs.

Equations

• Algebraic.Aggregate.Geometry.FieldMul.secondFactor b = ↑b.equivFun.symm ∘ₗ LinearMap.funLeft (ZMod 2) (ZMod 2) (Fin.natAdd n)

theorem Algebraic.Aggregate.Geometry.FieldMul.fieldMul_eq {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} (b : Module.Basis (Fin n) (ZMod 2) K) (v : Fin (n + n) → ZMod 2) : Cutwidth.MultiOutput.fieldMul b v = ⇑(b.repr ((firstFactor b) v * (secondFactor b) v))

Multiplication in coordinates multiplies the two encoded factors.

theorem Algebraic.Aggregate.Geometry.FieldMul.bitValue_boolFieldMul {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} (b : Module.Basis (Fin n) (ZMod 2) K) (z : Fin (n + n) → Bool) (i : Fin n) : bitValue (boolFieldMul b z i) = (b.repr ((firstFactor b) (bitVector z) * (secondFactor b) (bitVector z))) i

The prime-field outputs of Boolean multiplication.

theorem Algebraic.Aggregate.Geometry.FieldMul.factors_append {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} (b : Module.Basis (Fin n) (ZMod 2) K) (p q : Fin n → ZMod 2) : (firstFactor b) (Fin.append p q) = b.equivFun.symm p ∧ (secondFactor b) (Fin.append p q) = b.equivFun.symm q

The encoded factors of concatenated coordinates.

theorem Algebraic.Aggregate.Geometry.FieldMul.eq_zero_of_factors {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} (b : Module.Basis (Fin n) (ZMod 2) K) {v : Fin (n + n) → ZMod 2} (first : (firstFactor b) v = 0) (second : (secondFactor b) v = 0) : v = 0

Both encoded factors vanish only at the zero vector.

noncomputable def Algebraic.Aggregate.Geometry.FieldMul.polarForm {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} (b : Module.Basis (Fin n) (ZMod 2) K) (ℓ : K →ₗ[ZMod 2] ZMod 2) : LinearMap.BilinForm (ZMod 2) (Fin (n + n) → ZMod 2)

The polar form B(u, w) = ℓ(x_u y_w + x_w y_u) of the component ℓ(xy).

Equations

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

@[simp]

theorem Algebraic.Aggregate.Geometry.FieldMul.polarForm_apply {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} (b : Module.Basis (Fin n) (ZMod 2) K) (ℓ : K →ₗ[ZMod 2] ZMod 2) (u w : Fin (n + n) → ZMod 2) : ((polarForm b ℓ) u) w = ℓ ((firstFactor b) u * (secondFactor b) w + (firstFactor b) w * (secondFactor b) u)

theorem Algebraic.Aggregate.Geometry.FieldMul.polarForm_ker_eq_bot {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} (b : Module.Basis (Fin n) (ZMod 2) K) {ℓ : K →ₗ[ZMod 2] ZMod 2} (nonzero : ℓ ≠ 0) : LinearMap.ker (polarForm b ℓ) = ⊥

A nonzero component makes the polar form nondegenerate.

theorem Algebraic.Aggregate.Geometry.FieldMul.polar_eq_zero_of_affine {K : Type u_1} [Field K] [Algebra (ZMod 2) K] [CharP K 2] (ℓ : K →ₗ[ZMod 2] ZMod 2) {A P R A' P' R' : K} (affine : ℓ ((A + P + A + (A + R)) * (A' + P' + A' + (A' + R'))) = ℓ ((A + P) * (A' + P')) + ℓ (A * A') + ℓ ((A + R) * (A' + R'))) : ℓ (P * R' + R * P') = 0

A component ℓ(xy) preserving ternary sums at a + u, a, a + w vanishes on the polar form at (u, w).

theorem Algebraic.Aggregate.Geometry.FieldMul.nonaffineOnFlats_boolFieldMul {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} (b : Module.Basis (Fin n) (ZMod 2) K) : NonaffineOnFlats (boolFieldMul b) (n + 1)

No nonzero component of binary-field multiplication is affine on a flat with 2^(n+1) points.