Circuit-facing low--low quartic exclusion

The coordinate and basis-change argument in QuarticANF is stated for explicit affine-plus-rational factors. This file removes those coordinates from its interface and applies the result to the first useful child of the normalized seed. No circuit enumeration is involved.

theorem UnrestrictedBooleanMul.N4.lowLow_sum_mem_rationalLow_of_quartic_nonzero {g f : ANF 8} (hg : IsLowLowProduct g) (hf : IsLowLowProduct f) (hquartic : quarticProbeANF g ≠ 0) (hsum : g + f ∈ targetAmbient 8 (mulTarget 4)) : g + f ∈ rationalLowSpace

Two low--low products with a nonzero seed quartic cannot acquire a new target direction: if their sum is in Aff + T, it is already rational-low.

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

The normalized seed itself is a low--low product.

theorem UnrestrictedBooleanMul.N4.NormalizedEight.usefulSeedChild_not_lowLow {C : Circuit 8 8} (h : NormalizedEight C) (hquartic : quarticProbeANF (C.gate 3) ≠ 0) {target representative shift : ANF 8} (htarget : target ∈ targetAmbient 8 (mulTarget 4)) (htargetOld : target ∉ circuitFlag C 4) (hshift : shift ∈ circuitFlag C 4) (htargetEq : target = shift + representative) : ¬IsLowLowProduct representative

A useful first child of a normalized seed with nonzero quartic part cannot be represented by a low--low product. Both possible seed coefficients in the old-state shift are handled algebraically.