Four-term Hankel target geometry

This file starts the n = 4 proof with the coordinate geometry of the seven-dimensional target of four-term multiplication. All classifications are expressed as polynomial identities over F₂; no circuit or truth-table enumeration is used.

@[reducible, inline]

abbrev UnrestrictedBooleanMul.N4.TargetCoeff : Type

Coefficient vectors for the seven Hankel target directions of Mul 4.

Equations

• UnrestrictedBooleanMul.N4.TargetCoeff = (Fin 7 → UnrestrictedBooleanMul.F₂)

noncomputable def UnrestrictedBooleanMul.N4.targetBasis (s : Fin 7) : TargetCoeff

The coefficient vector supported at one target coordinate.

Equations

• UnrestrictedBooleanMul.N4.targetBasis s = (Pi.basisFun UnrestrictedBooleanMul.F₂ (Fin 7)) s

def UnrestrictedBooleanMul.N4.rZeroCoeff : TargetCoeff

The rational place at zero.

Equations

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

def UnrestrictedBooleanMul.N4.rOneCoeff : TargetCoeff

The rational place at one.

Equations

• UnrestrictedBooleanMul.N4.rOneCoeff = ![1, 1, 1, 1, 1, 1, 1]

def UnrestrictedBooleanMul.N4.rInfinityCoeff : TargetCoeff

The rational place at infinity.

Equations

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

def UnrestrictedBooleanMul.N4.rationalCoeffSpace : Submodule F₂ TargetCoeff

The three-dimensional space spanned by the rational places.

Equations

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

noncomputable def UnrestrictedBooleanMul.N4.targetANF (c : TargetCoeff) : ANF 8

Interpret a target coefficient vector as an ANF in the Mul 4 target.

Equations

• UnrestrictedBooleanMul.N4.targetANF c = ∑ s : Fin 7, c s • UnrestrictedBooleanMul.Mul 4 s

def UnrestrictedBooleanMul.N4.hankelMatrix (c : TargetCoeff) : Matrix (Fin 4) (Fin 4) F₂

The 4 × 4 Hankel matrix attached to a target coefficient vector.

Equations

• UnrestrictedBooleanMul.N4.hankelMatrix c i j = c ⟨↑i + ↑j, ⋯⟩

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

Algebraic rank-at-most-one condition: every 2 × 2 minor vanishes.

Equations

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

theorem UnrestrictedBooleanMul.N4.targetBasis_apply (s t : Fin 7) : targetBasis s t = if s = t then 1 else 0

@[simp]

theorem UnrestrictedBooleanMul.N4.rZeroCoeff_apply (i : Fin 7) : rZeroCoeff i = if i = 0 then 1 else 0

@[simp]

theorem UnrestrictedBooleanMul.N4.rInfinityCoeff_apply (i : Fin 7) : rInfinityCoeff i = if i = 6 then 1 else 0

@[simp]

theorem UnrestrictedBooleanMul.N4.rOneCoeff_apply (i : Fin 7) : rOneCoeff i = 1

theorem UnrestrictedBooleanMul.N4.rankOne_target_classification {c : TargetCoeff} (h : HankelRankLEOne c) (hc : c ≠ 0) : c = rZeroCoeff ∨ c = rOneCoeff ∨ c = rInfinityCoeff

The nonzero rank-one Hankel coefficient vectors are precisely the three F₂-rational places. The proof follows the manuscript's recurrence argument and uses only vanishing minors and field algebra.

@[simp]

theorem UnrestrictedBooleanMul.N4.rankOne_rZero : HankelRankLEOne rZeroCoeff

@[simp]

theorem UnrestrictedBooleanMul.N4.rankOne_rOne : HankelRankLEOne rOneCoeff

@[simp]

theorem UnrestrictedBooleanMul.N4.rankOne_rInfinity : HankelRankLEOne rInfinityCoeff