claimroutineinferred_dep

Fractional-linear case gives private simple zero

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

Statement (paper)

In the fractional-linear case, with ζ=(z−u)/(aℓ−u)\zeta=(z-u)/(a_\ell-u) one has Lℓ=−b(ζ−1)2/ζL_\ell=-b(\zeta-1)^2/\zeta, and Lℓ−4L_\ell-4 has two distinct simple zeros at finite points with z≠uz\ne u, the roots of bζ2+(4−2b)ζ+b=0b\zeta^2+(4-2b)\zeta+b=0. For a corresponding point sℓs_\ell, algebraic over B0(aℓ)B_0(a_\ell), no other radicand LmL_m, m≠ℓm\ne\ell, vanishes or equals 44 at sℓs_\ell, so this simple zero of Lℓ−4L_\ell-4 is shared by no other radicand, and order at its abscissa gives the required valuation vℓv_\ell over K0(z)K_0(z).

In plain English

In the hyperbola (fractional-linear) case, with ζ=(z−u)/(aℓ−u)\zeta=(z-u)/(a_\ell-u) we have Lℓ=−b(ζ−1)2/ζL_\ell=-b(\zeta-1)^2/\zeta, and Lℓ−4L_\ell-4 has two distinct finite simple zeros with z≠uz\ne u, the roots of bζ2+(4−2b)ζ+b=0b\zeta^2+(4-2b)\zeta+b=0. At a corresponding point sℓs_\ell no other radicand LmL_m (m≠ℓm\ne\ell) vanishes or equals 44, so this zero is private to LℓL_\ell and its order gives the valuation vℓv_\ell over K0(z)K_0(z).

Why it's here

This handles the hyperbola branch of the dichotomy from the same-curve claim, where b≠0b\ne0 and b≠1b\ne1. It produces, for each ℓ\ell, a simple zero of Lℓ−4L_\ell-4 that no other radicand shares, so the order of vanishing there is an odd valuation vℓv_\ell supporting the square-class independence of the DℓD_\ell in the parent lemma.
Classified routine:
A direct calculation on the hyperbola branch from the preceding same-curve claim: it substitutes the fractional-linear form, checks that the quadratic has distinct simple roots, and verifies that the zero is not shared by other radicands, which is standard valuation bookkeeping.

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:560
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

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