Cubic seed normal form

This file formalizes the exterior-algebra core of the manuscript's low-product normal form. It is deliberately independent of circuit syntax: two rational-place quadratic parts with vanishing quartic wedge share one quadratic direction, and the remaining cubic is a single vector wedged with that direction.

@[simp]

theorem UnrestrictedBooleanMul.N4.vectorWedge_self (x : LinearForm) : vectorWedge x x = 0

theorem UnrestrictedBooleanMul.N4.vectorWedge_comm (x y : LinearForm) : vectorWedge x y = vectorWedge y x

theorem UnrestrictedBooleanMul.N4.vectorWedgeTwo_add_left (x y : LinearForm) (q : TwoForm) : vectorWedgeTwo (x + y) q = vectorWedgeTwo x q + vectorWedgeTwo y q

theorem UnrestrictedBooleanMul.N4.vectorWedgeTwo_zero_left (q : TwoForm) : vectorWedgeTwo 0 q = 0

theorem UnrestrictedBooleanMul.N4.vectorWedgeTwo_zero_right (x : LinearForm) : vectorWedgeTwo x 0 = 0

theorem UnrestrictedBooleanMul.N4.rationalTwo_zero : rationalTwo 0 = 0

theorem UnrestrictedBooleanMul.N4.vectorWedge_add_right (x y z : LinearForm) : vectorWedge x (y + z) = vectorWedge x y + vectorWedge x z

def UnrestrictedBooleanMul.N4.rationalProductCubic (ell m : LinearForm) (α β : Fin 3 → F₂) : ThreeForm

Cubic high part of a product whose linear factors are ell,m and whose quadratic factors have rational-place coefficient words α,β.

Equations

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

def UnrestrictedBooleanMul.N4.booleanContraction (ell : LinearForm) (q : TwoForm) : TwoForm

Boolean degree-lowering contraction: the quadratic part created when a linear form multiplies a quadratic form and repeats one of its variables.

Equations

• UnrestrictedBooleanMul.N4.booleanContraction ell q i j = (ell i + ell j) * q i j

def UnrestrictedBooleanMul.N4.twoHadamard (q c : TwoForm) : TwoForm

Quadratic terms created by multiplying identical quadratic monomials.

Equations

• UnrestrictedBooleanMul.N4.twoHadamard q c i j = q i j * c i j

theorem UnrestrictedBooleanMul.N4.booleanContraction_rationalPlace (a b : F₂) (θ : Fin 3) : booleanContraction (a • placeA θ + b • placeB θ) (rationalPlaceTwo θ) = (a + b) • rationalPlaceTwo θ

Boolean contraction along a rational-place support only rescales that place. The two support vectors use disjoint A and B coordinates.

def UnrestrictedBooleanMul.N4.rationalProductQuadratic (a b : F₂) (ell m : LinearForm) (α β : Fin 3 → F₂) : TwoForm

Complete quadratic shadow of a product (a + ell + Q) * (b + m + C).

Equations

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

theorem UnrestrictedBooleanMul.N4.low_product_normal_form_exterior (ell m : LinearForm) (α β : Fin 3 → F₂) (hquartic : wedgeTwo (rationalTwo α) (rationalTwo β) = 0) (hcubic : rationalProductCubic ell m α β ≠ 0) : ∃ (γ : Fin 3 → F₂) (N : LinearForm) (z : LinearForm), γ ≠ 0 ∧ rationalProductCubic ell m α β = vectorWedgeTwo N (rationalTwo γ) ∧ vectorWedge ell m = vectorWedge z N

Exterior low-product normal form. The equality wedgeTwo Q C = 0 forces the two rational coefficient vectors to be dependent. The three possible dependencies over F₂ give the normal form directly.

theorem UnrestrictedBooleanMul.N4.low_product_quadratic_normal_form (a b : F₂) (ell m : LinearForm) (α β : Fin 3 → F₂) (hquartic : wedgeTwo (rationalTwo α) (rationalTwo β) = 0) (hcubic : rationalProductCubic ell m α β ≠ 0) : ∃ (γ : Fin 3 → F₂) (N : LinearForm) (z : LinearForm) (ρ : F₂), γ ≠ 0 ∧ rationalProductCubic ell m α β = vectorWedgeTwo N (rationalTwo γ) ∧ rationalProductQuadratic a b ell m α β = ρ • rationalTwo γ + vectorWedge z N + booleanContraction N (rationalTwo γ)

The quadratic companion to low_product_normal_form_exterior, including the Boolean contraction κ_G(N). The remaining scalar multiple of G lies in the rational target space.

theorem UnrestrictedBooleanMul.N4.low_product_quadratic_normal_form_weak (a b : F₂) (ell m : LinearForm) (α β : Fin 3 → F₂) (hquartic : wedgeTwo (rationalTwo α) (rationalTwo β) = 0) : ∃ (γ : Fin 3 → F₂) (N : LinearForm) (z : LinearForm) (ρ : F₂), rationalProductCubic ell m α β = vectorWedgeTwo N (rationalTwo γ) ∧ rationalProductQuadratic a b ell m α β = ρ • rationalTwo γ + vectorWedge z N + booleanContraction N (rationalTwo γ)

The same companion normal form without assuming the cubic part is nonzero. This is the form used by prefix rigidity.

def UnrestrictedBooleanMul.N4.targetAnnihilatorMap (h : ThreeForm) : TargetCoeff →ₗ[F₂] FiveForm

Cubic target-annihilator map in the concrete exterior coordinates.

Equations

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

def UnrestrictedBooleanMul.N4.targetAnnihilator (h : ThreeForm) : Submodule F₂ TargetCoeff

Target coefficient vectors whose two-form wedges to zero with the given three-form.

Equations

• UnrestrictedBooleanMul.N4.targetAnnihilator h = (UnrestrictedBooleanMul.N4.targetAnnihilatorMap h).ker

theorem UnrestrictedBooleanMul.N4.mem_targetAnnihilator_iff (h : ThreeForm) (c : TargetCoeff) : c ∈ targetAnnihilator h ↔ wedgeThreeTwo h (targetTwo c) = 0

theorem UnrestrictedBooleanMul.N4.zero_anchor_wedge_firstJet : wedgeTwo zeroPlaceTwo zeroFirstJetTwo = 0

The anchor and its first Hasse jet always annihilate a cubic anchored at the rational place zero. This is the algebraic source of the baseline two-dimensional annihilator in the manuscript.

theorem UnrestrictedBooleanMul.N4.targetBasis_zero_mem_anchoredAnnihilator (M : LinearForm) : targetBasis 0 ∈ targetAnnihilator (vectorWedgeTwo M (rationalPlaceTwo 0))

theorem UnrestrictedBooleanMul.N4.targetBasis_one_mem_anchoredAnnihilator (M : LinearForm) : targetBasis 1 ∈ targetAnnihilator (vectorWedgeTwo M (rationalPlaceTwo 0))

def UnrestrictedBooleanMul.N4.zeroFirstJetCoeffSpace : Submodule F₂ TargetCoeff

The plane spanned by the constant and first product coefficients.

Equations

• UnrestrictedBooleanMul.N4.zeroFirstJetCoeffSpace = Submodule.span UnrestrictedBooleanMul.F₂ (Set.range ![UnrestrictedBooleanMul.N4.targetBasis 0, UnrestrictedBooleanMul.N4.targetBasis 1])

theorem UnrestrictedBooleanMul.N4.zeroFirstJetCoeffSpace_le_anchoredAnnihilator (M : LinearForm) : zeroFirstJetCoeffSpace ≤ targetAnnihilator (vectorWedgeTwo M (rationalPlaceTwo 0))

theorem UnrestrictedBooleanMul.N4.zeroFirstJetCoeff_linearIndependent : LinearIndependent F₂ ![targetBasis 0, targetBasis 1]

theorem UnrestrictedBooleanMul.N4.zeroFirstJetCoeffSpace_finrank : Module.finrank F₂ ↥zeroFirstJetCoeffSpace = 2

theorem UnrestrictedBooleanMul.N4.anchoredAnnihilator_finrank_ge_two (M : LinearForm) : 2 ≤ Module.finrank F₂ ↥(targetAnnihilator (vectorWedgeTwo M (rationalPlaceTwo 0)))