claimroutineinferred_dep

Ambient identity gives critical point

Shows X2+Y3=s(1+F)X^2+Y^3=s(1+F) in RR, so ∇⁡F(P)=0\grad F(P)=0 at PP
produces the critical point of FF
Claim·§3 The affine-space fibre and the critical point·inside thmNoncoordinate polynomial with affine three-space zero fibre

Statement (paper)

With X=x+s3X=x+s^3 and Y=y−s2Y=y-s^2 interpreted via , one has the polynomial identity X2+Y3=s(1+F)X^2+Y^3=s(1+F) in RR. At P=(2,0,−1/2,1/2)P=(2,0,-1/2,1/2) in the variable order (h,u,v,w)(h,u,v,w) the values are x=−1x=-1, y=1y=1, s=1s=1, p=2p=2, X=Y=0X=Y=0, F=−1F=-1, and consequently ∇⁡F(P)=0\grad F(P)=0.

In plain English

With X=x+s3X=x+s^3 and Y=y−s2Y=y-s^2, the identity X2+Y3=s(1+F)X^2+Y^3=s(1+F) holds in RR. At P=(2,0,−1/2,1/2)P=(2,0,-1/2,1/2) in variables (h,u,v,w)(h,u,v,w) one has x=−1x=-1, y=1y=1, s=1s=1, p=2p=2, X=Y=0X=Y=0 and F=−1F=-1, and therefore ∇⁡F(P)=0\grad F(P)=0.

Why it's here

This is the step that produces the critical point: the cusp and translation identities from the earlier claim give X2+Y3=s(1+F)X^2+Y^3=s(1+F), and at PP both sides vanish to the order needed to force ∇⁡F(P)=0\grad F(P)=0, because XX and YY vanish and 1+F1+F vanishes while s=1s=1. The vanishing gradient is what the next claim uses, via Jacobian invertibility, to rule out FF being a coordinate.
Classified routine:
The identity follows from the earlier cusp and translation identities by substitution. Evaluating and differentiating it at the specified point is a direct calculation.

Uses

claimCusp and translation identities

Used by

claimVanishing gradient excludes coordinate

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Ambient identity yields a critical point" rests on claim-thm-main-1