claimroutineinferred_dep

Simple point on curve away from anchor

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

Statement (paper)

Let

f(z,w)

be the irreducible equation of the left locus, a curve

V_1

, and set

a=z_{r_\ell}

. Then there is a point

s_\ell=(a,b)\in V_1

with

b\in K_0

such that

f_w(a,b)\ne0

and

b\ne w_{r_\ell}

; that is, either

V_2\ne V_1

or the

z

-projection of

V_1

has degree at least two.

In plain English

On the irreducible curve

V_1

with equation

f(z,w)=0

, with

a=z_{r_\ell}

, there is a point

s_\ell=(a,b)\in V_1

with

b\in K_0

f_w(a,b)\ne0

and

b\ne w_{r_\ell}

. Equivalently, either

V_2\ne V_1

or the

z

-projection of

V_1

has degree at least two.

Why it's here

This supplies the base point

s_\ell

over the abscissa

a

of the

\ell

-th radicand's anchor. It is a smooth point of the curve (since

f_w\ne0

) and is distinct from the anchor, which lets later claims check that the other radicands are nonzero and not

4

there. It also lets a power-series embedding of

K_0(V_1)

around

s_\ell

be built in which

L_\ell

has order exactly one, giving the odd valuation

v_\ell

Classified routine:

Follows from the generic-grid lemma by a standard argument about curves. Because the coordinates are generic and independent, the projection to

z

has a simple point over

a

distinct from the anchor, by ordinary bookkeeping with the discriminant and degree of the projection.

Uses

lemGeneric complete grid with independent coordinates

Used by

claimOther radicands avoid 0 and 4 at s_ellclaimPower-series valuation of order one

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Curve case: simple point s_ell off anchor" rests on alg:generic-grid