Orbit-free low--low quartic exclusion

For independent rational coefficient words α, β, choose a nonzero 2 × 2 minor. The corresponding two direct cubic components reconstruct the two linear differences. Their quadratic wedge shadow therefore lies in one of the three support-pair spaces certified in QuarticAllPairs.

def UnrestrictedBooleanMul.N4.rationalCoeffMinor (α β : Fin 3 → F₂) (i j : Fin 3) : F₂

A two-by-two minor of two rational coefficient vectors.

Equations

• UnrestrictedBooleanMul.N4.rationalCoeffMinor α β i j = α i * β j + α j * β i

@[simp]

theorem UnrestrictedBooleanMul.N4.f2_mul_self_quartic (u : F₂) : u * u = u

theorem UnrestrictedBooleanMul.N4.exists_supportPair_minor_one (α β : Fin 3 → F₂) (hα : α ≠ 0) (hβ : β ≠ 0) (hαβ : α ≠ β) : ∃ (pair : Fin 3), rationalCoeffMinor α β (quarticSupportPair pair).1 (quarticSupportPair pair).2 = 1

theorem UnrestrictedBooleanMul.N4.rational_coeff_independent_of_wedge_ne_zero (α β : Fin 3 → F₂) (h : wedgeTwo (rationalTwo α) (rationalTwo β) ≠ 0) : α ≠ 0 ∧ β ≠ 0 ∧ α ≠ β

def UnrestrictedBooleanMul.N4.cubicDifferenceInput (α β : Fin 3 → F₂) (x y : LinearForm) : Fin 3 → LinearForm

The placewise linear inputs expressing a cubic difference as a direct sum.

Equations

• UnrestrictedBooleanMul.N4.cubicDifferenceInput α β x y theta = β theta • x + α theta • y

theorem UnrestrictedBooleanMul.N4.cubicDifference_directSum (α β : Fin 3 → F₂) (x y : LinearForm) : rationalCubicDirectSum (cubicDifferenceInput α β x y) = vectorWedgeTwo x (rationalTwo β) + vectorWedgeTwo y (rationalTwo α)

theorem UnrestrictedBooleanMul.N4.reconstruct_first_from_minor (α β : Fin 3 → F₂) (x y : LinearForm) (i j : Fin 3) (hminor : rationalCoeffMinor α β i j = 1) : x = α j • cubicDifferenceInput α β x y i + α i • cubicDifferenceInput α β x y j

theorem UnrestrictedBooleanMul.N4.reconstruct_second_from_minor (α β : Fin 3 → F₂) (x y : LinearForm) (i j : Fin 3) (hminor : rationalCoeffMinor α β i j = 1) : y = β j • cubicDifferenceInput α β x y i + β i • cubicDifferenceInput α β x y j

def UnrestrictedBooleanMul.N4.singlePlaceCoeff3 (theta : Fin 3) : Fin 3 → F₂

A rational-place coefficient vector supported at one place.

Equations

• UnrestrictedBooleanMul.N4.singlePlaceCoeff3 theta phi = if phi = theta then 1 else 0

@[simp]

theorem UnrestrictedBooleanMul.N4.rationalTwo_singlePlaceCoeff3 (theta : Fin 3) : rationalTwo (singlePlaceCoeff3 theta) = rationalPlaceTwo theta

theorem UnrestrictedBooleanMul.N4.cubicDifference_contraction_sum (α β : Fin 3 → F₂) (x y : LinearForm) : booleanContraction x (rationalTwo β) + booleanContraction y (rationalTwo α) = ∑ theta : Fin 3, booleanContraction (cubicDifferenceInput α β x y theta) (rationalPlaceTwo theta)

theorem UnrestrictedBooleanMul.N4.cubicDifference_contraction_mem (α β : Fin 3 → F₂) (x y : LinearForm) (hkernel : rationalCubicDirectSum (cubicDifferenceInput α β x y) = 0) : booleanContraction x (rationalTwo β) + booleanContraction y (rationalTwo α) ∈ rationalPlaceTwoSpace

theorem UnrestrictedBooleanMul.N4.aligned_lowLow_quartic_target_is_rational (α β : Fin 3 → F₂) (a₀ b₀ a₁ b₁ : F₂) (ell₀ m₀ ell₁ m₁ : LinearForm) (t : TargetCoeff) (hquartic : wedgeTwo (rationalTwo α) (rationalTwo β) ≠ 0) (hcubic : rationalProductCubic ell₀ m₀ α β = rationalProductCubic ell₁ m₁ α β) (hquadratic : targetTwo t = rationalProductQuadratic a₀ b₀ ell₀ m₀ α β + rationalProductQuadratic a₁ b₁ ell₁ m₁ α β) : IsRationalCoeff t

The complete aligned low--low quartic collision theorem, with no orbit case split.

theorem UnrestrictedBooleanMul.N4.aligned_lowLow_quartic_target_is_rational_add_rational (α β eta : Fin 3 → F₂) (a₀ b₀ a₁ b₁ : F₂) (ell₀ m₀ ell₁ m₁ : LinearForm) (t : TargetCoeff) (hquartic : wedgeTwo (rationalTwo α) (rationalTwo β) ≠ 0) (hcubic : rationalProductCubic ell₀ m₀ α β = rationalProductCubic ell₁ m₁ α β) (hquadratic : targetTwo t = rationalTwo eta + rationalProductQuadratic a₀ b₀ ell₀ m₀ α β + rationalProductQuadratic a₁ b₁ ell₁ m₁ α β) : IsRationalCoeff t

A rational quadratic offset does not affect the aligned collision conclusion.