claimroutineinferred_dep

Remaining equations are compatible and unimodular

Shows y2a=hby^2a=hb and rh+qy2=1rh+qy^2=1, so hW=ahW=a, y2W=by^2W=b is solvable
supplies compatibility and unimodularity for eliminating WW
Claim·§2 An elementary lifting lemma·inside lemLifting lemma: polynomial algebra over B

Statement (paper)

Let A=B[U,G]/(hG−yU−x)A=B[U,G]/(hG-yU-x), and in AA put a=y+U2a=y+U^2 and b=s−hG2+2UyGb=s-hG^2+2UyG. Then y2a−hb=0y^2a-hb=0 in AA, and with r=α(1+βy)r=\alpha(1+\beta y) and q=β2q=\beta^2 one has rh+qy2=1rh+qy^2=1.

In plain English

In A=B[U,G]/(hG−yU−x)A=B[U,G]/(hG-yU-x), the elements a=y+U2a=y+U^2 and b=s−hG2+2UyGb=s-hG^2+2UyG satisfy y2a=hby^2a=hb. Also r=α(1+βy)r=\alpha(1+\beta y) and q=β2q=\beta^2 satisfy rh+qy2=1rh+qy^2=1, where α,β\alpha,\beta are the elements with αh+βy=1\alpha h+\beta y=1 coming from (h,y)=B(h,y)=B.

Why it's here

The identity y2a−hb=0y^2a-hb=0 follows by expanding and using x2+y3=hsx^2+y^3=hs, which gives y2a−hb=(hG−yU)2−x2y^2a-hb=(hG-yU)^2-x^2, and this is 00 in AA because hG−yU=xhG-yU=x. The relation rh+qy2=1rh+qy^2=1 follows from αh+βy=1\alpha h+\beta y=1. Together they say that the system hW=ahW=a, y2W=by^2W=b is compatible and its coefficients are unimodular, so it has the unique solution W0=ra+qbW_0=ra+qb. This is what the next claim uses to eliminate WW.
Classified routine:
The compatibility identity follows by expansion using the preceding change-of-variable claim and x2+y3=hsx^2+y^3=hs; unimodularity follows by squaring the Bézout relation lpha h+eta y=1 in the indicated form.

Uses

claimChange of variable makes first relation linear

Used by

claimCompatible solution eliminates the variable W

Sources

PaperOpen
Section
§2 An elementary lifting lemma
Page
—
Label
—
Line
paper.tex:197
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Remaining equations are compatible and unimodular" rests on claim-lem-lift-1