Decomposable target geometry

This file connects products of linear forms to the Hankel classification. The key argument is symbolic: the absence of A ∧ A terms makes the two A-side vectors dependent, so the cross block is an outer product and every Hankel minor vanishes.

def UnrestrictedBooleanMul.N4.aCoord (i : Fin 4) : Fin 8

Coordinate of an input coefficient in the first polynomial.

Equations

• UnrestrictedBooleanMul.N4.aCoord i = ⟨↑i, ⋯⟩

def UnrestrictedBooleanMul.N4.bCoord (j : Fin 4) : Fin 8

Coordinate of an input coefficient in the second polynomial.

Equations

• UnrestrictedBooleanMul.N4.bCoord j = ⟨4 + ↑j, ⋯⟩

def UnrestrictedBooleanMul.N4.aPart (u : LinearForm) : Fin 4 → F₂

Restrict a linear form to the first polynomial input.

Equations

• UnrestrictedBooleanMul.N4.aPart u i = u (UnrestrictedBooleanMul.N4.aCoord i)

def UnrestrictedBooleanMul.N4.bPart (u : LinearForm) : Fin 4 → F₂

Restrict a linear form to the second polynomial input.

Equations

• UnrestrictedBooleanMul.N4.bPart u j = u (UnrestrictedBooleanMul.N4.bCoord j)

def UnrestrictedBooleanMul.N4.crossPart (u v : LinearForm) (i j : Fin 4) : F₂

The mixed input coordinates of the exterior product of two linear forms.

Equations

• UnrestrictedBooleanMul.N4.crossPart u v i j = UnrestrictedBooleanMul.N4.vectorWedge u v (UnrestrictedBooleanMul.N4.aCoord i) (UnrestrictedBooleanMul.N4.bCoord j)

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

A target coefficient word is decomposable when it is the quadratic cross part of two linear forms and their same-side exterior components vanish.

Equations

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

theorem UnrestrictedBooleanMul.N4.decomposableTarget_rankOne {c : TargetCoeff} (h : IsDecomposableTarget c) : HankelRankLEOne c

A decomposable target has Hankel rank at most one.

theorem UnrestrictedBooleanMul.N4.decomposableTarget_classification {c : TargetCoeff} (hdec : IsDecomposableTarget c) (hc : c ≠ 0) : c = rZeroCoeff ∨ c = rOneCoeff ∨ c = rInfinityCoeff

Rank-one target geometry in the form consumed by the prefix theorem.

def UnrestrictedBooleanMul.N4.rationalCoeffRep (α : Fin 3 → F₂) : TargetCoeff

Represent a linear combination of evaluations at zero, one, and infinity.

Equations

• UnrestrictedBooleanMul.N4.rationalCoeffRep α = α 0 • UnrestrictedBooleanMul.N4.rZeroCoeff + α 1 • UnrestrictedBooleanMul.N4.rOneCoeff + α 2 • UnrestrictedBooleanMul.N4.rInfinityCoeff

theorem UnrestrictedBooleanMul.N4.rationalCoeffRep_mem (α : Fin 3 → F₂) : rationalCoeffRep α ∈ rationalCoeffSpace

theorem UnrestrictedBooleanMul.N4.rationalCoeffRep_injective : Function.Injective rationalCoeffRep

theorem UnrestrictedBooleanMul.N4.IsRationalCoeff_iff (c : TargetCoeff) : IsRationalCoeff c ↔ ∃ (α : Fin 3 → F₂), c = rationalCoeffRep α