Rank-four support and the first Hasse jet

This file supplies the linear-algebra step used implicitly in the manuscript's first-feedback argument. The support of a two-form is the span of its eight columns. Each of the nine non-rational rank-two Hankel words has four explicitly independent columns. Consequently, if such a word is written as the sum of two decomposable forms, all four factors belong to its support.

The only finite certificates below concern the nine fixed Hankel words and their eight columns. They do not enumerate circuits or Boolean functions.

def UnrestrictedBooleanMul.N4.twoFormColumn (q : TwoForm) (j : Fin 8) : LinearForm

One column of a two-form coordinate matrix.

Equations

• UnrestrictedBooleanMul.N4.twoFormColumn q j i = q i j

def UnrestrictedBooleanMul.N4.twoFormSupport (q : TwoForm) : Submodule F₂ LinearForm

The subspace spanned by the columns of a two-form.

Equations

• UnrestrictedBooleanMul.N4.twoFormSupport q = Submodule.span UnrestrictedBooleanMul.F₂ (Set.range (UnrestrictedBooleanMul.N4.twoFormColumn q))

def UnrestrictedBooleanMul.N4.outsideSupportPivot : Fin 9 → Fin 4 → Fin 8

Four pivot columns for every non-rational rank-two Hankel word. The two infinity tangents use the last two rows and columns; all other words use the first two.

Equations

• UnrestrictedBooleanMul.N4.outsideSupportPivot = ![![0, 1, 4, 5], ![0, 1, 4, 5], ![0, 1, 4, 5], ![0, 1, 4, 5], ![2, 3, 6, 7], ![2, 3, 6, 7], ![0, 1, 4, 5], ![0, 1, 4, 5], ![0, 1, 4, 5]]

def UnrestrictedBooleanMul.N4.outsideSelectedColumn (i : Fin 9) (k : Fin 4) : LinearForm

One of four pivot columns of a non-rational rank-two target Hankel form.

Equations

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

theorem UnrestrictedBooleanMul.N4.outsideSelectedColumn_linearIndependent (i : Fin 9) : LinearIndependent F₂ (outsideSelectedColumn i)

theorem UnrestrictedBooleanMul.N4.outsideColumn_generated (i : Fin 9) (j : Fin 8) : ∃ (coeff : Fin 4 → F₂), twoFormColumn (targetTwo (outsideRankTwoWord i)) j = ∑ k : Fin 4, coeff k • outsideSelectedColumn i k

Every column is generated by the four pivots. This is a 9-by-8 matrix calculation, kept existential so no large coefficient table enters the trusted source.

theorem UnrestrictedBooleanMul.N4.outsideSupport_eq_selectedSpan (i : Fin 9) : twoFormSupport (targetTwo (outsideRankTwoWord i)) = Submodule.span F₂ (Set.range (outsideSelectedColumn i))

theorem UnrestrictedBooleanMul.N4.outsideSupport_finrank (i : Fin 9) : Module.finrank F₂ ↥(twoFormSupport (targetTwo (outsideRankTwoWord i))) = 4

def UnrestrictedBooleanMul.N4.fourVectorFamily (u z p w : LinearForm) : Fin 4 → LinearForm

The ordered family consisting of four specified linear forms.

Equations

• UnrestrictedBooleanMul.N4.fourVectorFamily u z p w = ![u, z, p, w]

def UnrestrictedBooleanMul.N4.fourVectorSpan (u z p w : LinearForm) : Submodule F₂ LinearForm

The subspace spanned by four specified linear forms.

Equations

• UnrestrictedBooleanMul.N4.fourVectorSpan u z p w = Submodule.span UnrestrictedBooleanMul.F₂ (Set.range (UnrestrictedBooleanMul.N4.fourVectorFamily u z p w))

theorem UnrestrictedBooleanMul.N4.fourVectorSpan_finrank_le (u z p w : LinearForm) : Module.finrank F₂ ↥(fourVectorSpan u z p w) ≤ 4

theorem UnrestrictedBooleanMul.N4.twoFormSupport_le_fourVectorSpan (q : TwoForm) (u z p w : LinearForm) (hq : q = vectorWedge u z + vectorWedge p w) : twoFormSupport q ≤ fourVectorSpan u z p w

theorem UnrestrictedBooleanMul.N4.decomposition_vectors_mem_outside_support (i : Fin 9) (u z p w : LinearForm) (hq : targetTwo (outsideRankTwoWord i) = vectorWedge u z + vectorWedge p w) : u ∈ twoFormSupport (targetTwo (outsideRankTwoWord i)) ∧ p ∈ twoFormSupport (targetTwo (outsideRankTwoWord i))

A rank-four two-form expressed as two wedges has all four displayed vectors in its intrinsic column support.

def UnrestrictedBooleanMul.N4.outsideTangentIndex (theta : Fin 3) (eps : F₂) : Fin 9

Locate either first-jet tangent at a rational place in the outside-target table.

Equations

• UnrestrictedBooleanMul.N4.outsideTangentIndex theta eps = ![![0, 1], ![2, 3], ![4, 5]] theta (if eps = 0 then 0 else 1)

theorem UnrestrictedBooleanMul.N4.outsideWord_tangent (theta : Fin 3) (eps : F₂) : outsideRankTwoWord (outsideTangentIndex theta eps) = rationalTangentAt theta eps

theorem UnrestrictedBooleanMul.N4.nonzero_place_vector_classifies_outside_support (theta : Fin 3) (a b : F₂) (i : Fin 9) (coeff : Fin 4 → F₂) : a ≠ 0 ∨ b ≠ 0 → quarticSupportVector theta a b = ∑ k : Fin 4, coeff k • outsideSelectedColumn i k → ∃ (eps : F₂), i = outsideTangentIndex theta eps

A nonzero vector from a rational-place plane can occur in an outside rank-two support only for one of the two tangent words at that place.

def UnrestrictedBooleanMul.N4.normalizedFirstJetVector (pa pb ja jb : F₂) : LinearForm

A vector supported on the first two coefficients of each input polynomial.

Equations

• UnrestrictedBooleanMul.N4.normalizedFirstJetVector pa pb ja jb = ![pa, ja, 0, 0, pb, jb, 0, 0]

theorem UnrestrictedBooleanMul.N4.normalizedFirstJetVector_eq (pa pb ja jb : F₂) : normalizedFirstJetVector pa pb ja jb = pa • aLinear 0 + pb • bLinear 0 + ja • aLinear 1 + jb • bLinear 1

def UnrestrictedBooleanMul.N4.InNormalizedFirstJet (theta : Fin 3) (u : LinearForm) : Prop

After place normalization, the vector has first-jet support and a nonzero jet component.

Equations

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

def UnrestrictedBooleanMul.N4.solveTangentSupportCertificate : Lean.ParserDescr

Check a fixed rational-place tangent on the sixteen coefficient vectors.

Equations

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

theorem UnrestrictedBooleanMul.N4.tangent_support_normalizes_firstJet (theta : Fin 3) (eps : F₂) (coeff : Fin 4 → F₂) : vectorWedgeTwo (∑ k : Fin 4, coeff k • outsideSelectedColumn (outsideTangentIndex theta eps) k) (rationalTwo (rationalSingleton theta)) ≠ 0 → InNormalizedFirstJet theta (∑ k : Fin 4, coeff k • outsideSelectedColumn (outsideTangentIndex theta eps) k)

The support calculation also recovers the nonzero first-jet component of the seed linear form after normalizing its rational place to zero.

theorem UnrestrictedBooleanMul.N4.rationalTwo_singleton (theta : Fin 3) : rationalTwo (rationalSingleton theta) = rationalPlaceTwo theta

theorem UnrestrictedBooleanMul.N4.same_singleton_collision_firstJet (theta : Fin 3) (N N' z w : LinearForm) (gamma : Fin 3 → F₂) (c : TargetCoeff) (hcubicNonzero : vectorWedgeTwo N (rationalTwo (rationalSingleton theta)) ≠ 0) (hsum : InPlaceSupport theta (N + N')) (htargetNonrational : ¬IsRationalCoeff c) (htarget : targetTwo c = rationalTwo gamma + vectorWedge z N + vectorWedge w N') : ∃ (eps : F₂), c + rationalCoeffRep gamma = rationalTangentAt theta eps ∧ InNormalizedFirstJet theta N

The equal-singleton branch of the low--low collision is exactly a first Hasse jet. This is the algebraic content of Proposition firstjet after the common rational place has been identified.

def UnrestrictedBooleanMul.N4.ExteriorFirstJetNormalForm : Prop

The exterior first-jet normal form with a nonzero seed cubic and a non-rational target.

Equations

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

theorem UnrestrictedBooleanMul.N4.exteriorFirstJetReducedCollision_classification {seedCoeff childCoeff rationalCoeff : Fin 3 → F₂} {seedLinear seedCompanion childLinear childCompanion : LinearForm} {targetCoeff : TargetCoeff} (hseedCoeff : seedCoeff ≠ 0) (hchildCoeff : childCoeff ≠ 0) (hcubicNonzero : vectorWedgeTwo seedLinear (rationalTwo seedCoeff) ≠ 0) (hcubic : vectorWedgeTwo seedLinear (rationalTwo seedCoeff) = vectorWedgeTwo childLinear (rationalTwo childCoeff)) (htargetNonrational : ¬IsRationalCoeff targetCoeff) (htarget : targetTwo targetCoeff = rationalTwo rationalCoeff + vectorWedge seedCompanion seedLinear + vectorWedge childCompanion childLinear) : ∃ (theta : Fin 3) (eps : F₂), seedCoeff = rationalSingleton theta ∧ childCoeff = rationalSingleton theta ∧ vectorWedgeTwo seedLinear (rationalTwo (rationalSingleton theta)) ≠ 0 ∧ targetCoeff + rationalCoeffRep rationalCoeff = rationalTangentAt theta eps ∧ InNormalizedFirstJet theta seedLinear

Classify a reduced collision without discarding its coefficient and linear witnesses.

theorem UnrestrictedBooleanMul.N4.exteriorFirstJetReducedCollision_normalForm (h : ExteriorFirstJetReducedCollision) : ExteriorFirstJetNormalForm

Circuit-independent endpoint of the first low-low feedback analysis.

theorem UnrestrictedBooleanMul.N4.NormalizedEight.exteriorFirstJetNormalForm {C : Circuit 8 8} (h : NormalizedEight C) : ExteriorFirstJetNormalForm

def UnrestrictedBooleanMul.N4.FirstJetTargetNormalForm (g target targetAffine : ANF 8) (targetCoeff : TargetCoeff) : Prop

The full ANF target normal form associated with a first-jet seed.

Equations

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

theorem UnrestrictedBooleanMul.N4.cubicLowLowNormalCollisionAt_targetNormalForm {g target targetAffine : ANF 8} {targetCoeff : TargetCoeff} (h : CubicLowLowNormalCollisionAt g target targetAffine targetCoeff) : FirstJetTargetNormalForm g target targetAffine targetCoeff

Correlated version of the first-jet theorem: the tangent classification belongs to the particular target witness appearing in the low--low collision, not merely to an unrelated existential representative.

theorem UnrestrictedBooleanMul.N4.cubicLowLowNormalCollision_targetNormalForm {g : ANF 8} (h : CubicLowLowNormalCollision g) : ∃ (target : ANF 8) (targetAffine : ANF 8) (targetCoeff : TargetCoeff), FirstJetTargetNormalForm g target targetAffine targetCoeff