Reason: Proof of lem:absolute-value-properties-2026b. Preliminaries (a)-(g) and claims 1-8 are reproduced from the published proof of lem:absolute-value-properties-2026a (attribution note at the head of the body); claim 9, the strict two-sided bound, is proved from claims 1, 3 and 6 with antisymmetry.
Proof
Attribution. The preliminary facts (a)--(g) and the proofs of claims 1--8 below are reproduced from the published proof of the preceding version of this lemma, published under the label lem:absolute-value-properties-2026a; only claim 9 and this note are new.
Throughout, F is an ordered field: a field together with a total orderβ€ such that aβ€b implies a+cβ€b+c, and 0β€a together with 0β€b implies 0β€ab. Absolute values are those of that definition. As in the statement, s<t abbreviates sβ€t together with sξ =t. We first record some consequences of these axioms.
(a)uβ€0 if and only if 0β€βu. Indeed, adding βu to uβ€0 gives 0β€βu, and adding u to 0β€βu gives uβ€0.
(b) If uβ€v then βvβ€βu: add βuβv to both sides.
(c)(βu)v=β(uv) and (βu)(βv)=uv, since uv+(βu)v=(u+(βu))v=0 and the same identity applied twice.
(d) If 0β€c and uβ€v then cuβ€cv: from uβ€v we get 0β€vβu, hence 0β€c(vβu)=cvβcu, and adding cu gives cuβ€cv.
(e)0β€u2 for every u: if 0β€u this is the second order axiom, and otherwise uβ€0 by totality, so 0β€βu by (a) and 0β€(βu)(βu)=u2 by (c).
(f) If 0β€a and 0β€b, then aβ€b if and only if a2β€b2. For the forward direction, (d) with c=a gives a2β€ab and (d) with c=b gives abβ€b2, so a2β€b2 by transitivity. Conversely, suppose a2β€b2 and, for a contradiction, that aβ€b fails. By totality bβ€a, and aξ =b. The forward direction applied to bβ€a gives b2β€a2, so a2=b2 by antisymmetry, that is (aβb)(a+b)=a2βb2=0. Since aξ =b we have aβbξ =0, so multiplying by its inverse gives a+b=0, that is a=βb. Then 0β€b gives aβ€0 by (a), so a=0 by antisymmetry, whence b=βa=0 and a=b, a contradiction. In particular, if 0β€a, 0β€b and a2=b2, then a=b.
(g)β£uβ£2=u2 for every u, because β£uβ£ is u or βu and (βu)(βu)=u2 by (c).
Claim 1. That β£xβ£ is x or βx is immediate from the definition. If 0β€x then β£xβ£=x, so 0β€β£xβ£; otherwise xβ€0 by totality, so 0β€βx=β£xβ£ by (a). If β£xβ£=0 then either β£xβ£=x, giving x=0, or β£xβ£=βx, giving βx=0 and hence x=0. Conversely 0β€0, so β£0β£=0.
Claim 2. If 0β€x fails, then xβ€0 by totality, so 0β€βx by (a); hence β£βxβ£=βx and β£xβ£=βx, and the two agree. If 0β€x and x=0, then β£βxβ£=β£0β£=0=β£xβ£. If 0β€x and xξ =0, then βxβ€0 by (a); moreover 0β€βx would force βx=0 by antisymmetry and hence x=0, so 0β€βx fails and β£βxβ£=β(βx)=x=β£xβ£.
Claim 3. If 0β€x then β£xβ£=x, so xβ€β£xβ£ by reflexivity, and ββ£xβ£=βxβ€0β€x by (a) and transitivity. If 0β€x fails then xβ€0 by totality and β£xβ£=βx, so xβ€0β€βx=β£xβ£ by (a) and transitivity, while ββ£xβ£=β(βx)=xβ€x.
Claim 4. By claim 1 we have 0β€β£xyβ£, and 0β€β£xβ£, 0β€β£yβ£, so 0β€β£xβ£β£yβ£ by the second order axiom. By (g),
Since both β£xyβ£ and β£xβ£β£yβ£ are nonnegative, (f) gives β£xyβ£=β£xβ£β£yβ£.
Claim 5. From 0β€β£yβ£ and (d) or directly by adding β£xβ£ we get β£xβ£β€β£xβ£+β£yβ£, and 0β€β£xβ£, so 0β€β£xβ£+β£yβ£ by transitivity; also 0β€β£x+yβ£ by claim 1. By (f) it suffices to prove β£x+yβ£2β€(β£xβ£+β£yβ£)2. Using (g), claim 4 and the field axioms,
By claim 3 applied to the element xy we have xyβ€β£xyβ£; adding xy and then β£xyβ£ gives xy+xyβ€β£xyβ£+β£xyβ£. Adding x2+y2 to both sides gives the required inequality.
Claim 6. Suppose β£xβ£β€c. By claim 3, xβ€β£xβ£, so xβ€c by transitivity; and βcβ€ββ£xβ£ by (b), while ββ£xβ£β€x by claim 3, so βcβ€x by transitivity. Conversely suppose βcβ€x and xβ€c. If 0β€x then β£xβ£=xβ€c. Otherwise β£xβ£=βx, and applying (b) to βcβ€x gives βxβ€c, that is β£xβ£β€c.
Claim 7. By claim 5 applied to xβy and y,
β£xβ£=β£(xβy)+yβ£β€β£xβyβ£+β£yβ£,
and adding ββ£yβ£ gives β£xβ£ββ£yβ£β€β£xβyβ£. Interchanging x and y gives β£yβ£ββ£xβ£β€β£yβxβ£, and β£yβxβ£=β£β(xβy)β£=β£xβyβ£ by claim 2. Applying (b) to β£yβ£ββ£xβ£β€β£xβyβ£ and using β(β£yβ£ββ£xβ£)=β£xβ£ββ£yβ£ yields ββ£xβyβ£β€β£xβ£ββ£yβ£. Thus ββ£xβyβ£β€β£xβ£ββ£yβ£β€β£xβyβ£, and claim 6 applied with c=β£xβyβ£ gives ββ£xβ£ββ£yβ£ββ€β£xβyβ£.
Claim 9. Suppose first that β£xβ£<c, so β£xβ£β€c and β£xβ£ξ =c. By claim 6, βcβ€x and xβ€c. If x=c, then c=xβ€β£xβ£ by claim 3, and β£xβ£β€c, so β£xβ£=c by antisymmetry, contradicting β£xβ£ξ =c; hence xξ =c and x<c. If x=βc, then ββ£xβ£β€x=βc by claim 3, so cβ€β£xβ£ by (b) together with β(βc)=c and β(ββ£xβ£)=β£xβ£; with β£xβ£β€c this gives β£xβ£=c by antisymmetry, again contradicting β£xβ£ξ =c. Hence βcξ =x and βc<x.
Conversely suppose βc<x and x<c. Then βcβ€x and xβ€c, so β£xβ£β€c by claim 6. Suppose β£xβ£=c. By claim 1, β£xβ£ equals x or βx. In the first case x=c, contradicting xξ =c; in the second βx=c, hence x=βc, contradicting βcξ =x. So β£xβ£ξ =c, and therefore β£xβ£<c.