Quadratic ANF projection

This is the coefficient-level bridge between Boolean ANFs and alternating two-forms. Diagonal entries are set to zero; off-diagonal entries are the squarefree quadratic coefficients. Products of affine ANFs therefore become decomposable alternating forms.

def UnrestrictedBooleanMul.N4.anfLinearProjection : ANF 8 →ₗ[F₂] LinearForm

Extract the coefficients of the eight linear monomials.

Equations

• UnrestrictedBooleanMul.N4.anfLinearProjection = { toFun := fun (p : UnrestrictedBooleanMul.ANF 8) (i : Fin 8) => p.coeff { vars := {i} }, map_add' := ⋯, map_smul' := ⋯ }

def UnrestrictedBooleanMul.N4.anfTwoProjection : ANF 8 →ₗ[F₂] TwoForm

Extract quadratic coefficients, with repeated-index coordinates zero.

Equations

• UnrestrictedBooleanMul.N4.anfTwoProjection = { toFun := fun (p : UnrestrictedBooleanMul.ANF 8) (i j : Fin 8) => if i = j then 0 else p.coeff { vars := {i, j} }, map_add' := ⋯, map_smul' := ⋯ }

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_one : anfTwoProjection 1 = 0

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_X (i : Fin 8) : anfTwoProjection (X i) = 0

@[simp]

theorem UnrestrictedBooleanMul.N4.anfLinearProjection_one : anfLinearProjection 1 = 0

@[simp]

theorem UnrestrictedBooleanMul.N4.anfLinearProjection_X (i j : Fin 8) : anfLinearProjection (X i) j = if j = i then 1 else 0

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_kills_affine : affine 8 ≤ anfTwoProjection.ker

theorem UnrestrictedBooleanMul.N4.vectorWedge_add_left_qp (u v w : LinearForm) : vectorWedge (u + v) w = vectorWedge u w + vectorWedge v w

theorem UnrestrictedBooleanMul.N4.vectorWedge_add_right_qp (u v w : LinearForm) : vectorWedge u (v + w) = vectorWedge u v + vectorWedge u w

theorem UnrestrictedBooleanMul.N4.vectorWedge_smul_left_qp (a : F₂) (u v : LinearForm) : vectorWedge (a • u) v = a • vectorWedge u v

theorem UnrestrictedBooleanMul.N4.vectorWedge_smul_right_qp (a : F₂) (u v : LinearForm) : vectorWedge u (a • v) = a • vectorWedge u v

@[simp]

theorem UnrestrictedBooleanMul.N4.vectorWedge_zero_left_qp (v : LinearForm) : vectorWedge 0 v = 0

@[simp]

theorem UnrestrictedBooleanMul.N4.vectorWedge_zero_right_qp (u : LinearForm) : vectorWedge u 0 = 0

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_X_mul_X (i j : Fin 8) : anfTwoProjection (X i * X j) = vectorWedge (anfLinearProjection (X i)) (anfLinearProjection (X j))

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_mul_of_affine {p q : ANF 8} (hp : p ∈ affine 8) (hq : q ∈ affine 8) : IsDecomposableTwo (anfTwoProjection (p * q))

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_aVar_mul_bVar (i j : Fin 4) : anfTwoProjection (aVar 4 i * bVar 4 j) = vectorWedge (anfLinearProjection (aVar 4 i)) (anfLinearProjection (bVar 4 j))

@[simp]

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_ite_zero (P : Prop) [Decidable P] (p : ANF 8) : anfTwoProjection (if P then p else 0) = if P then anfTwoProjection p else 0

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_Mul (s : Fin 7) : anfTwoProjection (Mul 4 s) = targetTwo (targetBasis s)

theorem UnrestrictedBooleanMul.N4.targetBasis_reconstruction (c : TargetCoeff) : ∑ s : Fin 7, c s • targetBasis s = c

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_targetANF (c : TargetCoeff) : anfTwoProjection (targetANF c) = targetTwo c