claimroutineinferred_dep

Private valuation in the line case

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

Statement (paper)

In the line case, with aℓ=zrℓa_\ell=z_{r_\ell} one has Lℓ=e(z−aℓ)2L_\ell=e(z-a_\ell)^2, so Lℓ−4L_\ell-4 has two distinct simple zeros. For a chosen zero z=aℓ+cz=a_\ell+c with c2=4/ec^2=4/e, the corresponding point sℓs_\ell on the line has coordinates algebraic over B0(aℓ)B_0(a_\ell), and for every independent anchor rmr_m (m≠ℓm\ne\ell) one has Lm(sℓ)≠0,4L_m(s_\ell)\ne0,4, by joint genericity. Hence order at that abscissa in K0(z)K_0(z) gives a valuation vℓv_\ell with vℓ(Dℓ)=1v_\ell(D_\ell)=1 and vℓ(Dm)=0v_\ell(D_m)=0 for m≠ℓm\ne\ell.

In plain English

When the limiting curve is a line, taking aℓ=zrℓa_\ell=z_{r_\ell} gives Lℓ=e(z−aℓ)2L_\ell=e(z-a_\ell)^2, so Lℓ−4L_\ell-4 has two distinct simple zeros. Order of vanishing at a chosen zero gives a valuation vℓv_\ell with vℓ(Dℓ)=1v_\ell(D_\ell)=1 and vℓ(Dm)=0v_\ell(D_m)=0 for all m≠ℓm\ne\ell.

Why it's here

This handles the line alternative from the previous claim's dichotomy: the simple zero of Lℓ−4L_\ell-4 makes DℓD_\ell have odd order there, while joint genericity ensures LmL_m takes values other than 00 and 44 at that point, so the other DmD_m have order zero. These valuations feed into the square-class independence of the DℓD_\ell in the parent lemma.
Classified routine:
Direct computation in the line case of the preceding dichotomy: a simple zero of a quadratic gives a place of odd order for D_ℓ, and genericity rules out vanishing of the other radicands. This is a standard valuation argument for function fields.

Uses

claimSame curve, linear or hyperbola form

Used by

claimSubset products of radicands are non-squares

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Line case private simple zero" rests on claim-alg-private-valuations-5