Quartic low--low coordinate separation

This is the finite linear certificate behind the low--low half of quartic exclusion. For x in the rational-place support P₁ and y in P₀, none of the nine rank-two target forms outside the rational-place space lies in x ∧ L + y ∧ L. The table below stores one separating linear functional for each of the 16 × 9 cases. Lean checks the functionals on the eight coordinate vectors; arbitrary vectors then follow by linearity.

Thus the certificate is a small algebraic matrix check, not an enumeration of circuits or Boolean functions.

def UnrestrictedBooleanMul.N4.upperPair : Fin 28 → Fin 8 × Fin 8

The 28 upper-triangular coordinate pairs of an alternating 8 × 8 matrix.

Equations

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

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

Packed separating covectors. The flat index order is (P₁-A coefficient, P₁-B coefficient, P₀-A coefficient, P₀-B coefficient, outside-word index).

Equations

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

def UnrestrictedBooleanMul.N4.f2IndexBit (a : F₂) : ℕ

Encode a field element as the natural number zero or one.

Equations

• UnrestrictedBooleanMul.N4.f2IndexBit a = if a = 0 then 0 else 1

def UnrestrictedBooleanMul.N4.quarticSeparatorIndex (a b c d : F₂) (i : Fin 9) : Fin 144

Pack four Boolean parameters and an outside-target index into a table row.

Equations

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

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

Extract one coefficient of the packed quartic separating covector.

Equations

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

def UnrestrictedBooleanMul.N4.twoFormCoordinate (i j : Fin 8) : TwoForm →ₗ[F₂] F₂

Extract one coordinate from a two-form coordinate array.

Equations

• UnrestrictedBooleanMul.N4.twoFormCoordinate i j = { toFun := fun (q : UnrestrictedBooleanMul.N4.TwoForm) => q i j, map_add' := ⋯, map_smul' := ⋯ }

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

The linear functional encoded by a quartic separating table row.

Equations

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

def UnrestrictedBooleanMul.N4.quarticSeparatorEval (a b c d : F₂) (i : Fin 9) (q : TwoForm) : F₂

Evaluate a quartic separating covector on a two-form.

Equations

• UnrestrictedBooleanMul.N4.quarticSeparatorEval a b c d i q = (UnrestrictedBooleanMul.N4.quarticSeparatorLinear a b c d i) q

def UnrestrictedBooleanMul.N4.quarticPoneVector (a b : F₂) : LinearForm

A vector in the two-dimensional input support at the place one.

Equations

• UnrestrictedBooleanMul.N4.quarticPoneVector a b = a • UnrestrictedBooleanMul.N4.placeA 1 + b • UnrestrictedBooleanMul.N4.placeB 1

def UnrestrictedBooleanMul.N4.quarticPzeroVector (c d : F₂) : LinearForm

A vector in the two-dimensional input support at the place zero.

Equations

• UnrestrictedBooleanMul.N4.quarticPzeroVector c d = c • UnrestrictedBooleanMul.N4.placeA 0 + d • UnrestrictedBooleanMul.N4.placeB 0

theorem UnrestrictedBooleanMul.N4.quarticSeparator_target_check (a b c d : F₂) (i : Fin 9) : (quarticSeparatorLinear a b c d i) (targetTwo (outsideRankTwoWord i)) = 1

theorem UnrestrictedBooleanMul.N4.quarticSeparator_pone_basis_check (a b c d : F₂) (i : Fin 9) (j : Fin 8) : (quarticSeparatorLinear a b c d i) (vectorWedge (quarticPoneVector a b) (coordinateLinear j)) = 0

theorem UnrestrictedBooleanMul.N4.quarticSeparator_pzero_basis_check (a b c d : F₂) (i : Fin 9) (j : Fin 8) : (quarticSeparatorLinear a b c d i) (vectorWedge (quarticPzeroVector c d) (coordinateLinear j)) = 0

theorem UnrestrictedBooleanMul.N4.quarticSeparator_pone (a b c d : F₂) (i : Fin 9) (z : LinearForm) : (quarticSeparatorLinear a b c d i) (vectorWedge (quarticPoneVector a b) z) = 0

theorem UnrestrictedBooleanMul.N4.quarticSeparator_pzero (a b c d : F₂) (i : Fin 9) (z : LinearForm) : (quarticSeparatorLinear a b c d i) (vectorWedge (quarticPzeroVector c d) z) = 0

theorem UnrestrictedBooleanMul.N4.outsideRankTwo_not_pone_pzero_wedges (a b c d : F₂) (i : Fin 9) (z w : LinearForm) : targetTwo (outsideRankTwoWord i) ≠ vectorWedge (quarticPoneVector a b) z + vectorWedge (quarticPzeroVector c d) w

The certified low--low separation statement in coordinate form.

theorem UnrestrictedBooleanMul.N4.rationalCoeffRep_add (u v : Fin 3 → F₂) : rationalCoeffRep (u + v) = rationalCoeffRep u + rationalCoeffRep v

theorem UnrestrictedBooleanMul.N4.target_eq_rational_add_pone_pzero_is_rational (t : TargetCoeff) (gamma : Fin 3 → F₂) (a b c d : F₂) (z w : LinearForm) (h : targetTwo t = rationalTwo gamma + vectorWedge (quarticPoneVector a b) z + vectorWedge (quarticPzeroVector c d) w) : IsRationalCoeff t

In the first quartic orbit, adding a form from P₁ ∧ L + P₀ ∧ L to a rational target form cannot expose a new target direction. The other two manuscript orbits are special cases obtained by setting the P₁ or both support vectors to zero.

theorem UnrestrictedBooleanMul.N4.quartic_cubic_kernel_zero_one (x y : LinearForm) (h : vectorWedgeTwo x (rationalPlaceTwo 1) + vectorWedgeTwo y (rationalPlaceTwo 0) = 0) : ∃ (a : F₂) (b : F₂) (c : F₂) (d : F₂), x = quarticPoneVector a b ∧ y = quarticPzeroVector c d

The direct-sum cubic comparison for the representative quartic plane span(r₀,r₁): cancellation forces the two linear differences into the opposite rational-place support planes.

def UnrestrictedBooleanMul.N4.zeroPlaceCoeff3 : Fin 3 → F₂

Select evaluation at zero among the three rational-place coordinates.

Equations

• UnrestrictedBooleanMul.N4.zeroPlaceCoeff3 = ![1, 0, 0]

def UnrestrictedBooleanMul.N4.onePlaceCoeff3 : Fin 3 → F₂

Select evaluation at one among the three rational-place coordinates.

Equations

• UnrestrictedBooleanMul.N4.onePlaceCoeff3 = ![0, 1, 0]

@[simp]

theorem UnrestrictedBooleanMul.N4.rationalTwo_zeroPlaceCoeff3 : rationalTwo zeroPlaceCoeff3 = rationalPlaceTwo 0

@[simp]

theorem UnrestrictedBooleanMul.N4.rationalTwo_onePlaceCoeff3 : rationalTwo onePlaceCoeff3 = rationalPlaceTwo 1

theorem UnrestrictedBooleanMul.N4.exists_rationalTwo_of_mem {q : TwoForm} (hq : q ∈ rationalPlaceTwoSpace) : ∃ (gamma : Fin 3 → F₂), q = rationalTwo gamma

theorem UnrestrictedBooleanMul.N4.aligned_zero_one_lowLow_target_is_rational (a₀ b₀ a₁ b₁ : F₂) (ell₀ m₀ ell₁ m₁ : LinearForm) (t : TargetCoeff) (hcubic : rationalProductCubic ell₀ m₀ zeroPlaceCoeff3 onePlaceCoeff3 = rationalProductCubic ell₁ m₁ zeroPlaceCoeff3 onePlaceCoeff3) (hquadratic : targetTwo t = rationalProductQuadratic a₀ b₀ ell₀ m₀ zeroPlaceCoeff3 onePlaceCoeff3 + rationalProductQuadratic a₁ b₁ ell₁ m₁ zeroPlaceCoeff3 onePlaceCoeff3) : IsRationalCoeff t

Low--low quartic collision for the representative plane span(r₀,r₁). Equal cubic highs force the linear differences into P₁ and P₀; the certified separation lemma then sends every target quadratic difference back to the rational-place span.