TheoremStatement: AI-adaptedProof: AI-adaptedprecheck 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.

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

Statement

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 put $c : = f (1)$ . Write $R^{2}$ for the set of functions $2 \to R$ with the metric $d_{\infty} ((a, b), (a^{'}, b^{'})) = \max {∣ a - a^{'} ∣, ∣ b - b^{'} ∣}$ ( $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it, Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric), and let

$Γ : = {(x, f (x)) : x \in R} \subseteq R^{2}$

be the graph of $f$ . If any one of the following six conditions holds, then $f (x) = c x$ for every real $x$ .

$f$ is continuous at some single point of $R$ (Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point).
$f$ is monotone on some nondegenerate interval (Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $R$ , with the dictionary to monotone sequences, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).
$f$ is bounded above on some nondegenerate interval (Lower bound, bounded below, bounded set).
$f$ is bounded below on some nondegenerate interval.
$f$ has constant sign on some nondegenerate interval $I$ : either $f (z) \geq 0$ for every $z \in I$ , or $f (z) \leq 0$ for every $z \in I$ .
$Γ$ is not dense in $R^{2}$ (Interior, closure, boundary, limit point, isolated point and dense subset of a metric space).

Conditions 3, 4 and 5 are not independent, and the proof does not pretend they are. Condition 5 is the special case of 3 or of 4 with the bound $0$ , and condition 4 is condition 3 applied to $- f$ ; they are listed separately only because each is the form in which the hypothesis usually arises. Condition 1 and condition 2 are each reduced to condition 3 in one line. Condition 6 is the only one that is not, and it is proved in the contrapositive: if $f$ is not of the form $x \mapsto c x$ , then $Γ$ is dense.

Two classical clauses are absent. Boundedness on a set of positive measure and Lebesgue measurability also force linearity, and neither is stated here: both require a measure, and this library develops none as it stands. Each is an independent sufficient condition, so restoring them would change nothing else on this page.

Facts & Assumptions

Given: An additive $f : R \to R$ with $c : = f (1)$ , and its graph $Γ = {(x, f (x)) : x \in 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$ ).

[L1]

An additive $f$ satisfies $f (0) = 0$ , $f (- x) = - f (x)$ and $f (q x) = q f (x)$ for every rational $q$ and every real $x$ (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]

If an additive $g$ is bounded above on some $[p, r]$ with $p < r$ , then $g (x) = g (1) x$ for every real $x$ (If an additive $f : R \to R$ is bounded above on some nondegenerate interval, then $f (x) = f (1) x$ for every real $x$ ).

[L3]

A nondegenerate interval contains a closed $[p, r]$ with $p < r$ , by order-convexity (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L4]

$f$ continuous at $c_{0}$ means: for every real $ε > 0$ there is a real $δ > 0$ with $∣ f (x) - f (c_{0}) ∣ < ε$ whenever $∣ x - c_{0} ∣ < δ$ ; and $∣ u ∣ < ε$ gives $u < ε$ (Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point, The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ , Basic properties of the absolute value).

[L5]

$f$ nondecreasing on $I$ means $f (x) \leq f (y)$ for $x \leq y$ in $I$ , and nonincreasing means $f (x) \geq f (y)$ ; monotone means one of the two (Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $R$ , with the dictionary to monotone sequences).

[L6]

$d_{\infty}$ is a metric on $R^{2}$ and its open ball of centre $(a, b)$ and radius $ε$ is ${(u, v) : ∣ u - a ∣ < ε and ∣ v - b ∣ < ε}$ ; a subset $S$ of a metric space is dense exactly when every open ball meets $S$ ( $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it, Open ball, closed ball and sphere in a metric space, Interior, closure, boundary, limit point, isolated point and dense subset of a metric space, The closure of a nonempty $A$ is ${x : d (x, A) = 0}$ , equals $A$ together with its limit points, and is the smallest closed superset).

[L7]

Strictly between any two distinct reals there lies a rational; $R$ is a field, so a nonzero real is invertible (The rationals embed densely in the reals, Complete ordered field (least-upper-bound property), For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

Proof

technique · cases

1.1

Assume at least one of the six conditions holds. The six steps below treat the six conditions in turn and are exhaustive for that assumption; in each the conclusion reached is $f (x) = c x$ for every real $x$ .

construct

2.1

Condition 3. If $f$ is bounded above on a nondegenerate interval, that interval contains a closed $[p, r]$ with $p < r$ on which $f$ is bounded above, and the boundedness lemma gives $f (x) = f (1) x = c x$ for every real $x$ .

step 1.1L2L3assume-case above

2.2

Condition 6, in the contrapositive: if $f$ is not $x \mapsto c x$ then $Γ$ is dense in $R^{2}$ . Suppose $f (x_{2}) \neq c x_{2}$ for some real $x_{2}$ . Then $x_{2} \neq 0$ , since $f (0) = 0$ . Put $x_{1} : = 1$ , $v_{1} : = (x_{1}, f (x_{1})) = (1, c)$ and $v_{2} : = (x_{2}, f (x_{2}))$ , and put $Δ : = x_{1} f (x_{2}) - x_{2} f (x_{1}) = f (x_{2}) - c x_{2}$ , which is nonzero by assumption.

step 1.1L1assume-case graph

3.1

Condition 4. If $f$ is bounded below on a nondegenerate interval $I$ , say $f (z) \geq m$ for $z \in I$ , then $- f$ is additive and satisfies $- f (z) \leq - m$ on $I$ , so $- f$ is bounded above on $I$ ; by step 2.1 applied to $- f$ we get $- f (x) = (- f) (1) x = - c x$ , hence $f (x) = c x$ .

step 2.1A1assume-case below

3.2

Condition 2. Let $f$ be monotone on a nondegenerate interval, which contains $[p, r]$ with $p < r$ . If $f$ is nondecreasing there then $f (z) \leq f (r)$ for every $z \in [p, r]$ , and if $f$ is nonincreasing there then $f (z) \leq f (p)$ ; either way $f$ is bounded above on $[p, r]$ and step 2.1 applies.

step 2.1L3L5assume-case mono

3.3

Condition 1. Let $f$ be continuous at a point $c_{0}$ . Taking $ε : = 1$ gives a real $δ > 0$ with $∣ f (x) - f (c_{0}) ∣ < 1$ , hence $f (x) < f (c_{0}) + 1$ , for every $x$ with $∣ x - c_{0} ∣ < δ$ . The set of such $x$ is the nondegenerate interval $(c_{0} - δ, c_{0} + δ)$ , so $f$ is bounded above on a nondegenerate interval and step 2.1 applies.

step 2.1L3L4assume-case cont

3.4

Let $(a, b) \in R^{2}$ and let $ε > 0$ be real. Put $α : = (a f (x_{2}) - b x_{2}) / Δ$ and $β : = (b x_{1} - a f (x_{1})) / Δ$ . Then $α x_{1} + β x_{2} = a$ and $α f (x_{1}) + β f (x_{2}) = b$ , as multiplying out and cancelling $Δ$ shows in each case.

step 2.2L7

4.1

Condition 5. If $f (z) \geq 0$ for every $z$ in a nondegenerate interval $I$ then $f$ is bounded below on $I$ by $0$ and step 3.1 applies; if $f (z) \leq 0$ for every $z \in I$ then $f$ is bounded above on $I$ by $0$ and step 2.1 applies. So sign-constancy is a special case of the two preceding conditions and needs no separate argument.

step 2.1step 3.1assume-case sign

4.2

Choose rationals $q_{1}, q_{2}$ with $∣ q_{1} - α ∣ < η$ and $∣ q_{2} - β ∣ < η$ , where $η > 0$ is a real chosen with $η (∣ x_{1} ∣ + ∣ x_{2} ∣) < ε$ and $η (∣ f (x_{1}) ∣ + ∣ f (x_{2}) ∣) < ε$ ; such rationals exist because a rational lies strictly between any two distinct reals, and such an $η$ exists because for a real $K \geq 0$ the inequality $η K < ε$ holds for all small enough $η > 0$ .

step 3.4L7

5.1

Put $x : = q_{1} x_{1} + q_{2} x_{2}$ . Then $f (x) = q_{1} f (x_{1}) + q_{2} f (x_{2})$ by additivity and rational homogeneity, so $(x, f (x)) \in Γ$ . Moreover $∣ x - a ∣ = ∣ (q_{1} - α) x_{1} + (q_{2} - β) x_{2} ∣ \leq η (∣ x_{1} ∣ + ∣ x_{2} ∣) < ε$ and likewise $∣ f (x) - b ∣ \leq η (∣ f (x_{1}) ∣ + ∣ f (x_{2}) ∣) < ε$ .

step 3.4step 4.2A1L1L7

6.1

So every open ball of $R^{2}$ meets $Γ$ , that is, $Γ$ is dense in $R^{2}$ . Reading this contrapositively: if $Γ$ is not dense in $R^{2}$ then $f (x) = c x$ for every real $x$ , which is condition 6.

step 2.2step 5.1L6

7.1

Each of the six conditions has now been shown to force $f (x) = c x$ for every real $x$ : condition 1 at step 3.3, condition 2 at step 3.2, condition 3 at step 2.1, condition 4 at step 3.1, condition 5 at step 4.1 and condition 6 at step 6.1.

step 2.1step 3.1step 4.1step 3.2step 3.3step 6.1cases-exhaustive∎

Remarks

Every clause reduces to one lemma. The engine is If an additive $f : R \to R$ is bounded above on some nondegenerate interval, then $f (x) = f (1) x$ for every real $x$ ; five of the six conditions are shown to imply its hypothesis, and the sixth is proved separately because a non-dense graph gives no bound on $f$ anywhere. The economy is deliberate: proving each clause from scratch would repeat the same translation-and-scaling argument five times.
The list is not a list of equivalent conditions. Each of the six implies linearity, and linearity implies all six, so over the additive functions they are indeed equivalent; but the theorem as stated is six implications in one direction, and that is what the proof establishes.
None of the six is dispensable in the sense that additivity alone suffices. There is an additive $f$ satisfying none of them (FALSE: every additive $f : R \to R$ is of the form $x \mapsto c x$ for a single real $c$ ), and by the theorem it is unbounded above and below on every nondegenerate interval, monotone on none, continuous at no point, of constant sign on no nondegenerate interval, and has dense graph. The construction costs the Axiom of Choice, and the companion page records what it looks like.

Depends on

Used by

Dependency tree · two levels

64 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)
Hamel basis (Wikipedia) (standard reference, not scraped)
Additive operators approximately preserving Birkhoff-James orthogonality (Aequationes mathematicae) (standard reference, not scraped)

Six regularity conditions each force an additive f:R→Rf:R→R to be x↦f(1)xx↦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 R2R2