lemmaroutineunresolved_ref

Private odd valuation for each radicand

Lemma·alg:private-valuations·§8.4 A separate odd valuation for each radicand

Statement (paper)

For every

\ell\in\{1,\ldots,j\}

there is an integer-valued valuation

v_\ell

M

such that

v_\ell(D_\ell)=1,\qquad v_\ell(D_m)=0\quad(m\ne\ell).

Consequently the classes of

D_1,\ldots,D_j

are independent in

M^\times/(M^\times)^2

In plain English

For each

\ell\in\{1,\ldots,j\}

there is an integer-valued valuation

v_\ell

M

with

v_\ell(D_\ell)=1

and

v_\ell(D_m)=0

for

m\ne\ell

. Hence the classes of

D_1,\ldots,D_j

are independent in

M^\times/(M^\times)^2

Why it's here

Each radicand

D_\ell

gets its own valuation, which sees only

D_\ell

to odd order and treats the other

D_m

as units. The construction splits by the shape of the limiting locus: the plane (orders along irreducible curves

Q_\ell

), a general curve (power-series branch at a smooth point), a line, or a hyperbola (simple zeros of

L_\ell-4

). Since a square has even valuation under every integer-valued valuation, any nonempty product of the

D_m

is a non-square, which gives independence modulo squares.

Classified routine:

A case-by-case construction of discrete valuations (orders of vanishing along curves or at smooth branch points) that separate the radicands. Independence modulo squares then follows by the standard parity argument: a square has even valuation, as in Kummer-theory independence criteria.

Uses

Nothing else in the paper

Used by

Nothing in the paper

Inside the proof

claimPlane case: order along irreducible Q_ellclaimSimple point on curve away from anchorclaimOther radicands avoid 0 and 4 at s_ellclaimPower-series valuation of order oneclaimSame curve, linear or hyperbola formclaimPrivate valuation in the line caseclaimFractional-linear case gives private simple zeroclaimSubset products of radicands are non-squares

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

warn
unresolved_ref
Excluding b=1 uses the unit-circle exclusion equation alg:unit-circle and deletion hypothesis argued in Section 8 text, not a labeled statement.