claimroutineinferred_dep
Vanishing gradient excludes coordinate
Rules out being a coordinate: an automorphism's Jacobian is invertible
turns the critical point into non-coordinateness
Claim·§3 The affine-space fibre and the critical point·inside thmNoncoordinate polynomial with affine three-space zero fibre
Statement (paper)
If were a coordinate of , that is, the first component of a polynomial automorphism of , then the Jacobian matrix of that automorphism at would be invertible. Its first row is , which is impossible, so is not a coordinate of .
In plain English
If were a coordinate of , i.e. the first component of a polynomial automorphism of , that automorphism's Jacobian matrix at would be invertible, yet its first row is zero. Hence is not a coordinate of .
Why it's here
This finishes the theorem's last conclusion by combining the critical point from the previous claim with a basic fact about automorphisms. An automorphism has an invertible Jacobian at every point, so a zero first row at gives a contradiction.
Classified routine:
This applies the standard chain-rule fact that a polynomial automorphism has an invertible Jacobian at every point to the critical point established in claim-thm-main-4.