CorollaryStatement: 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.

Every continuous $f$ with $f (x y) = f (x) + f (y)$ is $f (x) = c \log x$ for a unique $c$ , including $c = 0$

Statement

If $f : (0, \infty) \to R$ is continuous and $f (x y) = f (x) + f (y)$ for all $x, y > 0$ , then there is a unique $c \in R$ such that

$f (x) = c \log x (x > 0) .$

Here $c = 0$ gives the zero function.

Facts & Assumptions

Given: A continuous $f$ satisfying the product-to-sum equation.

[F1]

$E = L^{- 1}$ (The integral exponential $E : R \to (0, \infty)$ as the inverse of $L$ ) and $E (a + b) = E (a) E (b)$ (The inverse $E$ satisfies $E (a + b) = E (a) E (b)$ ).

[L1]

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

[L2]

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

[L3]

Every continuous additive real function 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}$ ).

[L4]

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

[F2]

For $b > 0$ , $b \neq 1$ , one defines $\log_{b} x = \log x / \log b$ (The logarithm to a positive base other than one).

[L5]

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

Put $g (t) = f (E (t))$ . By [F1] and the functional equation, $g$ is additive. By [L1], [L2], and continuity of $f$ , it is continuous.

F1L1L2given

1.2

Conversely, [L5] shows that each function $x \mapsto c \log x$ is continuous and satisfies the product-to-sum equation. For $c = 0$ this is the zero function.

L5algebra

1.3

If $c \neq 0$ , put $b = E (1 / c)$ . Then $b > 0$ and $\log b = 1 / c \neq 0 = \log 1$ , so $b \neq 1$ ; [F2] gives $\log_{b} x = c \log x$ . Thus the nonzero members are exactly the constant-multiple forms underlying logarithms to bases, while the zero member requires no division.

F1L4L5F2algebra

2.1

By [L3], $g (t) = c t$ for a unique scalar $c = g (1)$ .

step 1.1L3

3.1

For $x > 0$ , $x = E (L (x))$ , so $f (x) = g (L (x)) = c L (x) = c \log x$ . By [L4], $E (1) = e$ , hence $c = g (1) = f (e)$ , which also proves uniqueness.

F1step 2.1L4

4.1

Steps 3.1, 1.2, and 1.3 prove the classification and its endpoint case.

step 3.1step 1.2step 1.3∎

Depends on

Used by

Dropping f(e)=1 leaves the whole family c log, including logarithms to other bases and the zero function Example

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 147 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)

Every continuous ff with f(xy)=f(x)+f(y)f(xy)=f(x)+f(y) is f(x)=clog⁡xf(x)=clogx for a unique cc, including c=0c=0