Rational and degree-two places

The 4 × 4 Hankel rank-two classification is intentionally concrete. It is a closed calculation on 128 coefficient vectors and 16 cubic minors, not a search over circuits. Subsequent proofs consume the named rational, tangent, and degree-two-place families rather than raw bit patterns.

def UnrestrictedBooleanMul.N4.detThree (M : Matrix (Fin 3) (Fin 3) F₂) : F₂

Determinant of a 3 × 3 matrix in characteristic two.

Equations

• UnrestrictedBooleanMul.N4.detThree M = M 0 0 * M 1 1 * M 2 2 + M 0 0 * M 1 2 * M 2 1 + M 0 1 * M 1 0 * M 2 2 + M 0 1 * M 1 2 * M 2 0 + M 0 2 * M 1 0 * M 2 1 + M 0 2 * M 1 1 * M 2 0

def UnrestrictedBooleanMul.N4.hankelMinorThree (c : TargetCoeff) (dropRow dropCol : Fin 4) : F₂

A cubic minor obtained by deleting one row and one column.

Equations

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

def UnrestrictedBooleanMul.N4.HankelRankLETwo (c : TargetCoeff) : Prop

Algebraic rank-at-most-two condition: all 3 × 3 minors vanish.

Equations

• UnrestrictedBooleanMul.N4.HankelRankLETwo c = ∀ (dropRow dropCol : Fin 4), UnrestrictedBooleanMul.N4.hankelMinorThree c dropRow dropCol = 0

@[instance_reducible]

instance UnrestrictedBooleanMul.N4.instDecidableHankelRankLETwo (c : TargetCoeff) : Decidable (HankelRankLETwo c)

Equations

• UnrestrictedBooleanMul.N4.instDecidableHankelRankLETwo c = id inferInstance

def UnrestrictedBooleanMul.N4.rankTwoWord : Fin 16 → TargetCoeff

The sixteen coefficient words in the manuscript's rank-at-most-two table, including zero.

Equations

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

theorem UnrestrictedBooleanMul.N4.rankTwo_target_classification (c : TargetCoeff) : HankelRankLETwo c ↔ ∃ (i : Fin 16), c = rankTwoWord i

Complete binary rank-two Hankel classification.

def UnrestrictedBooleanMul.N4.IsRationalCoeff (c : TargetCoeff) : Prop

Direct algebraic description of the rational-place span.

Equations

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

@[instance_reducible]

instance UnrestrictedBooleanMul.N4.instDecidableIsRationalCoeff (c : TargetCoeff) : Decidable (IsRationalCoeff c)

Equations

• UnrestrictedBooleanMul.N4.instDecidableIsRationalCoeff c = Fintype.decidableExistsFintype

def UnrestrictedBooleanMul.N4.outsideRankTwoWord : Fin 9 → TargetCoeff

Six tangent words followed by the three nonzero degree-two-place words.

Equations

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

theorem UnrestrictedBooleanMul.N4.outside_rankTwo_classification (c : TargetCoeff) : HankelRankLETwo c ∧ c ≠ 0 ∧ ¬IsRationalCoeff c ↔ ∃ (i : Fin 9), c = outsideRankTwoWord i

Every nonzero rank-at-most-two target outside the rational-place span is one of the six rational tangents or one of the three degree-two-place forms.

def UnrestrictedBooleanMul.N4.degreeTwoPlaceBasis : Fin 2 → TargetCoeff

The two-dimensional closed degree-two place.

Equations

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

def UnrestrictedBooleanMul.N4.degreeTwoCoeffSpace : Submodule F₂ TargetCoeff

The target coefficient space of the irreducible quadratic place.

Equations

• UnrestrictedBooleanMul.N4.degreeTwoCoeffSpace = Submodule.span UnrestrictedBooleanMul.F₂ (Set.range UnrestrictedBooleanMul.N4.degreeTwoPlaceBasis)

def UnrestrictedBooleanMul.N4.tangentWord : Fin 6 → TargetCoeff

The first Hasse-jet direction at each rational place, with its translate by the place itself.

Equations

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

theorem UnrestrictedBooleanMul.N4.degreeTwoPlace_linearIndependent : LinearIndependent F₂ degreeTwoPlaceBasis

theorem UnrestrictedBooleanMul.N4.degreeTwoCoeffSpace_finrank : Module.finrank F₂ ↥degreeTwoCoeffSpace = 2

theorem UnrestrictedBooleanMul.N4.rationalCoeffSpace_eq : rationalCoeffSpace = Submodule.span F₂ (Set.range ![rZeroCoeff, rOneCoeff, rInfinityCoeff])