Classified quartic seed-using normal form

This is the circuit-level endpoint of the quartic and sextic identities. It adds the two independent seed coefficients, places the feedback coefficient in their plane, excludes the zero feedback, and applies the rational annihilator classification.

def UnrestrictedBooleanMul.N4.SeedUsingQuarticClassifiedForm (g : ANF 8) : Prop

A seed-using target witness with its factor in the classified quartic normal form.

Equations

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

theorem UnrestrictedBooleanMul.N4.NormalizedEight.seedUsingQuarticClassifiedForm {C : Circuit 8 8} (h : NormalizedEight C) (hquartic : quarticProbeANF (C.gate 3) ≠ 0) : SeedUsingQuarticClassifiedForm (C.gate 3)

A normalized eight-gate circuit with nonzero seed quartic reaches the fully classified seed-using form.