claimroutineinferred_dep

Center of coarsened valuation is a branch ideal

Shows the center of w∗w_* is the branch ideal p+\mathfrak p_+ or p−\mathfrak p_-
picks the tested branch
Claim·§2.5 Odd valuations select a tested branch·inside lemOdd valuation selects a tested branch

Statement (paper)

The set p={x∈RF:w∗(x~)>0}\mathfrak p=\{x\in R_F:w_*(\widetilde x)>0\} is a proper prime ideal of RFR_F containing rr, and it equals one of the two tested branch ideals p+,p−\mathfrak p_+,\mathfrak p_-, since RF/rRF≃(R/rR)[X]/(X2−2)≃(R/rR)×(R/rR)R_F/rR_F\simeq(R/rR)[X]/(X^2-2)\simeq(R/rR)\times(R/rR) and every prime of this product is one of its two maximal ideals.

In plain English

The set p={x∈RF:w∗(x~)>0}\mathfrak p=\{x\in R_F: w_*(\widetilde x)>0\} is a proper prime ideal of RFR_F containing rr, and it equals one of the two tested branch ideals p+\mathfrak p_+ or p−\mathfrak p_-.

Why it's here

Given that w∗w_* is nonnegative on RFR_F and positive on rr, the positivity locus is a proper prime ideal containing rr. Since RF/rRF≃(R/rR)×(R/rR)R_F/rR_F\simeq(R/rR)\times(R/rR), its only primes are the two maximal ideals, so p\mathfrak p must be p+\mathfrak p_+ or p−\mathfrak p_-. This chooses the branch used in the localization-to-valuation transfer in the next claim.
Classified routine:
Follows directly from the previous claim by the standard fact that the center of a valuation nonnegative on a ring is a prime ideal, combined with the Chinese remainder decomposition of R_F/rR_F into two copies of R/rR (which needs R/rR to be a field).

Uses

claimCoarsened valuation nonnegative on R_F, positive on r

Used by

claimLocalization membership transfers to valuation bounds

Sources

PaperOpen
Section
§2.5 Odd valuations select a tested branch
Page
—
Label
—
Line
sections/02-reduction.tex:685
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Center of coarsened valuation is a tested branch ideal" rests on claim-red-coarsening-2