OAI/AlgebraicGeometry/StableCoordinate/NonCoordinate.lean

The exact polynomial is not a coordinate in four variables

The sole temporary hypothesis is that the literal polynomial f is sent to the first variable by a complex algebra automorphism. The proved separated filtration and associated-graded construction then produce a nonzero locally nilpotent derivation on the actual quadric with a nonzero invariant in its center ideal. The proved normalized determinant lift carries this to a nonzero weight-preserving locally nilpotent derivation annihilating v, in contradiction with the proved rigidity theorem. No auxiliary construction or existence hypothesis remains in this statement.