claimroutineinferred_dep

Vanishing gradient excludes coordinate

Rules out FF 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 FF were a coordinate of RR, that is, the first component of a polynomial automorphism of RR, then the Jacobian matrix of that automorphism at P=(2,0,−1/2,1/2)P=(2,0,-1/2,1/2) would be invertible. Its first row is ∇⁡F(P)=0\grad F(P)=0, which is impossible, so FF is not a coordinate of RR.

In plain English

If FF were a coordinate of RR, i.e. the first component of a polynomial automorphism of RR, that automorphism's Jacobian matrix at P=(2,0,−1/2,1/2)P=(2,0,-1/2,1/2) would be invertible, yet its first row ∇⁡F(P)\grad F(P) is zero. Hence FF is not a coordinate of RR.

Why it's here

This finishes the theorem's last conclusion by combining the critical point ∇⁡F(P)=0\grad F(P)=0 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 PP 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.

Uses

claimAmbient identity gives critical point

Used by

Nothing in the paper

Sources

PaperOpen
Section
§3 The affine-space fibre and the critical point
Page
—
Label
—
Line
paper.tex:324
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Jacobian invertibility rules out a coordinate" rests on claim-thm-main-4