claimroutinestructure_uncertain

Cusp and translation identities

Shows x2+y3=hsx^2+y^3=hs and X2+Y3=x2+y3−s pX^2+Y^3=x^2+y^3-s\,p for the translation
identities behind the base algebra and the critical point
Claim·§3 The affine-space fibre and the critical point·inside thmNoncoordinate polynomial with affine three-space zero fibre

Statement (paper)

Direct expansion of gives x2+y3=hsx^2+y^3=hs. Moreover, for formal x,y,sx,y,s, the translation X=x+s3X=x+s^3, Y=y−s2Y=y-s^2 satisfies X2+Y3=x2+y3−sp(x,y,s)X^2+Y^3=x^2+y^3-sp(x,y,s), since the terms s6s^6 from the square and cube cancel.

In plain English

Expanding the definitions of x,y,sx,y,s gives x2+y3=hsx^2+y^3=hs. For formal x,y,sx,y,s, the translation X=x+s3X=x+s^3, Y=y−s2Y=y-s^2 gives X2+Y3=x2+y3−s p(x,y,s)X^2+Y^3=x^2+y^3-s\,p(x,y,s).

Why it's here

This is the algebraic bookkeeping behind the proof of the main theorem. The cusp relation x2+y3=hsx^2+y^3=hs and the translation, where the s6s^6 terms cancel, let the later claims identify the base algebra with a polynomial ring in X,YX,Y and derive the ambient identity that yields the critical point.
Classified routine:
These identities are direct polynomial expansions of the paper’s definitions and the binomial formulas; the cancellation of the s^6 terms requires no new technique.

Uses

Nothing else in the paper

Used by

claimBase algebra is a polynomial ringclaimUnit ideal gives affine three-space fibreclaimAmbient identity gives critical point

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • warn
    structure_uncertain
    critique: Split after paper.tex:258: lines 255–258 establish the cusp identity, while lines 259–267 independently establish the formal translation identity. Later claims use these identities separately (claim-thm-main-3 uses the cusp identity; claim-thm-main-2 uses the translation).