The normalized seed is genuinely cubic

Quartic exclusion says that the rational quadratic parts of the two seed factors are dependent. Expanding the three possible dependencies in the Boolean ANF algebra bounds the product by degree three. The independent high-part argument then makes its cubic projection nonzero.

theorem UnrestrictedBooleanMul.N4.DegreeLE.add {m d : ℕ} {p q : ANF m} (hp : DegreeLE d p) (hq : DegreeLE d q) : DegreeLE d (p + q)

theorem UnrestrictedBooleanMul.N4.representedLowFactor_degreeLE_two (a : F₂) (ell : LinearForm) (alpha : Fin 3 → F₂) : DegreeLE 2 (representedLowFactor a ell alpha)

theorem UnrestrictedBooleanMul.N4.NormalizedEight.seed_degreeLE_three {C : Circuit 8 8} (h : NormalizedEight C) : DegreeLE 3 (C.gate 3)

Quartic exclusion upgrades the normalized seed to degree at most three.

theorem UnrestrictedBooleanMul.N4.NormalizedEight.seed_cubicProjection_ne_zero {C : Circuit 8 8} (h : NormalizedEight C) : anfThreeProjection (C.gate 3) ≠ 0

The cubic homogeneous projection of the normalized seed is nonzero.

theorem UnrestrictedBooleanMul.N4.NormalizedEight.cubicSeedState {C : Circuit 8 8} (h : NormalizedEight C) : CubicSeedState C

The exact manuscript predicate: the normalized seed has nonzero cubic high part and no monomial above degree three.