Rational quartic annihilators in the Hankel target

Nine fixed exterior coordinates classify the target two-forms annihilated by a nonzero rational direction. The certificate ranges over only the seven nonzero rational coefficient vectors and 128 Hankel words. It is an algebraic coordinate check, not a circuit or truth-table enumeration.

def UnrestrictedBooleanMul.N4.rationalSingleton (theta : Fin 3) : Fin 3 → F₂

The unit coefficient vector for one rational place.

Equations

• UnrestrictedBooleanMul.N4.rationalSingleton theta = ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] theta

def UnrestrictedBooleanMul.N4.rationalTangentAt (theta : Fin 3) (eps : F₂) : TargetCoeff

A first-jet target at a rational place, optionally translated by the place itself.

Equations

• UnrestrictedBooleanMul.N4.rationalTangentAt ⟨0, isLt⟩ eps = ![eps, 1, 0, 0, 0, 0, 0]
• UnrestrictedBooleanMul.N4.rationalTangentAt ⟨1, isLt⟩ eps = ![eps, 1 + eps, eps, 1 + eps, eps, 1 + eps, eps]
• UnrestrictedBooleanMul.N4.rationalTangentAt ⟨2, isLt⟩ eps = ![0, 0, 0, 0, 0, 1, eps]

def UnrestrictedBooleanMul.N4.quarticAnnihilatorCoord : Fin 9 → Fin 8 × Fin 8 × Fin 8 × Fin 8

A compact set of quartic coordinates sufficient for the rational annihilator classification.

Equations

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

def UnrestrictedBooleanMul.N4.quarticAnnihilatorProbe (q r : TwoForm) (k : Fin 9) : F₂

Extract a designated quartic-annihilator coordinate of a wedge of two two-forms.

Equations

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

def UnrestrictedBooleanMul.N4.quarticAnnihilatorTable : Fin 9 → ℕ

Packed 9 × (7·3) bilinear coefficient matrix for the probe.

Equations

• UnrestrictedBooleanMul.N4.quarticAnnihilatorTable = ![194, 533552, 1682, 786438, 591232, 13330, 601088, 99458, 548864]

def UnrestrictedBooleanMul.N4.quarticAnnihilatorCoeffProbe (c : TargetCoeff) (delta : Fin 3 → F₂) (k : Fin 9) : F₂

The scalar bilinear formula for a quartic-annihilator probe on target coordinates.

Equations

• UnrestrictedBooleanMul.N4.quarticAnnihilatorCoeffProbe c delta ⟨0, isLt⟩ = c 0 * delta 1 + c 2 * delta 0 + c 2 * delta 1
• UnrestrictedBooleanMul.N4.quarticAnnihilatorCoeffProbe c delta ⟨1, isLt⟩ = c 1 * delta 1 + c 1 * delta 2 + c 3 * delta 1 + c 4 * delta 1 + c 6 * delta 1
• UnrestrictedBooleanMul.N4.quarticAnnihilatorCoeffProbe c delta ⟨2, isLt⟩ = c 0 * delta 1 + c 1 * delta 1 + c 2 * delta 1 + c 3 * delta 0 + c 3 * delta 1
• UnrestrictedBooleanMul.N4.quarticAnnihilatorCoeffProbe c delta ⟨3, isLt⟩ = c 0 * delta 1 + c 0 * delta 2 + c 6 * delta 0 + c 6 * delta 1
• UnrestrictedBooleanMul.N4.quarticAnnihilatorCoeffProbe c delta ⟨4, isLt⟩ = c 2 * delta 1 + c 2 * delta 2 + c 3 * delta 1 + c 5 * delta 1 + c 6 * delta 1
• UnrestrictedBooleanMul.N4.quarticAnnihilatorCoeffProbe c delta ⟨5, isLt⟩ = c 0 * delta 1 + c 1 * delta 1 + c 3 * delta 1 + c 4 * delta 0 + c 4 * delta 1
• UnrestrictedBooleanMul.N4.quarticAnnihilatorCoeffProbe c delta ⟨6, isLt⟩ = c 3 * delta 1 + c 3 * delta 2 + c 4 * delta 1 + c 5 * delta 1 + c 6 * delta 1
• UnrestrictedBooleanMul.N4.quarticAnnihilatorCoeffProbe c delta ⟨7, isLt⟩ = c 0 * delta 1 + c 2 * delta 1 + c 3 * delta 1 + c 5 * delta 0 + c 5 * delta 1
• UnrestrictedBooleanMul.N4.quarticAnnihilatorCoeffProbe c delta ⟨8, isLt⟩ = c 4 * delta 1 + c 4 * delta 2 + c 6 * delta 1

def UnrestrictedBooleanMul.N4.VanishesOnQuarticAnnihilatorProbe (c : TargetCoeff) (delta : Fin 3 → F₂) : Prop

Every designated quartic-annihilator coefficient vanishes.

Equations

• UnrestrictedBooleanMul.N4.VanishesOnQuarticAnnihilatorProbe c delta = ∀ (k : Fin 9), UnrestrictedBooleanMul.N4.quarticAnnihilatorCoeffProbe c delta k = 0

@[instance_reducible]

instance UnrestrictedBooleanMul.N4.instDecidableVanishesOnQuarticAnnihilatorProbe (c : TargetCoeff) (delta : Fin 3 → F₂) : Decidable (VanishesOnQuarticAnnihilatorProbe c delta)

Equations

• UnrestrictedBooleanMul.N4.instDecidableVanishesOnQuarticAnnihilatorProbe c delta = id inferInstance

theorem UnrestrictedBooleanMul.N4.quarticAnnihilatorCoeffProbe_eq (c : TargetCoeff) (delta : Fin 3 → F₂) (k : Fin 9) : quarticAnnihilatorCoeffProbe c delta k = quarticAnnihilatorProbe (targetTwo c) (rationalTwo delta) k

def UnrestrictedBooleanMul.N4.rationalAnnihilatorDelta : Fin 6 → Fin 3 → F₂

The rational-place coefficient vectors paired with the six tangent targets.

Equations

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

theorem UnrestrictedBooleanMul.N4.rational_target_annihilator_pair_classification (delta : Fin 3 → F₂) (c : TargetCoeff) : delta ≠ 0 → ¬IsRationalCoeff c → VanishesOnQuarticAnnihilatorProbe c delta → ∃ (i : Fin 6), delta = rationalAnnihilatorDelta i ∧ c = tangentWord i

Packed finite form of the rational target-annihilator certificate.

theorem UnrestrictedBooleanMul.N4.rational_target_annihilator_classification (delta : Fin 3 → F₂) (c : TargetCoeff) (hdelta : delta ≠ 0) (hc : ¬IsRationalCoeff c) (hprobe : VanishesOnQuarticAnnihilatorProbe c delta) : ∃ (theta : Fin 3) (eps : F₂), delta = rationalSingleton theta ∧ c = rationalTangentAt theta eps

A nonrational Hankel target annihilated by a nonzero rational two-form is a first tangent at one of the three singleton rational places.

theorem UnrestrictedBooleanMul.N4.vanishesOnQuarticAnnihilatorProbe_of_wedge_zero {c : TargetCoeff} {delta : Fin 3 → F₂} (h : wedgeTwo (targetTwo c) (rationalTwo delta) = 0) : VanishesOnQuarticAnnihilatorProbe c delta