Circuit-level quartic seed-using normal form

The first useful suffix gate is first reduced to the two algebraic child types. Under a nonzero seed quartic, the low--low type is impossible. The remaining seed-using type is recorded together with its two Boolean idempotence equations and the rational-annihilator certificate.

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

The complete seed-using normal form, kept in Prop so that it can be obtained from the existential useful-child certificate without choosing data computationally.

Equations

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

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

Under a nonzero seed quartic, the first useful child has the complete seed-using algebraic normal form needed by the rest of the quartic exclusion.