Target alternating two-forms

The quadratic target is represented as the alternating 8 × 8 matrix with the 4 × 4 Hankel matrix in its two cross blocks. This small coordinate layer is shared by the quadratic lower bound and the cubic annihilator.

noncomputable def UnrestrictedBooleanMul.N4.aLinear (i : Fin 4) : LinearForm

Coordinate linear forms on the two four-dimensional input blocks.

Equations

• UnrestrictedBooleanMul.N4.aLinear i = (Pi.basisFun UnrestrictedBooleanMul.F₂ (Fin 8)) (UnrestrictedBooleanMul.N4.aCoord i)

noncomputable def UnrestrictedBooleanMul.N4.bLinear (i : Fin 4) : LinearForm

The linear form selecting one coefficient of the second input polynomial.

Equations

• UnrestrictedBooleanMul.N4.bLinear i = (Pi.basisFun UnrestrictedBooleanMul.F₂ (Fin 8)) (UnrestrictedBooleanMul.N4.bCoord i)

noncomputable def UnrestrictedBooleanMul.N4.zeroPlaceTwo : TwoForm

The first three Hasse coefficients at the rational place zero.

Equations

• UnrestrictedBooleanMul.N4.zeroPlaceTwo = UnrestrictedBooleanMul.N4.vectorWedge (UnrestrictedBooleanMul.N4.aLinear 0) (UnrestrictedBooleanMul.N4.bLinear 0)

noncomputable def UnrestrictedBooleanMul.N4.zeroFirstJetTwo : TwoForm

The two-form of the first Hasse coefficient at zero.

Equations

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

noncomputable def UnrestrictedBooleanMul.N4.zeroSecondJetTwo : TwoForm

The two-form of the second Hasse coefficient at zero.

Equations

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

def UnrestrictedBooleanMul.N4.targetTwo (c : TargetCoeff) : TwoForm

The alternating two-form whose mixed block is the target Hankel matrix.

Equations

• UnrestrictedBooleanMul.N4.targetTwo c i j = if hi : ↑i < 4 then if hj : 4 ≤ ↑j then c ⟨↑i + (↑j - 4), ⋯⟩ else 0 else if hj : ↑j < 4 then c ⟨↑j + (↑i - 4), ⋯⟩ else 0

def UnrestrictedBooleanMul.N4.targetTwoLinear : TargetCoeff →ₗ[F₂] TwoForm

The target Hankel two-form construction as a linear map.

Equations

• UnrestrictedBooleanMul.N4.targetTwoLinear = { toFun := UnrestrictedBooleanMul.N4.targetTwo, map_add' := ⋯, map_smul' := ⋯ }

theorem UnrestrictedBooleanMul.N4.targetTwo_cross (c : TargetCoeff) (i j : Fin 4) : targetTwo c (aCoord i) (bCoord j) = c ⟨↑i + ↑j, ⋯⟩

theorem UnrestrictedBooleanMul.N4.targetTwo_sameA (c : TargetCoeff) (i j : Fin 4) : targetTwo c (aCoord i) (aCoord j) = 0

theorem UnrestrictedBooleanMul.N4.targetTwo_sameB (c : TargetCoeff) (i j : Fin 4) : targetTwo c (bCoord i) (bCoord j) = 0

@[simp]

theorem UnrestrictedBooleanMul.N4.targetTwo_basis_zero : targetTwo (targetBasis 0) = zeroPlaceTwo

@[simp]

theorem UnrestrictedBooleanMul.N4.targetTwo_basis_one : targetTwo (targetBasis 1) = zeroFirstJetTwo

@[simp]

theorem UnrestrictedBooleanMul.N4.targetTwo_basis_two : targetTwo (targetBasis 2) = zeroSecondJetTwo

@[simp]

theorem UnrestrictedBooleanMul.N4.rationalPlaceTwo_zero_eq : rationalPlaceTwo 0 = zeroPlaceTwo

theorem UnrestrictedBooleanMul.N4.targetTwo_injective : Function.Injective targetTwo

theorem UnrestrictedBooleanMul.N4.targetTwo_rationalCoeffRep (α : Fin 3 → F₂) : targetTwo (rationalCoeffRep α) = rationalTwo α

The concrete rational-place coordinates agree in the Hankel and exterior models.

def UnrestrictedBooleanMul.N4.targetTwoSpace : Submodule F₂ TwoForm

The seven-dimensional subspace of target Hankel two-forms.

Equations

• UnrestrictedBooleanMul.N4.targetTwoSpace = UnrestrictedBooleanMul.N4.targetTwoLinear.range

def UnrestrictedBooleanMul.N4.IsDecomposableTwo (q : TwoForm) : Prop

The two-form is the exterior product of two linear forms.

Equations

• UnrestrictedBooleanMul.N4.IsDecomposableTwo q = ∃ (u : UnrestrictedBooleanMul.N4.LinearForm) (v : UnrestrictedBooleanMul.N4.LinearForm), q = UnrestrictedBooleanMul.N4.vectorWedge u v

theorem UnrestrictedBooleanMul.N4.targetTwoSpace_finrank : Module.finrank F₂ ↥targetTwoSpace = 7