claimroutine

Same curve, linear or hyperbola form

Claim·§8.4 A separate odd valuation for each radicand·inside lemPrivate odd valuation for each radicand

Statement (paper)

The two loci are the same curve, and the projection degree is one for both projections. Its irreducible equation therefore has degree one in each variable, so it has either the form , w=ez+e′w=ez+e' with e≠0e\ne0, or the form , (z−u)(w−v)=b(z-u)(w-v)=b with b≠0b\ne0, with constants in B0B_0. In the case one has b≠1b\ne1, by the exact unit-circle exclusion .

In plain English

The two limiting loci coincide as one curve, and both coordinate projections have degree one, so its irreducible equation is either a line w=ez+e′w=ez+e' with e≠0e\ne0 or a hyperbola (z−u)(w−v)=b(z-u)(w-v)=b with b≠0b\ne0, with constants in B0B_0. In the hyperbola case b≠1b\ne1.

Why it's here

This pins the curve down to one of two explicit shapes, which are the only cases the later private-simple-zero claims (line case and fractional-linear case) need to handle. The exclusion b≠1b\ne1 comes from the earlier result that the loci are not a common unit circle (z−u)(w−v)=1(z-u)(w-v)=1.
Classified routine:
A bidegree-(1,1) irreducible curve has equation azw+bz+cw+d=0, which elementary algebra reduces to a line or a hyperbola (z-u)(w-v)=b. The exclusion b≠1 follows directly from the earlier claim alg-obstruction-2 that the loci are not a common unit circle.

Uses

claimMinimal loci are symmetric, not a common unit circle

Used by

claimPrivate valuation in the line caseclaimFractional-linear case gives private simple zero

Sources

PaperOpen
Section
§8.4 A separate odd valuation for each radicand
Page
—
Label
—
Line
sections/07-algebra.tex:528
Leannot aligned

Phase 2 aligns this node to a Lean declaration.