ANF low-product bridge

This module turns the exterior prefix-rigidity lemma into a statement about actual Boolean ANFs. All coordinate certificates below range only over an input coordinate and one of the three rational places; no circuit states are enumerated.

@[simp]

theorem UnrestrictedBooleanMul.N4.linearANF_zero : linearANF 0 = 0

theorem UnrestrictedBooleanMul.N4.linearANF_add (ell m : LinearForm) : linearANF (ell + m) = linearANF ell + linearANF m

theorem UnrestrictedBooleanMul.N4.linearANF_smul (a : F₂) (ell : LinearForm) : linearANF (a • ell) = a • linearANF ell

theorem UnrestrictedBooleanMul.N4.linearANF_coordinate (i : Fin 8) : linearANF (coordinateLinear i) = X i

theorem UnrestrictedBooleanMul.N4.affineANF_add (a b : F₂) (ell m : LinearForm) : affineANF (a + b) (ell + m) = affineANF a ell + affineANF b m

theorem UnrestrictedBooleanMul.N4.affineANF_smul (a b : F₂) (ell : LinearForm) : affineANF (a * b) (a • ell) = a • affineANF b ell

theorem UnrestrictedBooleanMul.N4.affineANF_mem (a : F₂) (ell : LinearForm) : affineANF a ell ∈ affine 8

theorem UnrestrictedBooleanMul.N4.exists_affineANF_of_mem {p : ANF 8} (hp : p ∈ affine 8) : ∃ (a : F₂) (ell : LinearForm), p = affineANF a ell

@[simp]

theorem UnrestrictedBooleanMul.N4.rationalANF_zero : rationalANF 0 = 0

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_linear_mul_linear (ell m : LinearForm) : anfThreeProjection (linearANF ell * linearANF m) = 0

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_affine_mul_affine (a b : F₂) (ell m : LinearForm) : anfThreeProjection (affineANF a ell * affineANF b m) = 0

theorem UnrestrictedBooleanMul.N4.quarticProbeANF_affine_mul_affine (a b : F₂) (ell m : LinearForm) : quarticProbeANF (affineANF a ell * affineANF b m) = 0

theorem UnrestrictedBooleanMul.N4.quarticProbeANF_affine_mul_rational (a : F₂) (ell : LinearForm) (β : Fin 3 → F₂) : quarticProbeANF (affineANF a ell * rationalANF β) = 0

theorem UnrestrictedBooleanMul.N4.quarticProbeANF_rational_mul_affine (α : Fin 3 → F₂) (b : F₂) (m : LinearForm) : quarticProbeANF (rationalANF α * affineANF b m) = 0

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_affine_mul_rational (a : F₂) (ell : LinearForm) (β : Fin 3 → F₂) : anfThreeProjection (affineANF a ell * rationalANF β) = vectorWedgeTwo ell (rationalTwo β)

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_rational_mul_affine (α : Fin 3 → F₂) (b : F₂) (m : LinearForm) : anfThreeProjection (rationalANF α * affineANF b m) = vectorWedgeTwo m (rationalTwo α)

theorem UnrestrictedBooleanMul.N4.lowProduct_quarticProjection (a b : F₂) (ell m : LinearForm) (α β : Fin 3 → F₂) : quarticProbeANF ((affineANF a ell + rationalANF α) * (affineANF b m + rationalANF β)) = quarticWedgeProbe (rationalTwo α) (rationalTwo β)

theorem UnrestrictedBooleanMul.N4.lowProduct_cubicProjection_of_quartic_zero (a b : F₂) (ell m : LinearForm) (α β : Fin 3 → F₂) (hprobe : quarticWedgeProbe (rationalTwo α) (rationalTwo β) = 0) : anfThreeProjection ((affineANF a ell + rationalANF α) * (affineANF b m + rationalANF β)) = rationalProductCubic ell m α β

def UnrestrictedBooleanMul.N4.vectorWedgeBilinear : LinearForm →ₗ[F₂] LinearForm →ₗ[F₂] TwoForm

The exterior product of two linear forms as a bilinear map.

Equations

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

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_linear_mul_linear (ell m : LinearForm) : anfTwoProjection (linearANF ell * linearANF m) = vectorWedge ell m

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_affine_mul_affine (a b : F₂) (ell m : LinearForm) : anfTwoProjection (affineANF a ell * affineANF b m) = vectorWedge ell m

def UnrestrictedBooleanMul.N4.monomialTwo (s : Finset (Fin 8)) : TwoForm

The quadratic coordinate array of a squarefree monomial.

Equations

• UnrestrictedBooleanMul.N4.monomialTwo s i j = if i = j then 0 else if s = {i, j} then 1 else 0

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_monomial (s : Finset (Fin 8)) : anfTwoProjection (monomial s) = monomialTwo s

theorem UnrestrictedBooleanMul.N4.booleanContraction_add_left_h (ell m : LinearForm) (q : TwoForm) : booleanContraction (ell + m) q = booleanContraction ell q + booleanContraction m q

theorem UnrestrictedBooleanMul.N4.booleanContraction_smul_left_h (a : F₂) (ell : LinearForm) (q : TwoForm) : booleanContraction (a • ell) q = a • booleanContraction ell q

theorem UnrestrictedBooleanMul.N4.booleanContraction_add_right_h (ell : LinearForm) (q r : TwoForm) : booleanContraction ell (q + r) = booleanContraction ell q + booleanContraction ell r

theorem UnrestrictedBooleanMul.N4.booleanContraction_smul_right_h (a : F₂) (ell : LinearForm) (q : TwoForm) : booleanContraction ell (a • q) = a • booleanContraction ell q

def UnrestrictedBooleanMul.N4.booleanContractionBilinear : LinearForm →ₗ[F₂] TwoForm →ₗ[F₂] TwoForm

Boolean contraction of a linear form with a two-form, as a bilinear map.

Equations

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

def UnrestrictedBooleanMul.N4.quadraticPlaceModel (r : Fin 8) (θ : Fin 3) : TwoForm

Quadratic part of an input variable times a rational-place product.

Equations

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

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_linear_mul_rational (ell : LinearForm) (β : Fin 3 → F₂) : anfTwoProjection (linearANF ell * rationalANF β) = booleanContraction ell (rationalTwo β)

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_rationalANF (α : Fin 3 → F₂) : anfTwoProjection (rationalANF α) = rationalTwo α

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_affine_mul_rational (a : F₂) (ell : LinearForm) (β : Fin 3 → F₂) : anfTwoProjection (affineANF a ell * rationalANF β) = a • rationalTwo β + booleanContraction ell (rationalTwo β)

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_rational_mul_affine (α : Fin 3 → F₂) (b : F₂) (m : LinearForm) : anfTwoProjection (rationalANF α * affineANF b m) = b • rationalTwo α + booleanContraction m (rationalTwo α)

theorem UnrestrictedBooleanMul.N4.lowProduct_quadraticProjection_of_quartic_zero (a b : F₂) (ell m : LinearForm) (α β : Fin 3 → F₂) (hprobe : quarticWedgeProbe (rationalTwo α) (rationalTwo β) = 0) : anfTwoProjection ((affineANF a ell + rationalANF α) * (affineANF b m + rationalANF β)) = rationalProductQuadratic a b ell m α β

theorem UnrestrictedBooleanMul.N4.exists_lowProduct_rep_of_mem_rationalLow {p : ANF 8} (hp : p ∈ rationalLowSpace) : ∃ (a : F₂) (ell : LinearForm) (α : Fin 3 → F₂), p = affineANF a ell + rationalANF α

theorem UnrestrictedBooleanMul.N4.exists_targetAmbient_rep {p : ANF 8} (hp : p ∈ targetAmbient 8 (mulTarget 4)) : ∃ (u : ANF 8) (c : TargetCoeff), u ∈ affine 8 ∧ p = u + targetANF c

theorem UnrestrictedBooleanMul.N4.targetCoeff_eq_rationalCoeffRep_of_mem {c : TargetCoeff} (hc : c ∈ rationalCoeffSpace) : ∃ (α : Fin 3 → F₂), c = rationalCoeffRep α

theorem UnrestrictedBooleanMul.N4.rationalLow_mul_mem_of_mem_targetAmbient {p q : ANF 8} (hp : p ∈ rationalLowSpace) (hq : q ∈ rationalLowSpace) (hpq : p * q ∈ targetAmbient 8 (mulTarget 4)) : p * q ∈ rationalLowSpace

Actual ANF prefix closure: a product of two affine-plus-rational wires that lands back in Aff + T has no new target direction.