LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28

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 : \mathbb{R} \to \mathbb{R}$ is bounded above on some nondegenerate interval, then $f(x) = f(1)\,x$ for every real $x$

Statement

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

$f(x) \;=\; f(1)\,x \qquad \text{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 $\mathbb{Q}$ to cover the whole line.

Facts & Assumptions

Given: An additive $f : \mathbb{R} \to \mathbb{R}$ , reals $p < r$ , and a real $M$ with $f(z) \le 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 $\mathbb{R} \to \mathbb{R}$ ).

[A2]

$f(z) \le M$ for every $z$ with $p \le z \le r$ , where $p < r$ (Intervals of $\mathbb{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(qx) = qf(x)$ for every rational $q$ and every real $x$ , and $f(\iota(n)x) = \iota(n)f(x)$ for every $n \in \mathbb{N}$ (An additive $f : \mathbb{R} \to \mathbb{R}$ satisfies $f(0) = 0$ , $f(-x) = -f(x)$ and $f(qx) = 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 \ge 1$ with $x < \iota(n)$ , and $\iota$ is positive and strictly increasing on the naturals $\ge 1$ (Every complete ordered field is Archimedean, For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$ , The canonical natural $\iota(n) = n \cdot 1_F$ of a field, Canonical naturals are positive and strictly increasing).

[L4]

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

Proof

technique · direct

1.1

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

A1L1construct

2.1

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

step 1.1A2L4

2.2

$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$ .

step 1.1

2.3

$g$ is identically $0$ . Suppose $g(x_{0}) \ne 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$ .

step 1.1L1

3.1

$g$ is bounded above by $M'$ on the whole of $\mathbb{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) \le M'$ .

step 2.1step 2.2L2

4.1

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

step 1.1step 3.1step 2.3L1L3L4

5.1

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

step 1.1step 4.1∎

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 : \mathbb{R} \to \mathbb{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 $\mathbb{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 $\iota(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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 64 results over 24 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click 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 : \mathbb{R} \to \mathbb{R}f:R→R is bounded above on some nondegenerate interval, then f(x)=f(1) xf(x) = f(1)\,xf(x)=f(1)x for every real xxx