Quartic separation for every pair of rational-place supports

There are only three unordered pairs of rational places. The first pair is certified in QuarticCoordinates; the packed rows below certify the other two. This lets the low--low proof select a nonzero 2 × 2 coefficient minor directly, without formalizing a separate PGL₂(F₂) action.

def UnrestrictedBooleanMul.N4.quarticZeroInfinitySeparators (i : Fin 144) : ℕ

Packed separating covectors for the rational places at zero and infinity.

Equations

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

def UnrestrictedBooleanMul.N4.quarticOneInfinitySeparators (i : Fin 144) : ℕ

Packed separating covectors for the rational places at one and infinity.

Equations

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

def UnrestrictedBooleanMul.N4.quarticOtherPairSeparatorTable (i : Fin 288) : ℕ

The two remaining support-pair tables, stored as bounded blocks.

Equations

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

def UnrestrictedBooleanMul.N4.quarticSupportPair : Fin 3 → Fin 3 × Fin 3

Pair zero is (P₁,P₀), pair one (P₀,P∞), and pair two (P₁,P∞).

Equations

• UnrestrictedBooleanMul.N4.quarticSupportPair = ![(1, 0), (0, 2), (1, 2)]

def UnrestrictedBooleanMul.N4.quarticSupportVector (theta : Fin 3) (a b : F₂) : LinearForm

A vector in the two-input support of a chosen rational place.

Equations

• UnrestrictedBooleanMul.N4.quarticSupportVector theta a b = a • UnrestrictedBooleanMul.N4.placeA theta + b • UnrestrictedBooleanMul.N4.placeB theta

def UnrestrictedBooleanMul.N4.quarticPairSeparatorRow (pair : Fin 3) (index : Fin 144) : ℕ

Select a packed separating covector for one of the three rational-place pairs.

Equations

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

def UnrestrictedBooleanMul.N4.quarticPairSeparatorBit (pair : Fin 3) (a b c d : F₂) (i : Fin 9) (k : Fin 28) : F₂

Extract a coefficient of the covector separating a target from a support pair.

Equations

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

def UnrestrictedBooleanMul.N4.quarticPairSeparatorLinear (pair : Fin 3) (a b c d : F₂) (i : Fin 9) : TwoForm →ₗ[F₂] F₂

The separating linear functional for a rational-place pair and its support parameters.

Equations

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

theorem UnrestrictedBooleanMul.N4.quarticPairSeparator_target_check (pair : Fin 3) (a b c d : F₂) (i : Fin 9) : (quarticPairSeparatorLinear pair a b c d i) (targetTwo (outsideRankTwoWord i)) = 1

theorem UnrestrictedBooleanMul.N4.quarticPairSeparator_first_basis_check (pair : Fin 3) (a b c d : F₂) (i : Fin 9) (j : Fin 8) : (quarticPairSeparatorLinear pair a b c d i) (vectorWedge (quarticSupportVector (quarticSupportPair pair).1 a b) (coordinateLinear j)) = 0

theorem UnrestrictedBooleanMul.N4.quarticPairSeparator_second_basis_check (pair : Fin 3) (a b c d : F₂) (i : Fin 9) (j : Fin 8) : (quarticPairSeparatorLinear pair a b c d i) (vectorWedge (quarticSupportVector (quarticSupportPair pair).2 c d) (coordinateLinear j)) = 0

theorem UnrestrictedBooleanMul.N4.quarticPairSeparator_first (pair : Fin 3) (a b c d : F₂) (i : Fin 9) (z : LinearForm) : (quarticPairSeparatorLinear pair a b c d i) (vectorWedge (quarticSupportVector (quarticSupportPair pair).1 a b) z) = 0

theorem UnrestrictedBooleanMul.N4.quarticPairSeparator_second (pair : Fin 3) (a b c d : F₂) (i : Fin 9) (z : LinearForm) : (quarticPairSeparatorLinear pair a b c d i) (vectorWedge (quarticSupportVector (quarticSupportPair pair).2 c d) z) = 0

theorem UnrestrictedBooleanMul.N4.outsideRankTwo_not_supportPair_wedges (pair : Fin 3) (a b c d : F₂) (i : Fin 9) (z w : LinearForm) : targetTwo (outsideRankTwoWord i) ≠ vectorWedge (quarticSupportVector (quarticSupportPair pair).1 a b) z + vectorWedge (quarticSupportVector (quarticSupportPair pair).2 c d) w

theorem UnrestrictedBooleanMul.N4.target_eq_rational_add_supportPair_is_rational (t : TargetCoeff) (gamma : Fin 3 → F₂) (pair : Fin 3) (a b c d : F₂) (z w : LinearForm) (h : targetTwo t = rationalTwo gamma + vectorWedge (quarticSupportVector (quarticSupportPair pair).1 a b) z + vectorWedge (quarticSupportVector (quarticSupportPair pair).2 c d) w) : IsRationalCoeff t