# A stable-coordinate counterexample in four variables

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [An explicit noncoordinate polynomial with affine three-space zero fibre](../../preprints/An-explicit-noncoordinate-polynomial-with-affine-three-space-zero-fibre-September-24-2026/paper.pdf)
- [A stable coordinate that is not a coordinate in four variables](../../preprints/A-stable-coordinate-that-is-not-a-coordinate-in-four-variables-October-5-2026/stable-coordinate-four-variables.pdf)

## Scope

The stable coordinate conjecture predicts that a polynomial that becomes a coordinate after adjoining variables was already a coordinate. The formalization gives an explicit degree-five polynomial in four complex variables that becomes a coordinate after adjoining one variable but is not a coordinate in four variables. Every fiber is isomorphic to affine three-space, yet no fiber can be carried to a coordinate hyperplane by an ambient polynomial automorphism.

The Abhyankar–Sathaye conjecture predicts that a polynomial defining an affine-space quotient must be an ambient coordinate. For every $n\ge4$, the formalized counterexample gives $F\in\mathbb C[x_1,\ldots,x_n]$ with quotient $\mathbb C[x_1,\ldots,x_n]/(F)\cong\mathbb C[y_1,\ldots,y_{n-1}]$, although $F$ is not a coordinate.

A companion gives $n-1$ commuting, locally nilpotent derivations, linearly independent over the polynomial ring, whose common kernel is generated by the construction's explicit polynomial and contains no ambient coordinate. The extra $n-4$ derivations are ordinary partial derivatives in the added variables. The three-variable case is not covered.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Noncoordinate polynomial in every dimension at least four | [AbhyankarSathaye.lean](../ComparatorChallenges/AbhyankarSathaye.lean) |
| Commuting locally nilpotent derivations | [CommutingDerivations.lean](../ComparatorChallenges/CommutingDerivations.lean) |
| Degree-five stable noncoordinate with nonrectifiable affine-space fibers | [StableCoordinateFour.lean](../ComparatorChallenges/StableCoordinateFour.lean) |