claimroutineinferred_dep

Other radicands avoid 0 and 4 at s_ell

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

Statement (paper)

For every m≠ℓm\ne\ell, one has Lm(sℓ)≠0L_m(s_\ell)\ne0 and Lm(sℓ)≠4L_m(s_\ell)\ne4. These are nonvanishing statements in U\mathcal U, so placing more of their entries in K0K_0 does not change them.

In plain English

For every m≠ℓm\ne\ell, the other radicand's function LmL_m satisfies Lm(sℓ)≠0L_m(s_\ell)\ne0 and Lm(sℓ)≠4L_m(s_\ell)\ne4 at the chosen point sℓs_\ell. Since these are nonvanishing statements in U\mathcal U, enlarging the part of the entries placed in K0K_0 leaves them unchanged.

Why it's here

This shows that at sℓs_\ell only the ℓ\ell-th radicand degenerates, so every DmD_m with m≠ℓm\ne\ell is a unit there. This is what makes vℓ(Dm)=0v_\ell(D_m)=0 in the order-one valuation built from the power-series embedding at sℓs_\ell. It rests on sℓs_\ell being a smooth point away from the anchor and on the independence of the grid coordinates from the generic grid lemma. The remark on K0K_0 lets the argument pass to larger fields without redoing it.
Classified routine:
A direct consequence of the preceding claim (choice of a smooth point sℓs_\ell away from the anchor) combined with the algebraic independence of grid coordinates from the generic grid lemma; a nonvanishing check by standard bookkeeping.

Uses

claimSimple point on curve away from anchorlemGeneric complete grid with independent coordinates

Used by

claimPower-series valuation of order one

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Other radicands nonvanishing at s_ell" rests on claim-alg-private-valuations-2
  • info
    inferred_dep
    outline: "Other radicands nonvanishing at s_ell" rests on alg:generic-grid