TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

$\log$ is the unique continuous $f : (0, \infty) \to R$ with $f (x y) = f (x) + f (y)$ and $f (e) = 1$

Statement

The natural logarithm is the unique continuous function $f : (0, \infty) \to R$ satisfying

$f (x y) = f (x) + f (y) (x, y > 0), f (e) = 1.$

Facts & Assumptions

Given: A continuous $f : (0, \infty) \to R$ satisfying the displayed functional equation and normalisation.

[F1]

$E = L^{- 1}$ , so $E (L (x)) = x$ (The integral exponential $E : R \to (0, \infty)$ as the inverse of $L$ ).

[L1]

$E (a + b) = E (a) E (b)$ (The inverse $E$ satisfies $E (a + b) = E (a) E (b)$ ).

[L2]

$E$ is differentiable (The inverse $E$ is differentiable, $E^{'} = E$ , and $E (0) = 1$ ), hence continuous (A function differentiable at $c$ is continuous at $c$ ).

[L3]

A composite of continuous functions is continuous (A composite of continuous functions is continuous, with no side hypothesis of the kind the composition of limits needs).

[L4]

A continuous additive function $g : R \to R$ has the form $g (t) = c t$ (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}$ ).

[L5]

$E = \exp$ (The integral exponential $E$ is the published exponential function) and $e = \exp (1)$ (The real exponential function and the number $e$ by a power series).

[L6]

$L = \log$ on $(0, \infty)$ (The integral logarithm $L$ is the published natural logarithm).

[L7]

The natural logarithm is continuous and satisfies $\log (x y) = \log x + \log y$ (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

Proof

technique · direct

1.1

Define $g : R \to R$ by $g (t) : = f (E (t))$ . The addition law and the equation for $f$ give $g (a + b) = g (a) + g (b)$ .

L1given

1.2

The function $E$ is continuous by [L2], so $g$ is continuous by [L3] and the assumed continuity of $f$ .

L2L3given

1.3

Conversely, [L7] says that the natural logarithm is continuous and has the required equation. Moreover, [L5] gives $e = E (1)$ , so [F1] and [L6] give $\log (e) = L (E (1)) = 1$ . Thus it also has the required normalisation.

L7L5F1L6

2.1

By [L4], $g (t) = c t$ for some $c \in R$ .

step 1.1step 1.2L4

3.1

From [L5], $E (1) = e$ , so $c = g (1) = f (e) = 1$ . Hence $g (t) = t$ .

step 2.1L5given

4.1

For $x > 0$ , [F1] gives $x = E (L (x))$ , so $f (x) = g (L (x)) = L (x) = \log x$ by [L6].

F1step 3.1L6

5.1

Steps 4.1 and 1.3 prove existence and uniqueness.

step 4.1step 1.3∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 146 results over 23 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

Henry Ricardo, The Equivalence of Definitions of the Natural Logarithm Function (standard reference, not scraped)

log⁡log is the unique continuous f:(0,∞)→Rf:(0,∞)→R with f(xy)=f(x)+f(y)f(xy)=f(x)+f(y) and f(e)=1f(e)=1