The normalized hard annihilator and second jet

For a first-jet seed M ∧ E₀, eight quintic rows determine the target annihilator. They force the last four Hankel coefficients to vanish, so the annihilator is exactly ⟨E₀,E₁,E₂⟩. The bridge below is a fixed algebraic matrix on coordinate vectors and target basis elements; no truth table or circuit state is enumerated.

def UnrestrictedBooleanMul.N4.hardQuinticCoord : Fin 8 → Fin 8 × Fin 8 × Fin 8 × Fin 8 × Fin 8

Eight quintic coordinates detecting the second-jet obstruction.

Equations

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

def UnrestrictedBooleanMul.N4.hardQuinticSet (u : Fin 8) : Finset (Fin 8)

The squarefree monomial for a second-jet quintic coordinate.

Equations

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

def UnrestrictedBooleanMul.N4.hardQuinticProbeANF : ANF 8 →ₗ[F₂] Fin 8 → F₂

Extract the eight ANF coefficients used for the second-jet obstruction.

Equations

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

def UnrestrictedBooleanMul.N4.hardQuinticWedgeProbe (M : LinearForm) (c : TargetCoeff) : Fin 8 → F₂

The second-jet quintic probes of a linear form, the zero-place form, and a target.

Equations

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

theorem UnrestrictedBooleanMul.N4.hardQuinticProbeANF_eq_zero_of_degreeLE_four {p : ANF 8} (hp : DegreeLE 4 p) : hardQuinticProbeANF p = 0

def UnrestrictedBooleanMul.N4.hardQuinticWedgeProbeBilinear : LinearForm →ₗ[F₂] TargetCoeff →ₗ[F₂] Fin 8 → F₂

The second-jet quintic probes as a bilinear map in the linear form and target.

Equations

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

theorem UnrestrictedBooleanMul.N4.hardQuinticProbe_linear_zeroPlace_target (M : LinearForm) (c : TargetCoeff) : hardQuinticProbeANF (linearANF M * rationalANF (rationalSingleton 0) * targetANF c) = hardQuinticWedgeProbe M c

The selected ANF degree-five rows are the corresponding exterior rows of the first-jet cubic against an arbitrary target word.

theorem UnrestrictedBooleanMul.N4.hardAnnihilator_rows_classify (pa pb ja jb : F₂) (c : TargetCoeff) (hjet : ja ≠ 0 ∨ jb ≠ 0) (hzero : hardQuinticWedgeProbe (normalizedFirstJetVector pa pb ja jb) c = 0) : c 3 = 0 ∧ c 4 = 0 ∧ c 5 = 0 ∧ c 6 = 0

Eight fixed quintic rows reduce the annihilator of a nonzero normalized first-jet seed to its first three Hankel coordinates.

theorem UnrestrictedBooleanMul.N4.hardAnnihilator_classification (pa pb ja jb : F₂) (c : TargetCoeff) (hjet : ja ≠ 0 ∨ jb ≠ 0) (hzero : hardQuinticWedgeProbe (normalizedFirstJetVector pa pb ja jb) c = 0) : c = c 2 • targetBasis 2 + c 1 • targetBasis 1 + c 0 • targetBasis 0

theorem UnrestrictedBooleanMul.N4.hardAnnihilator_outside_feedback_is_secondJet (pa pb ja jb : F₂) (c : TargetCoeff) (hjet : ja ≠ 0 ∨ jb ≠ 0) (houtside : c ∉ feedbackCoeffSpace) (hzero : hardQuinticWedgeProbe (normalizedFirstJetVector pa pb ja jb) c = 0) : ∃ (α : F₂) (β : F₂), c = secondJetFeedbackCoeff α β

A hard annihilator outside the feedback state is exactly a second jet.

theorem UnrestrictedBooleanMul.N4.degreeLE_two_of_mem_zeroFeedbackLowSpace {p : ANF 8} (hp : p ∈ zeroFeedbackLowSpace) : DegreeLE 2 p

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_eq_zero_of_degreeLE_two {p : ANF 8} (hp : DegreeLE 2 p) : anfThreeProjection p = 0

theorem UnrestrictedBooleanMul.N4.hardQuinticProbe_mul_target_congr_of_cubic {p q : ANF 8} (hp : DegreeLE 3 p) (hq : DegreeLE 3 q) (hcubic : anfThreeProjection p = anfThreeProjection q) (c : TargetCoeff) : hardQuinticProbeANF (p * targetANF c) = hardQuinticProbeANF (q * targetANF c)

Multiplication by a quadratic target sees only the cubic homogeneous part in the selected hard rows.

theorem UnrestrictedBooleanMul.N4.normalizedSeed_absorption_hardAnnihilator {g correction addend : ANF 8} {M N : LinearForm} {fConst : F₂} {fLinear : LinearForm} {c : TargetCoeff} (hg : DegreeLE 3 g) (hcorrection : DegreeLE 2 correction) (haddend : DegreeLE 2 addend) (hseed : g + correction = linearANF M * (linearANF N + rationalANF (rationalSingleton 0))) (habsorb : (g + addend) * (affineANF fConst fLinear + targetANF c) = affineANF fConst fLinear + targetANF c) : hardQuinticWedgeProbe M c = 0

Degree five in a normalized seed absorption identity supplies the hard annihilator equation used by the second-jet classification.