Alphabeta Math
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 10 results · all verified · 8 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Continuity, IVT, EVT, and Uniform Continuity: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

The distance ψ(x)=d(x,Z) from a real number to the integers is 1-Lipschitz, hence uniformly continuous, takes values in [0,1/2], and vanishes exactly on Z

Example

Take R with its usual metric d(x,y)=∣x−y∣ (The absolute value makes R a metric space: d(x,y)=∣x−y∣ is a metric, its open balls are the intervals (x−r,x+r), and it is unbounded), identify Z with its canonical copy inside R (The integers as equivalence classes of pairs of naturals, The naturals embed in the integers, The integers embed in the rationals, The rationals embed densely in the reals), and let

ψ(x)  :=  d(x,Z)  =  inf⁡{ ∣x−n∣ : n∈Z }

be the distance from x to the nonempty set Z (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space). Then:

  1. ψ is 1-Lipschitz on R: ∣ψ(x)−ψ(y)∣≤∣x−y∣ for all real x,y. Consequently ψ is uniformly continuous on R (Uniform continuity of f:A→R: one δ serving every pair of points of A) and continuous on R (Continuity of f:A→R at a point of A and on A: the ε-δ condition, its agreement with lim⁡x→cf(x)=f(c) at a limit point, and continuity at an isolated point).
  2. The infimum is attained, and computed. Writing m:=⌊x⌋ for the integer part of x (Integer part: for every real x there is exactly one integer m with m≤x<m+1) and t:=x−m, so that 0≤t<1, ψ(x)  =  min⁡{ t, 1−t }  =  min⁡{ ∣x−m∣, ∣x−(m+1)∣ }, so ψ(x)=∣x−n∣ for n=m or n=m+1.
  3. Range. 0≤ψ(x)≤1/2 for every real x (Intervals of R: the nine order-convex forms, nondegeneracy, and length).
  4. Zero set. ψ(x)=0 if and only if x∈Z.

Why this example is here. It is the standard uniformly continuous function of this track that is not defined by a formula in the field operations, and it is obtained from the metric machinery rather than rebuilt: claim 1 is ∣d(x,A)−d(y,A)∣≤d(x,y), so the distance to a fixed nonempty set is 1-Lipschitz applied to A:=Z in the metric space R, transported to a statement about a real function by Dictionary: for A⊆R with the metric d(x,y)=∣x−y∣, continuity and uniform continuity of f:A→R agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of R is compact in the open-cover sense of R exactly when it is a compact metric subspace, clause 3. Only claims 2 to 4, which compute the value, need an argument of their own.

The same function is computed elsewhere, and nothing here depends on that. The trigonometry-free oscillator ψ(x)=inf⁡n∈Z∣x−n∣ is well defined and attained at a nearest integer, takes values in [0,1/2], vanishes exactly on Z, equals 1/2 at half-integers, and is 1-periodic introduces ψ on the companion page of The ε-δ limit lim⁡x→cf(x)=L of f:A→R at a limit point c of A and proves the same computation together with 1-periodicity and the value at half-integers. That item lives on an examples page, which is a leaf of the dependency graph, so no item may rest on it; the verification below is therefore self-contained, and the duplication is deliberate rather than an oversight.

Facts & Assumptions

Given: R with the metric d(x,y)=∣x−y∣; the canonical copy of Z inside R; a real x, the integer m:=⌊x⌋ and the real t:=x−m; and ψ(x):=d(x,Z).

[L1]

Distance to a nonempty set: for nonempty A⊆X in a metric space, d(x,A):=inf⁡{ d(x,a):a∈A }, the infimum existing because the set of distances is nonempty and bounded below by 0 (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, Greatest lower bound (infimum), Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric).

[L2]

∣d(x,A)−d(y,A)∣≤d(x,y): the distance to a fixed nonempty set is 1-Lipschitz as a map of metric spaces (∣d(x,A)−d(y,A)∣≤d(x,y), so the distance to a fixed nonempty set is 1-Lipschitz).

[L4]

R with d(x,y)=∣x−y∣ is a metric space (The absolute value makes R a metric space: d(x,y)=∣x−y∣ is a metric, its open balls are the intervals (x−r,x+r), and it is unbounded), and Z sits inside R as a totally ordered subring containing 0 and 1 and closed under n↦n±1, with no integer strictly between n and n+1 (The integers as equivalence classes of pairs of naturals, The naturals embed in the integers, The integers embed in the rationals, The rationals embed densely in the reals).

[L5]

Integer part: for every real x there is exactly one integer m with m≤x<m+1 (Integer part: for every real x there is exactly one integer m with m≤x<m+1).

[L6]

Infimum and minimum: a lower bound of a set that belongs to the set is its infimum and its minimum (Greatest lower bound (infimum), Maximum and minimum of a set); and the minimum of a two-element set of reals exists and is one of the two (Every nonempty finite set of reals has a maximum and a minimum).

[L7]

Absolute value and order: ∣u∣≥0; ∣u∣=0 exactly when u=0; ∣u∣=u for u≥0 and ∣u∣=−u for u≤0; the order is total; 1/2>0 and 1−1/2=1/2 (Basic properties of the absolute value, Ordered field, Intervals of R: the nine order-convex forms, nondegeneracy, and length).

Verification

technique · direct
1.1

Z is a nonempty subset of the metric space R, since 0∈Z, so ψ(x)=d(x,Z) is defined for every real x by [L1], and ψ(x)≥0.

L1L4L7
1.2

By [L5] the integer m=⌊x⌋ satisfies m≤x<m+1, so t=x−m satisfies 0≤t<1, and (m+1)−x=1−t satisfies 0<1−t≤1.

L5L7
2.1

Claim 1. By [L2], ∣ψ(x)−ψ(y)∣=∣d(x,Z)−d(y,Z)∣≤d(x,y)=∣x−y∣ for all real x,y; by [L3] this says exactly that ψ is Lipschitz with constant 1 as a real function on R, hence uniformly continuous on R and continuous on R.

step 1.1L2L3
2.2

Every distance from x to an integer is at least min⁡{t,1−t}. Let n∈Z. By [L4] and totality either n≤m or m<n, and in the second case m+1≤n. If n≤m then x−n≥x−m=t≥0, so ∣x−n∣=x−n≥t. If m+1≤n then n−x≥(m+1)−x=1−t>0, so ∣x−n∣=n−x≥1−t. Either way ∣x−n∣≥min⁡{t,1−t}.

step 1.2L4L6L7
2.3

Both candidate values occur. Since t≥0 we have t=∣x−m∣, and since 1−t>0 we have 1−t=∣x−(m+1)∣, with m and m+1 in Z.

step 1.2L4L7
3.1

Claim 2. By steps 2.2 and 2.3 the real min⁡{t,1−t} is a lower bound of { ∣x−n∣:n∈Z } belonging to that set, so by [L6] it is the infimum and the minimum: ψ(x)=min⁡{t,1−t}=min⁡{∣x−m∣,∣x−(m+1)∣}, attained at n=m or n=m+1.

step 2.2step 2.3L1L6
4.1

Claim 3. ψ(x)≥0 since t≥0 and 1−t>0. And ψ(x)≤1/2: if t≤1/2 then ψ(x)≤t≤1/2, while if t>1/2 then 1−t<1−1/2=1/2 and ψ(x)≤1−t<1/2. So 0≤ψ(x)≤1/2.

step 1.2step 3.1L7
4.2

Claim 4. If ψ(x)=0 then min⁡{t,1−t}=0 by step 3.1; since 1−t>0 this forces t=0, that is x=m∈Z. Conversely if x∈Z then ∣x−x∣=0 is a member of the set of distances and 0 is a lower bound of it by step 1.1, so ψ(x)=0 by [L6].

step 1.1step 1.2step 3.1L6L7
5.1

Claims 1 to 4 are verified: ψ is 1-Lipschitz and therefore uniformly continuous and continuous on R, its value at x is min⁡{t,1−t} and is attained at a nearest integer, its values lie in [0,1/2], and it vanishes exactly on Z.

step 2.1step 3.1step 4.1step 4.2∎

Remarks

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

The indicator of Q is continuous at no point of R

Statement refuted

Refuted claim: every function R→R is continuous at at least one point (Continuity of f:A→R at a point of A and on A: the ε-δ condition, its agreement with lim⁡x→cf(x)=f(c) at a limit point, and continuity at an isolated point).

The witness is the Dirichlet function, the indicator of the rationals: writing Q for the canonical copy of the rationals inside R (The rationals embed densely in the reals),

1Q:R→R,1Q(x):={1if x∈Q,0if x∉Q.

It is continuous at no point of R. The mechanism is that both Q and its complement are dense (Both Q and R∖Q are dense in R, and every nonempty open subset of R is uncountable), so every neighbourhood of every real contains a point of each, and the two values differ by 1.

The argument is choice free. Density is used in the form "every neighbourhood of every point meets the set", which is The closure equals the set together with its limit points, equals the set of points every neighbourhood of which meets it, and is the smallest closed superset; a set is closed iff it contains its limit points applied to a closure equal to R; no sequence is built, so neither A point lies in the closure of A⊆R iff some sequence in A converges to it, so a subset of R is closed iff it is sequentially closed nor f is continuous at c∈A if and only if f(xk)→f(c) for every sequence in A converging to c, the converse direction costing countable choice is invoked, and the countable choice those two spend is not spent here.

Facts & Assumptions

Given: The canonical copy Q⊆R of the rationals, its complement X:=R∖Q, and the function 1Q:R→R taking the value 1 on Q and 0 on X.

[L1]

Continuity at c: for every real ε>0 there is a real δ>0 with ∣1Q(x)−1Q(c)∣<ε for every real x with ∣x−c∣<δ. So continuity at c fails as soon as some real ε0>0 admits, for every real δ>0, a real x with ∣x−c∣<δ and ∣1Q(x)−1Q(c)∣≥ε0 (Continuity of f:A→R at a point of A and on A: the ε-δ condition, its agreement with lim⁡x→cf(x)=f(c) at a limit point, and continuity at an isolated point, The ε-neighbourhood and the punctured ε-neighbourhood of a point of R).

[L4]

1Q is a well-defined function: X is by definition the complement R∖Q, so every real either lies in Q or does not, exclusively; and ∣1−0∣=∣0−1∣=1, with 1/2>0 and 1/2<1 (Basic properties of the absolute value, Ordered field).

Counterexample

technique · direct
1.1

1Q is a well-defined function on R taking only the values 0 and 1, and R is the disjoint union of Q and X.

L4
1.2

Let c∈R be arbitrary, put ε0:=1/2>0, and let a real δ>0 be given.

L4
2.1

By [L2] and [L3] the neighbourhood Nδ(c) meets Q and it meets X: there are reals p∈Nδ(c)∩Q and z∈Nδ(c)∩X, so ∣p−c∣<δ and ∣z−c∣<δ, with 1Q(p)=1 and 1Q(z)=0.

step 1.2L2L3choose
3.1

If c∈Q then 1Q(c)=1 and the point x:=z satisfies ∣x−c∣<δ and ∣1Q(x)−1Q(c)∣=∣0−1∣=1≥ε0. If c∉Q then 1Q(c)=0 and the point x:=p satisfies ∣x−c∣<δ and ∣1Q(x)−1Q(c)∣=∣1−0∣=1≥ε0. By [L4] these two possibilities are exhaustive and exclusive.

step 1.1step 2.1L4
4.1

So for the fixed ε0=1/2 no real δ>0 serves at c, and by [L1] the function 1Q is not continuous at c. As c was an arbitrary real, it is continuous at no point of R, and the refuted claim is false.

step 1.2step 3.1L1∎

Remarks

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

x⋅1Q(x) is continuous at 0 and at no other point

Example

Let 1Q be the indicator of the rationals (The indicator of Q is continuous at no point of R) and put

h:R→R,h(x):=x⋅1Q(x),

so h(x)=x for rational x and h(x)=0 for irrational x. Then:

  1. h is continuous at 0 (Continuity of f:A→R at a point of A and on A: the ε-δ condition, its agreement with lim⁡x→cf(x)=f(c) at a limit point, and continuity at an isolated point);
  2. h is not continuous at any c≠0.

So the set of points of continuity of a real function can be a single point. Together with The indicator of Q is continuous at no point of R, where that set is empty, this shows how little the set of continuity points is constrained by the mere existence of the function.

The point of the example. Continuity at c compares h(x) with h(c), and the two branches of h agree only where x=0. Multiplying the indicator by x damps the jump: near 0 both branches are small, so the discrepancy is at most ∣x∣; away from 0 the discrepancy is at least ∣c∣/2 on every neighbourhood, because each branch is realised arbitrarily close to c.

Facts & Assumptions

Given: The canonical copy Q⊆R of the rationals with complement X:=R∖Q, and h:R→R with h(x)=x for x∈Q and h(x)=0 for x∈X.

[L1]

Continuity at c, in the form of Continuity of f:A→R at a point of A and on A: the ε-δ condition, its agreement with lim⁡x→cf(x)=f(c) at a limit point, and continuity at an isolated point: for every real ε>0 there is a real δ>0 with ∣h(x)−h(c)∣<ε whenever ∣x−c∣<δ; and it fails at c as soon as some real ε0>0 admits, for every real δ>0, a real x with ∣x−c∣<δ and ∣h(x)−h(c)∣≥ε0 (The ε-neighbourhood and the punctured ε-neighbourhood of a point of R).

[L3]

X is by definition the complement R∖Q, so every real lies in exactly one of Q and X; hence h is a well-defined function, and ∣h(x)∣≤∣x∣ for every real x (Basic properties of the absolute value, The indicator of Q is continuous at no point of R).

[L4]

Absolute value and order: ∣u∣≥0 and ∣u∣>0 exactly when u≠0 (Basic properties of the absolute value); the reverse triangle inequality ∣∣u∣−∣v∣∣≤∣u−v∣, hence ∣u−v∣≥∣u∣−∣v∣ (The reverse triangle inequality); and the minimum of a two-element set of reals exists and is one of the two (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set, Ordered field).

Verification

technique · direct
1.1

h is well defined and satisfies ∣h(x)∣≤∣x∣ for every real x: on Q one has ∣h(x)∣=∣x∣ and on X one has ∣h(x)∣=0≤∣x∣. Also 0∈Q, so h(0)=0.

L3L4
1.2

Claim 2, the setup. Let c≠0 be real, put ε0:=∣c∣/2>0 by [L4], and let a real δ>0 be given. Put δ′:=min⁡{δ, ∣c∣/2}>0 by [L4].

L4choose
2.1

Claim 1. Let a real ε>0 be given and take δ:=ε. Every real x with ∣x−0∣<δ satisfies ∣h(x)−h(0)∣=∣h(x)∣≤∣x∣<ε by step 1.1. So h is continuous at 0.

step 1.1L1L4
2.2

By [L2] the neighbourhood Nδ′(c) meets Q and meets X: fix p∈Nδ′(c)∩Q and z∈Nδ′(c)∩X, so ∣p−c∣<δ′≤δ and ∣z−c∣<δ′≤δ, with h(p)=p and h(z)=0.

step 1.2L2choose
3.1

The rational case. Suppose c∈Q, so h(c)=c. Take x:=z: then ∣x−c∣<δ and ∣h(x)−h(c)∣=∣0−c∣=∣c∣≥∣c∣/2=ε0.

step 1.2step 2.2L3L4
3.2

The irrational case. Suppose c∈X, so h(c)=0. Take x:=p: then ∣x−c∣<δ, and ∣p∣≥∣c∣−∣p−c∣>∣c∣−∣c∣/2=∣c∣/2 by [L4] and step 2.2, so ∣h(x)−h(c)∣=∣p∣>∣c∣/2=ε0.

step 1.2step 2.2L3L4
4.1

By [L3] the two cases of steps 3.1 and 3.2 are exhaustive, so for every real δ>0 some x with ∣x−c∣<δ has ∣h(x)−h(c)∣≥ε0; by [L1] the function h is not continuous at c. Since c≠0 was arbitrary, claim 2 holds, and with step 2.1 the set of points of continuity of h is exactly {0}.

step 2.1step 3.1step 3.2L1L3∎

Remarks

  • Where the damping factor does its work. The estimate ∣h(x)∣≤∣x∣ of step 1.1 is the whole of claim 1, and it is available only because the two branches of h agree at 0. Replacing x by any function vanishing at 0 and continuous there gives the same conclusion at 0; replacing it by a nonzero constant gives The indicator of Q is continuous at no point of R back.

  • The choice of δ′=min⁡{δ,∣c∣/2} is what makes the irrational case work. Without shrinking to ∣c∣/2 the rational point p near c could be close to 0, and then ∣h(p)−h(c)∣=∣p∣ would be small; the shrinking keeps p away from 0 by at least ∣c∣/2.

  • This example is choice free, for the same reason as The indicator of Q is continuous at no point of R: density is used only in the form "every neighbourhood meets the set", never to build a sequence.

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-07-27Open item page →

x↦1/x is continuous on (0,1) and not uniformly continuous there, the pairs 1/(k+2) and 1/(k+3) defeating every δ

Statement refuted

Refuted claim: the function f:(0,1)→R, f(x):=1/x, is uniformly continuous on (0,1) (Uniform continuity of f:A→R: one δ serving every pair of points of A, Intervals of R: the nine order-convex forms, nondegeneracy, and length).

f is continuous on (0,1) (Continuity of f:A→R at a point of A and on A: the ε-δ condition, its agreement with lim⁡x→cf(x)=f(c) at a limit point, and continuity at an isolated point) and its domain is bounded, so this is the sharpest simple instance of FALSE: every continuous real function is uniformly continuous on its domain: neither continuity nor boundedness of the domain implies uniform continuity, and what Heine-Cantor in R: a continuous real function on a compact subset of R is uniformly continuous, proved R-natively from sequential compactness actually needs is compactness, which (0,1) does not have because it is not closed (A subset of R is compact if and only if it is closed and bounded).

The refutation exhibits, for every δ>0, a pair of points of (0,1) closer than δ whose f-values differ by exactly 1. The pairs are

xk:=1k+2,yk:=1k+3(k∈N),

and the shift by 2 and 3 is not cosmetic: N contains 0 here (Sequences of reals: bounded, eventually, frequently, tails, subsequences is 0-indexed), so 1/k is undefined at k=0 and 1/(k+1) leaves (0,1) at k=0.

Facts & Assumptions

Given: The interval A:=(0,1) and the function f:A→R, f(x):=1/x. Naturals are identified with their canonical images in R.

[L1]

Uniform continuity on A fails as soon as some real ε0>0 admits, for every real δ>0, a pair x,x′∈A with ∣x−x′∣<δ and ∣f(x)−f(x′)∣≥ε0 (Uniform continuity of f:A→R: one δ serving every pair of points of A, Ordered field).

[L3]

Archimedean property in reciprocal form: for every real η>0 there is a natural m≥1 with 1/m<η; and 0<s<t implies 0<1/t<1/s (For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε, Every complete ordered field is Archimedean, Inverses of positives are positive, and reciprocation reverses order).

[L4]

Ordered-field arithmetic: for k∈N one has k+3>k+2≥2>1>0, so 0<1/(k+3)<1/(k+2)<1 and both lie in (0,1); and (k+2)(k+3)≥k+2>0 (Ordered field, Intervals of R: the nine order-convex forms, nondegeneracy, and length, Basic properties of the absolute value).

Counterexample

technique · direct
1.1

f is continuous on A=(0,1): the identity is continuous there by [L2] and satisfies x>0≠0 for every x∈A, so its reciprocal is continuous on A by [L2].

L2L4
1.2

For k∈N put xk:=1/(k+2) and yk:=1/(k+3). By [L4] both lie in A, and f(xk)=k+2, f(yk)=k+3. At the first index, k=0, this reads x0=1/2 and y0=1/3, both in (0,1).

L4
2.1

The separation of the arguments is ∣xk−yk∣=1k+2−1k+3=1(k+2)(k+3)≤1k+2, using (k+2)(k+3)≥k+2>0 and [L3]; the separation of the values is ∣f(xk)−f(yk)∣=∣(k+2)−(k+3)∣=1.

step 1.2L3L4
3.1

Put ε0:=1>0 and let a real δ>0 be given. By [L3] fix a natural m≥1 with 1/m<δ, and take k:=m. Then k+2>m>0, so 1/(k+2)<1/m<δ by [L3], and step 2.1 gives ∣xk−yk∣≤1/(k+2)<δ while ∣f(xk)−f(yk)∣=1≥ε0.

step 2.1L3choose
4.1

So no real δ>0 serves ε0=1, and by [L1] the function f is not uniformly continuous on (0,1), although by step 1.1 it is continuous there: the refuted claim is false.

step 1.1step 3.1L1L5∎

Remarks

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

x↦x2 is continuous on R and not uniformly continuous, the pairs k+1 and k+1+1/(k+1) defeating every δ

Statement refuted

Refuted claim: the function f:R→R, f(x):=x2 (Integer powers am), is uniformly continuous on R (Uniform continuity of f:A→R: one δ serving every pair of points of A).

f is continuous on R (Continuity of f:A→R at a point of A and on A: the ε-δ condition, its agreement with lim⁡x→cf(x)=f(c) at a limit point, and continuity at an isolated point) and R is a closed subset of itself, so this is the complement of x↦1/x is continuous on (0,1) and not uniformly continuous there, the pairs 1/(k+2) and 1/(k+3) defeating every δ: there the domain was bounded and not closed, here it is closed and not bounded, and uniform continuity fails in both cases. Neither half of compactness suffices on its own, and Heine-Cantor in R: a continuous real function on a compact subset of R is uniformly continuous, proved R-natively from sequential compactness needs both (A subset of R is compact if and only if it is closed and bounded).

The refutation exhibits, for every δ>0, a pair of reals closer than δ whose squares differ by more than 2. The pairs are

ak:=k+1,bk:=k+1+1k+1(k∈N),

and the shift by 1 is not cosmetic: N contains 0 here (Sequences of reals: bounded, eventually, frequently, tails, subsequences is 0-indexed), so the reciprocal 1/k would be undefined at the first index.

Facts & Assumptions

Given: The function f:R→R, f(x):=x2. Naturals are identified with their canonical images in R.

[L1]

Uniform continuity on R fails as soon as some real ε0>0 admits, for every real δ>0, a pair x,x′∈R with ∣x−x′∣<δ and ∣f(x)−f(x′)∣≥ε0 (Uniform continuity of f:A→R: one δ serving every pair of points of A, Ordered field).

[L3]

Archimedean property in reciprocal form: for every real η>0 there is a natural m≥1 with 1/m<η; and 0<s<t implies 0<1/t<1/s (For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε, Every complete ordered field is Archimedean, Inverses of positives are positive, and reciprocation reverses order).

[L4]

Ordered-field arithmetic: for k∈N one has k+1≥1>0, so 1/(k+1) is defined and positive; the identity v2−u2=(v−u)(v+u); and ∣u∣≥0 with ∣u∣=u for u≥0 (Ordered field, Basic properties of the absolute value, Integer powers am).

Counterexample

technique · direct
1.1

f is continuous on R, being a polynomial function.

L2
1.2

For k∈N put ak:=k+1 and bk:=(k+1)+1/(k+1), both defined because k+1≥1>0 by [L4]. At the first index, k=0, this reads a0=1 and b0=2.

L4
2.1

The separation of the arguments is ∣ak−bk∣=1/(k+1). The separation of the values is, by [L4], ∣f(bk)−f(ak)∣=∣bk−ak∣ (bk+ak)=1k+1(2(k+1)+1k+1)=2+1(k+1)2>2.

step 1.2L4
3.1

Put ε0:=2>0 and let a real δ>0 be given. By [L3] fix a natural m≥1 with 1/m<δ and take k:=m; then k+1>m>0, so ∣ak−bk∣=1/(k+1)<1/m<δ by [L3], while step 2.1 gives ∣f(ak)−f(bk)∣>2=ε0.

step 2.1L3choose
4.1

So no real δ>0 serves ε0=2, and by [L1] the function f is not uniformly continuous on R, although by step 1.1 it is continuous there: the refuted claim is false.

step 1.1step 3.1L1L5∎

Remarks

ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27↗ rests on later materialOpen item page →

On [0,1] the function xβ is β-Hölder and is α-Hölder for no rational α>β, so the Hölder classes are strictly nested

Example

Let β∈Q with 0<β≤1 (Order on the rationals) and let

fβ:[0,1]→R,fβ(x):=xβ

be the rational power of a nonnegative base (Rational powers ar of a positive base, with the convention 0β=0), on the closed bounded interval [0,1] (Intervals of R: the nine order-convex forms, nondegeneracy, and length). Hölder conditions for a real function on [0,1] are the metric ones instantiated, by Dictionary: for A⊆R with the metric d(x,y)=∣x−y∣, continuity and uniform continuity of f:A→R agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of R is compact in the open-cover sense of R exactly when it is a compact metric subspace, clause 4: g is γ-Hölder with constant C when ∣g(x)−g(y)∣≤C ∣x−y∣γ for all x,y∈[0,1] (Lipschitz map, α-Hölder map for rational 0<α≤1, and contraction). Then:

  1. fβ is β-Hölder with constant 1: ∣xβ−yβ∣  ≤  ∣x−y∣βfor all x,y∈[0,1].
  2. fβ is α-Hölder for no rational α with β<α≤1: for such an α there is no real C≥0 with ∣xβ−yβ∣≤C∣x−y∣α throughout [0,1].
  3. The classes are nested: if 0<β<α≤1 are rational and g:[0,1]→R is α-Hölder with constant C, then g is β-Hölder with the same constant C.
  4. Hence the nesting is strict, at every pair of rational exponents 0<β<α≤1: the α-Hölder functions on [0,1] form a proper subclass of the β-Hölder ones, fβ lying in the second and not the first. Taking α=1: for rational 0<β<1 the function fβ is uniformly continuous on [0,1] (Uniform continuity of f:A→R: one δ serving every pair of points of A) and is not Lipschitz.

What this witnesses. Contraction implies Lipschitz implies uniformly continuous implies continuous; every Hölder map is uniformly continuous, and a Lipschitz map on a bounded space is Hölder for every exponent asserts Lipschitz ⇒ uniformly continuous ⇒ continuous and α-Hölder ⇒ uniformly continuous, and claims no converse; it says so explicitly. This item supplies the missing witnesses on the real line, and it is one of the two named in the remarks of Dictionary: for A⊆R with the metric d(x,y)=∣x−y∣, continuity and uniform continuity of f:A→R agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of R is compact in the open-cover sense of R exactly when it is a compact metric subspace. The other is x↦1/x is continuous on (0,1) and not uniformly continuous there, the pairs 1/(k+2) and 1/(k+3) defeating every δ, which separates continuity from uniform continuity.

Why the exponents are rational. Rational powers ar of a positive base is the exponent theory available at this page's position in the reading order, so the example is stated for rational exponents. The later Real powers for positive bases, with the zero-base positive-exponent convention ↗ supplies real exponents; the restriction here belongs to the local toolkit, not to the Hölder notion. Exponents above 1 are excluded there for a reason of substance: they force constancy (If ∣f(x)−f(y)∣≤C∣x−y∣α on an interval for some rational α>1 then f is constant).

Facts & Assumptions

Given: A rational β with 0<β≤1, the interval [0,1], and fβ(x)=xβ. Naturals are identified with their canonical images in R.

[L1]

Rational powers: ar is defined for a>0 and r∈Q, with a1=a and aq/1=aq agreeing with the integer power; 0r=0 for rational r>0; and 1r=1 (Rational powers ar of a positive base, Existence and uniqueness of n-th roots: a unique a1/n≥0 with (a1/n)n=a, Integer powers am, Monotonicity of r↦ar and of a↦ar).

[L2]

Laws of rational exponents for a,b>0 and r,s∈Q: ar>0; ar+s=aras; (ab)r=arbr; a−r=1/ar; (ar)s=ars. The product law persists for a,b≥0 when r>0 (Laws of rational exponents).

[L3]

Monotonicity: for 0<a<1 and rationals r<s one has ar>as; for a>1 and r<s one has ar<as; for a=1 all powers are 1; and for rational r>0 and 0<a<b one has ar<br (Monotonicity of r↦ar and of a↦ar).

[L5]

Archimedean property: for every real η>0 there is a natural q≥1 with 1/q<η, and for every real t a natural n with t<n; and 0<s<t implies 0<1/t<1/s (For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε, Every complete ordered field is Archimedean, Inverses of positives are positive, and reciprocation reverses order).

[L6]

Absolute value and order in R: ∣u∣≥0; ∣u∣=u for u≥0; the order is total, so two points of [0,1] may be named so that one is ≤ the other; and [0,1]={ x:0≤x≤1 } (Basic properties of the absolute value, Ordered field, Intervals of R: the nine order-convex forms, nondegeneracy, and length).

Verification

technique · direct
1.1

For 0≤t≤1 one has tβ≥t. If t=0 then tβ=0=t by [L1]; if t=1 then tβ=1=t by [L1]. If 0<t<1 then, when β<1, [L3] with r:=β<s:=1 gives tβ>t1=t, and when β=1 it is an equality.

L1L3L6
1.2

Claim 3. Let 0<β<α≤1 be rational and let g satisfy ∣g(x)−g(y)∣≤C∣x−y∣α on [0,1]. For x,y∈[0,1] put a:=∣x−y∣, so 0≤a≤1 by [L6]. If a=0 then aα=aβ=0 by [L1]; if a=1 then both are 1 by [L1]; and if 0<a<1 then [L3] with r:=β<s:=α gives aα<aβ. In every case aα≤aβ, so ∣g(x)−g(y)∣≤Caα≤Caβ and g is β-Hölder with the same constant.

L1L3L4L6
1.3

Claim 2, the setup. Let α∈Q with β<α≤1 and suppose, for contradiction, that some real C≥0 satisfies ∣xβ−yβ∣≤C∣x−y∣α for all x,y∈[0,1]. Taking x:=1 and y:=0 gives 1=∣1−0∣≤C⋅1=C by [L1], so C≥1>0. Taking y:=0 and an arbitrary x with 0<x≤1 gives xβ≤Cxα.

L1L6
2.1

Subadditivity: (u+v)β≤uβ+vβ for all reals u,v≥0. If u+v=0 then u=v=0 and both sides are 0 by [L1]. Otherwise put s:=u+v>0, p:=u/s and q:=v/s, so p,q≥0 and p+q=1, whence 0≤p≤1 and 0≤q≤1. By step 1.1, pβ≥p and qβ≥q, so pβ+qβ≥p+q=1. By the product law of [L2], valid for nonnegative bases since β>0, uβ=(ps)β=pβsβ and vβ=qβsβ; hence uβ+vβ=(pβ+qβ)sβ≥sβ=(u+v)β, using sβ>0 from [L2].

step 1.1L1L2L6
2.2

Claim 2, the estimate. Put γ:=α−β, a rational with γ>0. For 0<x≤1, dividing the inequality of step 1.3 by xα>0 and using [L2] gives xβ−α=xβx−α≤C, that is 1/xγ≤C and hence xγ≥1/C>0 by [L5]. Applying this at x:=1/n for a natural n≥1, and using (1/n)γ=1/nγ from [L2], gives nγ≤C for every natural n≥1.

step 1.3L2L5
3.1

Claim 1. Let x,y∈[0,1]; by [L6] name them so that y≤x. Put u:=y≥0 and v:=x−y≥0, so x=u+v. By step 2.1, xβ≤yβ+(x−y)β, that is xβ−yβ≤(x−y)β=∣x−y∣β. Also yβ≤xβ: for y=0 this reads 0≤xβ by [L1] and [L2], and for 0<y≤x it is [L3] with the exponent β>0, together with equality when y=x. Hence ∣xβ−yβ∣=xβ−yβ≤∣x−y∣β, so fβ is β-Hölder with constant 1.

step 2.1L1L2L3L4L6
3.2

Claim 2, the contradiction. By [L5] fix a natural q≥1 with 1/q<γ, and then a natural n with Cq<n; since Cq>0 we have n≥1, and since C≥1 we have Cq≥1 and so n>1. By [L3] with the exponent 1/q>0 applied to the bases Cq<n, and by (Cq)1/q=Cq⋅(1/q)=C1=C from [L1] and [L2], we get n1/q>C; and by [L3] with the base n>1 and the exponents 1/q<γ we get nγ>n1/q>C. That contradicts step 2.2, so no such C exists and claim 2 holds.

step 2.2L1L2L3L5
4.1

Claim 4. Let 0<β<α≤1 be rational. Every α-Hölder function on [0,1] is β-Hölder by step 1.2, and fβ is β-Hölder by step 3.1 and not α-Hölder by step 3.2; so the inclusion of classes is proper. With α:=1 and 0<β<1: fβ is β-Hölder, hence uniformly continuous on [0,1] by [L4], and it is not 1-Hölder, that is not Lipschitz.

step 3.1step 1.2step 3.2L4∎

Remarks

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passverified 2026-08-09 (gpt-5.6-terra-codex-subscription)Open item page →

The identity is uniformly continuous on R and its square is not, so uniform continuity is not preserved by products

Statement refuted

Refuted claim: if f,g:A→R are uniformly continuous on A⊆R (Uniform continuity of f:A→R: one δ serving every pair of points of A) then so is their pointwise product fg.

The witness is the simplest possible one: A:=R and f=g=id, the identity. The identity is uniformly continuous on R — one may take δ:=ε — and its product with itself is x↦x2, which is not uniformly continuous on R (x↦x2 is continuous on R and not uniformly continuous, the pairs k+1 and k+1+1/(k+1) defeating every δ).

The contrast with continuity is the point. Products do preserve continuity, with no hypothesis at all (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function). The reason the proof there does not transfer is visible in the estimate: bounding ∣f(x)g(x)−f(x′)g(x′)∣ requires a bound on the values of f and g near the two points, and for continuity that bound is local, supplied afresh at each point, whereas uniform continuity would need one bound valid on the whole domain. On an unbounded domain no such bound need exist.

Facts & Assumptions

Given: The domain A:=R, the identity id:R→R, id(x)=x, and its square x↦x2 (Integer powers am).

[L1]

Uniform continuity on A: for every real ε>0 there is a real δ>0 such that all x,x′∈A with ∣x−x′∣<δ satisfy ∣h(x)−h(x′)∣<ε (Uniform continuity of f:A→R: one δ serving every pair of points of A).

[L4]

Absolute value and order: ∣u∣≥0 and ∣u∣=0 exactly when u=0; the order is total (Basic properties of the absolute value, Ordered field).

Counterexample

technique · direct
1.1

The identity is uniformly continuous on R: given a real ε>0, take δ:=ε; then all x,x′∈R with ∣x−x′∣<δ satisfy ∣id(x)−id(x′)∣=∣x−x′∣<ε.

L1L4
1.2

The pointwise product of the identity with itself is the function x↦x2.

L3
1.3

By [L2] the function x↦x2 is not uniformly continuous on R.

L2
2.1

So f:=id and g:=id are uniformly continuous on A=R while fg is not: the refuted claim is false.

step 1.1step 1.2step 1.3L1∎

Remarks

  • Where the implication survives. On a bounded domain the product of two uniformly continuous functions is uniformly continuous, because each factor is then bounded: a uniformly continuous function on a bounded set is bounded, and the estimate ∣fg−f′g′∣≤∣f∣ ∣g−g′∣+∣g′∣ ∣f−f′∣ closes. Nothing on this page asserts that, and it is not used anywhere here; the witness above shows only that the unrestricted claim fails.

  • Sums and scalar multiples are safe. If f and g are uniformly continuous on A then so are f+g and αf, by the same ε/2 and ε/∣α∣ arguments that work for continuity, with the δ's inherited uniformly. It is only the product, and the quotient, that need a bound on values.

  • A second witness on a bounded domain. x↦1/x is not uniformly continuous on (0,1) (x↦1/x is continuous on (0,1) and not uniformly continuous there, the pairs 1/(k+2) and 1/(k+3) defeating every δ) although the identity is; that failure is a quotient rather than a product, and it shows that boundedness of the domain does not rescue every algebraic operation.

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-07-27verified 2026-09-09 (gpt-6-astra)Open item page →

The identity on (0,1) is bounded with no greatest value, and on [0,∞) it is continuous and unbounded

Statement refuted

Refuted claim: for the conclusions of the extreme value theorem it is enough that the domain be bounded, or that it be closed; that is, a continuous real function on a bounded domain attains a greatest value, and a continuous real function on a closed domain is bounded (Continuity of f:A→R at a point of A and on A: the ε-δ condition, its agreement with lim⁡x→cf(x)=f(c) at a limit point, and continuity at an isolated point, Lower bound, bounded below, bounded set, Maximum and minimum of a set).

Both halves are false, and one function refutes both:

  • on E1:=(0,1), which is bounded and not closed, the identity is continuous and bounded, sup⁡ of its image exists and equals 1, and no point of E1 attains it;
  • on E2:=[0,∞), which is closed and not bounded, the identity is continuous and unbounded.

Neither E1 nor E2 is compact (A subset of R is compact if and only if it is closed and bounded), so Extreme value theorem: a continuous real function on a nonempty compact subset of R attains a greatest and a least value does not apply to either, and both are instances of Rudin 4.20, the sharp converse: on a noncompact E⊆R there is an unbounded continuous function and a bounded continuous function with no greatest value, and if E is bounded there is a continuous function on E that is not uniformly continuous: the first is its bounded-not-closed case, the second its unbounded case. Together they show that neither half of "closed and bounded" can be dropped.

This item is the worked witness for FALSE: a continuous real function on a bounded domain attains a greatest value, which refutes the first half alone.

Facts & Assumptions

Given: The sets E1:=(0,1) and E2:=[0,∞) (Intervals of R: the nine order-convex forms, nondegeneracy, and length) and the identity id(x)=x on each of them.

[L2]

A greatest value of h on E is a point p∈E with h(x)≤h(p) for every x∈E; a set is bounded when it lies between two reals (Maximum and minimum of a set, Lower bound, bounded below, bounded set).

[L3]

Suprema: a nonempty set bounded above has a least upper bound, and for u=sup⁡S every real ε>0 admits s∈S with u−ε<s (Complete ordered field (least-upper-bound property), Epsilon characterisation of the supremum).

[L4]

Archimedean property: for every real t there is a natural n≥1 with t<n (Every complete ordered field is Archimedean).

[L5]

Ordered-field arithmetic: for 0<x<1 one has x<(x+1)/2<1; the maximum of a two-element set of reals exists and is one of them; and n≥1>0 for a natural n≥1 (Ordered field, Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

Counterexample

technique · direct
1.1

The identity is continuous on E1 and on E2 by [L1], and E1 is bounded while E2 is closed, by [L6].

L1L6
1.2

On E1 the identity is bounded. Every x∈(0,1) satisfies 0≤x≤1, so the image id[E1]=E1 lies between 0 and 1 and is bounded by [L2].

L5L2
1.3

On E2 the identity is unbounded. Let a real M be given. By [L4] there is a natural n≥1 with M<n, and n≥0 so n∈[0,∞)=E2 with id(n)=n>M. So no real bounds id[E2] above, and by [L2] the identity is unbounded on E2.

L2L4L5
2.1

On E1 there is no greatest value. Let p∈E1, so 0<p<1. By [L5] the point p′:=(p+1)/2 satisfies p<p′<1 and p′>0, so p′∈E1 and id(p′)=p′>p=id(p). Hence no p∈E1 satisfies id(x)≤id(p) for every x∈E1, and by [L2] the identity attains no greatest value on E1.

step 1.2L2L5
3.1

The supremum exists and equals 1. By step 1.2 and [L3] the nonempty set id[E1]=(0,1) has a least upper bound u, and u≤1 since 1 bounds it above. For a real ε>0 the point x:=max⁡{1/2, 1−ε/2} lies in (0,1) by [L5] and satisfies x>1−ε, so no real below 1 bounds (0,1) above; hence u=1. By step 2.1 no point of E1 has value 1, so the supremum is not attained.

step 1.2step 2.1L3L5
4.1

So on the bounded set E1 a continuous function attains no greatest value, and on the closed set E2 a continuous function is unbounded: both halves of the refuted claim are false, and by [L6] neither domain is compact, so no conflict with Extreme value theorem: a continuous real function on a nonempty compact subset of R attains a greatest and a least value arises.

step 1.1step 2.1step 3.1step 1.3L6∎

Remarks

ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

The intermediate value theorem gives a second proof that every nonnegative real has an n-th root, applied to xn on a closed bounded interval

Example

Let a∈R with a≥0 and let n∈N with n≥1. Put M:=a+1 and consider

f:[0,M]→R,f(x):=xn

(Integer powers am, Intervals of R: the nine order-convex forms, nondegeneracy, and length). Then f is continuous on [0,M], f(0)=0≤a≤Mn=f(M), and the intermediate value theorem (Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on [a,b] takes every value between f(a) and f(b)) supplies c∈[0,M] with

cn=a.

Moreover c is the only nonnegative real with this property, so c=a1/n in the notation of Existence and uniqueness of n-th roots: a unique a1/n≥0 with (a1/n)n=a.

This is a second proof of an existing theorem, not a new one. Existence and uniqueness of n-th roots: a unique a1/n≥0 with (a1/n)n=a already proves existence and uniqueness of n-th roots, by an argument that runs directly from the least-upper-bound property and the factorisation of bn−an; it is the item the rest of the library cites, and no second identifier is minted for the same statement. What is recorded here is that the intermediate value theorem gives the existence half in three lines once continuity of x↦xn is available, which is the standard modern route and the reason the theorem is usually met in this form.

No circularity. Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on [a,b] takes every value between f(a) and f(b) rests on A nested sequence of nonempty closed bounded intervals has nonempty intersection, and the intersection is a single point exactly when the lengths tend to 0, on the algebra of continuous functions and on the sequential criterion, none of which uses n-th roots; and the uniqueness half below is Monotonicity of x↦xn and of n↦an, which is pure ordered-field arithmetic. So this argument could have been the library's definition of a1/n; it is not, only because the roots were needed at order 16, long before continuity existed.

Facts & Assumptions

Given: A real a≥0, a natural n≥1, and M:=a+1; the function f(x)=xn on [0,M].

[L2]

Intermediate value theorem: for u≤v, a function continuous on [u,v] takes every value between f(u) and f(v) (Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on [a,b] takes every value between f(a) and f(b)).

[L3]

Powers and order: 0n=0 for n≥1; if t≥1 and n≥1 then tn≥t; and x↦xn is strictly increasing on the nonnegative reals for n≥1, hence injective there (Monotonicity of x↦xn and of n↦an, Integer powers am).

[L4]

Existence and uniqueness of n-th roots: for a≥0 and n≥1 there is a unique s≥0 with sn=a, written a1/n (Existence and uniqueness of n-th roots: a unique a1/n≥0 with (a1/n)n=a).

[L5]

Ordered-field arithmetic: a≥0 gives M=a+1≥1>0 and M>a; and 0≤M (Ordered field, Complete ordered field (least-upper-bound property)).

Verification

technique · direct
1.1

M=a+1≥1>0 by [L5], so [0,M] is a nonempty closed bounded interval, and f is continuous on it by [L1].

L1L5
1.2

f(0)=0n=0≤a by [L3] and the hypothesis a≥0; and f(M)=Mn≥M=a+1>a by [L3] and [L5]. So f(0)≤a≤f(M).

L3L5
2.1

By [L2] applied on [0,M] with the value a, there is c∈[0,M] with cn=a; in particular c≥0.

step 1.1step 1.2L2choose
3.1

c is the only nonnegative real with cn=a: by [L3] the map t↦tn is injective on the nonnegative reals, so two nonnegative solutions would coincide. Hence c=a1/n in the notation of [L4], and the existence half of [L4] has been re-proved from the intermediate value theorem.

step 2.1L3L4∎

Remarks

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

A worked fixed point on [1,2] for the map x↦(x+2/x)/2, from the one-dimensional fixed point theorem

Example

Let

φ:[1,2]→R,φ(x):=12(x+2x)

(Intervals of R: the nine order-convex forms, nondegeneracy, and length). Then:

  1. φ is continuous on [1,2] (Continuity of f:A→R at a point of A and on A: the ε-δ condition, its agreement with lim⁡x→cf(x)=f(c) at a limit point, and continuity at an isolated point);
  2. φ(x)∈[1,2] for every x∈[1,2];
  3. by Every continuous map of a closed bounded interval into itself has a fixed point, φ has a fixed point in [1,2]; and
  4. that fixed point is unique and equals 2=21/2 (Existence and uniqueness of n-th roots: a unique a1/n≥0 with (a1/n)n=a).

What the example is for. It is the smallest nontrivial instance of the one-dimensional fixed point theorem in which the fixed point can be named, and it shows that the theorem, which asserts existence only, may be combined with an algebraic identity to pin the point down. The identity is elementary: φ(c)=c says c+2/c=2c, that is c2=2.

No derivative is used, and none is available at this point in the reading order. The usual argument that φ maps [1,2] into itself computes the minimum of φ by differentiation; the two-line order estimate of step 1.2 below replaces it. The same map is treated as a contraction of [1,2] in The map x↦(x+2/x)/2 is a contraction of [1,2] with fixed point 2, and the a priori bound gives the error after n steps, where the Banach fixed point theorem gives the same point together with an error bound after n iterations; that route needs completeness of the metric subspace, this one needs only the intermediate value theorem.

Facts & Assumptions

Given: The interval [1,2] and the function φ(x)=12(x+2/x) on it.

[L2]

One-dimensional fixed point theorem: a continuous φ:[a,b]→R with a≤b and φ(x)∈[a,b] for all x∈[a,b] has a fixed point in [a,b] (Every continuous map of a closed bounded interval into itself has a fixed point, Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on [a,b] takes every value between f(a) and f(b)).

[L3]

Reciprocals and order: for 1≤x≤2 one has 0<x, hence 1/2≤1/x≤1 and so 1≤2/x≤2 (Inverses of positives are positive, and reciprocation reverses order, Ordered field).

[L4]

Square roots: for a≥0 there is a unique s≥0 with s2=a, written a1/2=a; and t↦t2 is strictly increasing on the nonnegative reals (Existence and uniqueness of n-th roots: a unique a1/n≥0 with (a1/n)n=a, Monotonicity of x↦xn and of n↦an, Integer powers am).

[L5]

Ordered-field arithmetic: 1≤2; halving preserves order; and 12=1≤2≤4=22 (Ordered field, Complete ordered field (least-upper-bound property), Integer powers am).

Verification

technique · direct
1.1

Claim 1. On [1,2] the identity is continuous and does not vanish, since x≥1>0; so x↦2/x is continuous there by [L1], and φ=12(id+2/id) is continuous on [1,2] as a scalar multiple of a sum of continuous functions.

L1L3
1.2

Claim 2. Let x∈[1,2]. By [L3] we have 1≤2/x≤2, and by hypothesis 1≤x≤2; adding, 2≤x+2/x≤4, and halving gives 1≤φ(x)≤2 by [L5]. So φ(x)∈[1,2].

L3L5
2.1

Claim 3. By [L2], applied with a:=1, b:=2 and the map φ, which is continuous by step 1.1 and maps [1,2] into itself by step 1.2, there is c∈[1,2] with φ(c)=c.

step 1.1step 1.2L2choose
3.1

Every fixed point squares to 2. Let c∈[1,2] satisfy φ(c)=c. Then c≥1>0, so multiplying 12(c+2/c)=c by 2c gives c2+2=2c2, that is c2=2.

step 2.1L3L5
4.1

Claim 4. By [L4] there is exactly one nonnegative real whose square is 2, namely 2; since every fixed point c is ≥1>0 and satisfies c2=2 by step 3.1, the fixed point is unique and equals 2. And 2 does lie in [1,2]: from 12=1≤2≤4=22 and the strict monotonicity of t↦t2 on the nonnegative reals ([L4], [L5]) one gets 1≤2≤2.

step 3.1L4L5∎

Remarks

  • A sharper bound, from a square. For x>0 one has (x−2/x)2≥0, and expanding gives x+2/x≥22, so φ(x)≥2 for every x>0. That is the same identity The map x↦(x+2/x)/2 is a contraction of [1,2] with fixed point 2, and the a priori bound gives the error after n steps uses, and it shows that φ maps (0,∞) into [2,∞); the crude estimate of step 1.2 is all that claim 2 needs, and it avoids square roots entirely.

  • Existence and identification are separate steps. Every continuous map of a closed bounded interval into itself has a fixed point gives claim 3 with no information about where the point is; claim 4 is pure algebra and would be equally valid if no fixed point existed, since it only says which number a fixed point must be. It is the combination that names 2.

  • The interval matters. On [−2,−1] the same formula has the fixed point −2, and on an interval straddling 0 the map is not even defined. Choosing [1,2] is what makes claim 2 true and isolates the positive root.

Sources