ANF form of the low--low quartic exclusion

The rational--rational product may have Boolean lower-degree terms when the quartic part is nonzero. For two aligned products it is literally the same term, so it cancels before the cubic and quadratic projections are evaluated. This is the circuit-facing version of the exterior theorem.

noncomputable def UnrestrictedBooleanMul.N4.representedLowFactor (a : F₂) (ell : LinearForm) (α : Fin 3 → F₂) : ANF 8

An affine factor together with a linear combination of rational-place targets.

Equations

• UnrestrictedBooleanMul.N4.representedLowFactor a ell α = UnrestrictedBooleanMul.N4.affineANF a ell + UnrestrictedBooleanMul.N4.rationalANF α

theorem UnrestrictedBooleanMul.N4.rationalANF_add (α β : Fin 3 → F₂) : rationalANF (α + β) = rationalANF α + rationalANF β

theorem UnrestrictedBooleanMul.N4.rationalANF_smul (a : F₂) (α : Fin 3 → F₂) : rationalANF (a • α) = a • rationalANF α

theorem UnrestrictedBooleanMul.N4.alignedLowProducts_quarticProjection (a₀ b₀ a₁ b₁ : F₂) (ell₀ m₀ ell₁ m₁ : LinearForm) (α β : Fin 3 → F₂) : quarticProbeANF (representedLowFactor a₀ ell₀ α * representedLowFactor b₀ m₀ β + representedLowFactor a₁ ell₁ α * representedLowFactor b₁ m₁ β) = 0

theorem UnrestrictedBooleanMul.N4.alignedLowProducts_cubicProjection (a₀ b₀ a₁ b₁ : F₂) (ell₀ m₀ ell₁ m₁ : LinearForm) (α β : Fin 3 → F₂) : anfThreeProjection (representedLowFactor a₀ ell₀ α * representedLowFactor b₀ m₀ β + representedLowFactor a₁ ell₁ α * representedLowFactor b₁ m₁ β) = rationalProductCubic ell₀ m₀ α β + rationalProductCubic ell₁ m₁ α β

theorem UnrestrictedBooleanMul.N4.alignedLowProducts_quadraticProjection (a₀ b₀ a₁ b₁ : F₂) (ell₀ m₀ ell₁ m₁ : LinearForm) (α β : Fin 3 → F₂) : anfTwoProjection (representedLowFactor a₀ ell₀ α * representedLowFactor b₀ m₀ β + representedLowFactor a₁ ell₁ α * representedLowFactor b₁ m₁ β) = rationalProductQuadratic a₀ b₀ ell₀ m₀ α β + rationalProductQuadratic a₁ b₁ ell₁ m₁ α β

theorem UnrestrictedBooleanMul.N4.wedge_ne_zero_of_quarticProbe_ne_zero (q r : TwoForm) (h : quarticWedgeProbe q r ≠ 0) : wedgeTwo q r ≠ 0

theorem UnrestrictedBooleanMul.N4.same_rational_minors_of_probe_eq (α β γ δ : Fin 3 → F₂) (h : quarticWedgeProbe (rationalTwo α) (rationalTwo β) = quarticWedgeProbe (rationalTwo γ) (rationalTwo δ)) : SameRationalMinors α β γ δ

theorem UnrestrictedBooleanMul.N4.representedLowFactor_basis_change_first (α β γ δ : Fin 3 → F₂) (p q r s a b : F₂) (ell m : LinearForm) (hγ : γ = coeffCombination p q α β) (hδ : δ = coeffCombination r s α β) (hdet : p * s + q * r = 1) : s • representedLowFactor a ell γ + q • representedLowFactor b m δ = representedLowFactor (s * a + q * b) (changedFirstLinear s q ell m) α

theorem UnrestrictedBooleanMul.N4.representedLowFactor_basis_change_second (α β γ δ : Fin 3 → F₂) (p q r s a b : F₂) (ell m : LinearForm) (hγ : γ = coeffCombination p q α β) (hδ : δ = coeffCombination r s α β) (hdet : p * s + q * r = 1) : r • representedLowFactor a ell γ + p • representedLowFactor b m δ = representedLowFactor (r * a + p * b) (changedSecondLinear r p ell m) β

theorem UnrestrictedBooleanMul.N4.basis_changed_product_eq (u v : ANF 8) (p q r s : F₂) (hdet : p * s + q * r = 1) : (s • u + q • v) * (r • u + p • v) = u * v + (s * r) • u + (q * p) • v

theorem UnrestrictedBooleanMul.N4.representedLowFactor_mem (a : F₂) (ell : LinearForm) (α : Fin 3 → F₂) : representedLowFactor a ell α ∈ rationalLowSpace

theorem UnrestrictedBooleanMul.N4.alignedLowProducts_mem_rationalLow (a₀ b₀ a₁ b₁ : F₂) (ell₀ m₀ ell₁ m₁ : LinearForm) (α β : Fin 3 → F₂) (hquartic : quarticWedgeProbe (rationalTwo α) (rationalTwo β) ≠ 0) (hsum : representedLowFactor a₀ ell₀ α * representedLowFactor b₀ m₀ β + representedLowFactor a₁ ell₁ α * representedLowFactor b₁ m₁ β ∈ targetAmbient 8 (mulTarget 4)) : representedLowFactor a₀ ell₀ α * representedLowFactor b₀ m₀ β + representedLowFactor a₁ ell₁ α * representedLowFactor b₁ m₁ β ∈ rationalLowSpace

Two products with an aligned nonzero quartic basis cannot expose a new target quadratic direction.

theorem UnrestrictedBooleanMul.N4.add_mem_targetAmbient_of_mem_rationalLow {x y : ANF 8} (hx : x ∈ targetAmbient 8 (mulTarget 4)) (hy : y ∈ rationalLowSpace) : x + y ∈ targetAmbient 8 (mulTarget 4)

Adding a rational-low correction preserves the target ambient space. Keeping this elementary submodule step opaque prevents the elaborator from repeatedly unfolding the represented low factors in the basis-change argument below.

theorem UnrestrictedBooleanMul.N4.lowLowProducts_mem_rationalLow_of_quartic_nonzero (a₀ b₀ a₁ b₁ : F₂) (ell₀ m₀ ell₁ m₁ : LinearForm) (α β γ δ : Fin 3 → F₂) (hquartic : quarticWedgeProbe (rationalTwo α) (rationalTwo β) ≠ 0) (hsum : representedLowFactor a₀ ell₀ α * representedLowFactor b₀ m₀ β + representedLowFactor a₁ ell₁ γ * representedLowFactor b₁ m₁ δ ∈ targetAmbient 8 (mulTarget 4)) : representedLowFactor a₀ ell₀ α * representedLowFactor b₀ m₀ β + representedLowFactor a₁ ell₁ γ * representedLowFactor b₁ m₁ δ ∈ rationalLowSpace

Complete ANF low--low quartic collision, including algebraic basis alignment.