D=b^(6*(q-1)) clears every AuxJet coefficient for ell<7,k<n; powers of sqrt2 introduce no denominators. Equivalence of cleared coordinate zero and quadratic zero is proved.
Method: native-induction. Induction: finite row/column enumeration. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.