LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)

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.

If an additive $f : R \to R$ is bounded above on some nondegenerate interval, then $f (x) = f (1) x$ for every real $x$

Statement

Throughout, $N \subseteq Z \subseteq Q \subseteq R$ denotes the canonical copies. Natural numbers, integers and rationals are written directly when used in real arithmetic.

Let $f : R \to R$ be additive (Cauchy's functional equation $f (x + y) = f (x) + f (y)$ , and the additive functions $R \to R$ ) and suppose there are reals $p < r$ and a real $M$ with $f (z) \leq M$ for every $z \in [p, r]$ ; that is, $f$ is bounded above on a nondegenerate interval (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, Lower bound, bounded below, bounded set). Then

$f (x) = f (1) x for every real x .$

A nondegenerate interval is all that is needed, and its position is irrelevant. Any order-convex set with two distinct points contains a closed $[p, r]$ with $p < r$ , and the hypothesis is used only through that closed interval; the argument then translates the interval along $Q$ to cover the whole line.

Facts & Assumptions

Given: An additive $f : R \to R$ , reals $p < r$ , and a real $M$ with $f (z) \leq M$ for every $z \in [p, r]$ .

[A1]

$f (x + y) = f (x) + f (y)$ for all reals $x, y$ (Cauchy's functional equation $f (x + y) = f (x) + f (y)$ , and the additive functions $R \to R$ ).

[A2]

$f (z) \leq M$ for every $z$ with $p \leq z \leq r$ , where $p < r$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, Lower bound, bounded below, bounded set).

[L1]

An additive $f$ satisfies $f (0) = 0$ , $f (- x) = - f (x)$ , $f (q x) = q f (x)$ for every rational $q$ and every real $x$ , and $f (n x) = n f (x)$ for every $n \in N$ (An additive $f : R \to R$ satisfies $f (0) = 0$ , $f (- x) = - f (x)$ and $f (q x) = q f (x)$ for every rational $q$ and every real $x$ ; in particular $f (q) = q f (1)$ at every rational $q$ ).

[L2]

Strictly between any two distinct reals there lies a rational (The rationals embed densely in the reals).

[L3]

For every real $x$ there is a natural $n \geq 1$ with $x < n$ , and the natural numbers $\geq 1$ are positive in $R$ and their order is preserved there (Every complete ordered field is Archimedean, For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, Canonical naturals are positive and strictly increasing).

[L4]

$R$ is an ordered field: sums and products of positives are positive, and $u > 0$ with $v \geq u$ gives $v > 0$ (Complete ordered field (least-upper-bound property), Basic properties of the absolute value).

Proof

technique · direct

1.1A1L1construct

Put $c : = f (1)$ and define $g : R \to R$ by $g (x) : = f (x) - c x$ . Then $g$ is additive, since both $f$ and $x \mapsto c x$ are, and $g (q) = f (q) - c q = q f (1) - c q = 0$ for every rational $q$ .

2.1step 1.1A2L4

$g$ is bounded above on $[p, r]$ : for $z \in [p, r]$ one has $g (z) = f (z) - c z \leq M + ∣ c ∣ K$ , where $K : = \max {∣ p ∣, ∣ r ∣}$ , because $∣ c z ∣ \leq ∣ c ∣ ∣ z ∣ \leq ∣ c ∣ K$ and hence $- c z \leq ∣ c ∣ K$ . Write $M^{'} : = M + ∣ c ∣ K$ for this bound.

2.2step 1.1

$g (x + q) = g (x)$ for every real $x$ and every rational $q$ : additivity gives $g (x + q) = g (x) + g (q)$ and $g (q) = 0$ .

2.3step 1.1L1

$g$ is identically $0$ . Suppose $g (x_{0}) \neq 0$ for some real $x_{0}$ . Replacing $x_{0}$ by $- x_{0}$ if necessary, which changes the sign of $g (x_{0})$ since $g (- x) = - g (x)$ , we may take $g (x_{0}) > 0$ .

3.1step 2.1step 2.2L2

$g$ is bounded above by $M^{'}$ on the whole of $R$ . Let $x$ be real. The two reals $x - r$ and $x - p$ satisfy $x - r < x - p$ , so there is a rational $q$ with $x - r < q < x - p$ ; then $p < x - q < r$ , so $x - q \in [p, r]$ and $g (x) = g ((x - q) + q) = g (x - q) \leq M^{'}$ .

4.1step 1.1step 3.1step 2.3L1L3L4

With $x_{0}$ as in step 2.3, take a natural $n \geq 1$ with $M^{'} / g (x_{0}) < n$ ; then $n g (x_{0}) > M^{'}$ . But $g (n x_{0}) = n g (x_{0}) > M^{'}$ , contradicting step 3.1. So no such $x_{0}$ exists and $g$ vanishes identically.

5.1step 1.1step 4.1∎

Therefore $f (x) = c x = f (1) x$ for every real $x$ .

Remarks

Only an upper bound is used, and only on one interval. The proof never bounds $f$ below and never uses more than the single closed interval $[p, r]$ ; the translation invariance of step 2.2 and the sliding argument of step 3.1 do the rest. A lower bound on an interval gives the same conclusion by applying the lemma to $- f$ , which is additive and bounded above there, and that is how Six regularity conditions each force an additive $f : R \to R$ to be $x \mapsto f (1) x$ : continuity at a single point, monotonicity on a nondegenerate interval, boundedness above on one, boundedness below on one, constancy of sign on one, and a graph that is not dense in $R^{2}$ obtains five of its six clauses from this one lemma, the sixth being argued separately there.
Where the Archimedean property enters. Once, in step 4.1, to make the multiples $n g (x_{0})$ exceed the bound $M^{'}$ . Over a non-Archimedean ordered field the argument fails at exactly that point, and the statement is not asserted there.

Depends on

Used by

Six regularity conditions each force an additive f : ℝ → ℝ to be x ↦ f(1)x: continuity at a single point, monotonicity on a nondegenerate interval, boundedness above on one, boundedness below on one, constancy of sign on one, and a graph that is not dense in ℝ² Theorem

Dependency tree · two levels

39 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Cauchy's functional equation (Wikipedia) (standard reference, not scraped)
Additive operators approximately preserving Birkhoff-James orthogonality (Aequationes mathematicae) (standard reference, not scraped)

If an additive f:R→Rf:R→R is bounded above on some nondegenerate interval, then f(x)=f(1) xf(x)=f(1)x for every real xx