Session-authored (Fable 5 assisted)

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.

✓ 16 results · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 16 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Integral Logarithm and the Equivalence of Its Characterisations

1 · Prerequisites

2 · Summary

The oriented Riemann integral, its additivity, the first fundamental theorem of calculus, the mean value theorem, and the intermediate value theorem provide the calculus background. The declared dependency the-logarithm-and-general-powers supplies the already-published exponential, natural logarithm, their laws, the Mercator series, and the Landau root limit, but those results enter only after the independent integral construction has been completed.

The function $L (x) = \int_{1}^{x} d t / t$ is developed from its definition through its derivative, product law, unboundedness, and bijectivity. Its inverse $E$ solves the normalised differential equation and is then identified with the published exponential by one uniqueness theorem, which identifies $L$ with the natural logarithm. Continuous and differentiable functional equations, a global continuation of the Mercator series, and the Landau limit then assemble into an equivalence theorem with an explicit non-circularity roadmap.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-13Open item page →

The integral logarithm $L (x) : = \int_{1}^{x} \frac{d t}{t}$ for $x > 0$

Definition

For $x > 0$ , define the integral logarithm

$L (x) : = \int_{1}^{x} \frac{d t}{t},$

using the oriented integral when $x < 1$ (The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ ).

This is well defined. The function $t \mapsto 1 / t$ is continuous wherever $t \neq 0$ by the quotient clause of Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function. For $x \neq 1$ it is therefore continuous on the nondegenerate compact interval with endpoints $1$ and $x$ , hence Riemann integrable there by A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, whose hypothesis is $a < b$ . At $x = 1$ the interval is degenerate and that theorem does not apply; there The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ stipulates $\int_{1}^{1} f = 0$ , so $L (1) = 0$ directly.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

The integral logarithm satisfies $L^{'} (x) = 1 / x$ for $x > 0$ and $L (1) = 0$

Statement

For every $x > 0$ ,

$L^{'} (x) = \frac{1}{x},$

and $L (1) = 0$ .

Facts & Assumptions

Given: $x > 0$ and $L$ as defined.

[F1]

$L (z) = \int_{1}^{z} d t / t$ for $z > 0$ (The integral logarithm $L (x) : = \int_{1}^{x} \frac{d t}{t}$ for $x > 0$ ).

[L1]

If an integrand is Riemann integrable on a compact interval and continuous at $c$ , then its integral function with fixed lower endpoint has derivative equal to the integrand at $c$ (The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive).

[L2]

Oriented integrals satisfy $\int_{u}^{v} f + \int_{v}^{w} f = \int_{u}^{w} f$ (For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ ).

[F2]

An oriented integral reverses sign when its endpoints are reversed and is $0$ when the endpoints agree (The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ ).

Proof

technique · direct

1.1

Choose $a, b$ with $0 < a < x < b$ . For every $z \in (a, b)$ , additivity gives $L (z) = \int_{1}^{a} \frac{d t}{t} + \int_{a}^{z} \frac{d t}{t} .$

F1L2

1.2

By [F1] and the equal-endpoint convention [F2], $L (1) = \int_{1}^{1} d t / t = 0$ .

F1F2

2.1

The first term in step 1.1 is constant in $z$ . Since $1 / t$ is continuous at $x$ , [L1] gives $L^{'} (x) = 1 / x$ .

step 1.1L1algebra

3.1

Since $x > 0$ was arbitrary, steps 2.1 and 1.2 prove both claims.

step 2.1step 1.2∎

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

The integral logarithm is continuous and strictly increasing on $(0, \infty)$

Statement

The function $L : (0, \infty) \to R$ is continuous and strictly increasing.

Facts & Assumptions

Given: $L$ on $(0, \infty)$ .

[L1]

$L$ is differentiable and $L^{'} (x) = 1 / x$ for $x > 0$ (The integral logarithm satisfies $L^{'} (x) = 1 / x$ for $x > 0$ and $L (1) = 0$ ).

[L2]

Differentiability at a point implies continuity there (A function differentiable at $c$ is continuous at $c$ ).

[L3]

If a function is continuous on $[a, b]$ and differentiable on $(a, b)$ , then $f (b) - f (a) = f^{'} (c) (b - a)$ for some $c \in (a, b)$ (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

Proof

technique · direct

1.1

By [L1] and [L2], $L$ is continuous at every point of $(0, \infty)$ .

L1L2

1.2

Let $0 < a < b$ . Applying [L3] gives a $c \in (a, b)$ such that $L (b) - L (a) = L^{'} (c) (b - a) = \frac{b - a}{c} > 0.$

L1L3algebra

2.1

Hence $L (a) < L (b)$ whenever $0 < a < b$ , so $L$ is strictly increasing; step 1.1 supplies continuity.

step 1.1step 1.2∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

The integral logarithm satisfies $L (x y) = L (x) + L (y)$ for all positive $x$ and $y$

Statement

For all $x, y > 0$ ,

$L (x y) = L (x) + L (y) .$

Facts & Assumptions

Given: $y > 0$ , with $x$ ranging over $(0, \infty)$ .

[L1]

$L^{'} (z) = 1 / z$ for $z > 0$ , and $L (1) = 0$ (The integral logarithm satisfies $L^{'} (x) = 1 / x$ for $x > 0$ and $L (1) = 0$ ).

[L2]

If $f$ is differentiable at $g (x)$ and $g$ at $x$ , then $(f \circ g)^{'} (x) = f^{'} (g (x)) g^{'} (x)$ (The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ ).

[L3]

A continuous function on an order-convex interval whose derivative vanishes throughout the interior is constant (A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant).

[L4]

A differentiable function is continuous (A function differentiable at $c$ is continuous at $c$ ).

[L5]

Sums, differences and scalar multiples of functions differentiable at a point are differentiable there, with the corresponding derivatives (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

Proof

technique · direct

1.1

Define $h (x) : = L (x y) - L (x)$ on $(0, \infty)$ . By [L1] and [L2] each term is differentiable, so [L5] makes $h$ differentiable with $h^{'} (x) = \frac{y}{x y} - \frac{1}{x} = 0.$

L1L2L5algebra

2.1

By [L4], $h$ is continuous, so [L3] makes it constant on $(0, \infty)$ .

step 1.1L4L3

3.1

Evaluating at $x = 1$ gives $h (x) = h (1) = L (y) - L (1) = L (y)$ . Therefore $L (x y) - L (x) = L (y)$ , which is the claimed product law.

step 2.1L1algebra∎

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

$L (1 / x) = - L (x)$ , $L (x^{n}) = n L (x)$ , and in particular $L (2^{n}) = n L (2)$

Statement

For $x > 0$ ,

$L (1 / x) = - L (x) .$

For every integer $m$ ,

$L (x^{m}) = m L (x),$

and in particular $L (2^{m}) = m L (2)$ . Moreover, $L (2) > 0$ .

Facts & Assumptions

Given: $x > 0$ and an integer exponent $m$ .

[L1]

$L (x y) = L (x) + L (y)$ for positive $x, y$ (The integral logarithm satisfies $L (x y) = L (x) + L (y)$ for all positive $x$ and $y$ ).

[L2]

$L$ is strictly increasing on $(0, \infty)$ (The integral logarithm is continuous and strictly increasing on $(0, \infty)$ ).

[F1]

Natural powers are defined recursively by $x^{0} = 1$ and $x^{n + 1} = x^{n} x$ ; negative integer powers are reciprocal positive powers (Integer powers $a^{m}$ ).

[L3]

A property holding at $0$ and inherited from $n$ to $n + 1$ holds for every natural number (The principle of mathematical induction).

Proof

technique · direct

1.1

Setting both inputs equal to $1$ in [L1] gives $L (1) = 2 L (1)$ , hence $L (1) = 0$ . Applying [L1] to $x (1 / x) = 1$ then gives $L (1 / x) = - L (x)$ .

L1algebra

2.1

For natural $n$ , the identity $L (x^{n}) = n L (x)$ holds at $n = 0$ because $x^{0} = 1$ and $L (1) = 0$ . If it holds at $n$ , then $L (x^{n + 1}) = L (x^{n} x) = L (x^{n}) + L (x) = (n + 1) L (x) .$

step 1.1F1L1algebra

2.2

Since $2 > 1$ and $L (1) = 0$ , strict increase gives $L (2) > 0$ .

step 1.1L2algebra

3.1

Induction [L3] proves the power identity for every natural exponent.

step 2.1L3

4.1

If $m < 0$ , write $m = - n$ with $n > 0$ . Then $x^{m} = 1 / x^{n}$ , so steps 1.1 and 3.1 give $L (x^{m}) = - L (x^{n}) = - n L (x) = m L (x)$ . Thus the formula holds for every integer.

F1step 1.1step 3.1algebra

5.1

Substitute $x = 2$ in step 4.1, together with the natural and zero cases, to obtain $L (2^{m}) = m L (2)$ for every integer $m$ .

step 3.1step 4.1step 2.2∎

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

The integral logarithm is unbounded above and below

Statement

For every $M \in R$ there are $a, b > 0$ such that

$L (a) < M < L (b) .$

In particular, $L$ is unbounded both below and above.

Facts & Assumptions

Given: $M \in R$ .

[L1]

$L (2) > 0$ and, for every natural $n$ , $L (2^{n}) = n L (2)$ and $L (2^{- n}) = - n L (2)$ ( $L (1 / x) = - L (x)$ , $L (x^{n}) = n L (x)$ , and in particular $L (2^{n}) = n L (2)$ ).

[L2]

For every real $r$ , there is a natural number $n \geq 1$ with $r < n$ (Every complete ordered field is Archimedean).

Proof

technique · direct

1.1

If $M < 0$ , take $n = 1$ ; then $n L (2) > 0 > M$ . If $M \geq 0$ , apply [L2] to $M / L (2)$ and choose $n \geq 1$ with $M / L (2) < n$ , so $M < n L (2)$ .

L1L2algebra

1.2

If $M > 0$ , take $m = 1$ ; then $- m L (2) < 0 < M$ . If $M \leq 0$ , apply [L2] to $(- M) / L (2)$ and choose $m \geq 1$ with $(- M) / L (2) < m$ , so $- m L (2) < M$ .

L1L2algebra

2.1

Set $b = 2^{n}$ and $a = 2^{- m}$ . By [L1] and steps 1.1 and 1.2, $L (a) < M < L (b)$ , and both $a$ and $b$ are positive.

step 1.1step 1.2L1algebra∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

$L : (0, \infty) \to R$ is a continuous strictly increasing bijection

Statement

The function

$L : (0, \infty) \to R$

is a continuous strictly increasing bijection.

Facts & Assumptions

Given: $L$ on $(0, \infty)$ and a target $r \in R$ .

[L1]

$L$ is continuous and strictly increasing on $(0, \infty)$ (The integral logarithm is continuous and strictly increasing on $(0, \infty)$ ).

[L2]

For every real $r$ , there are positive $a, b$ with $L (a) < r < L (b)$ (The integral logarithm is unbounded above and below).

[L3]

A continuous real function on $[a, b]$ takes every value between its endpoint values (Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a, b]$ takes every value between $f (a)$ and $f (b)$ ).

Proof

technique · direct

1.1

Strict increase in [L1] makes $L$ injective.

1.2

By [L2], choose positive $a, b$ with $L (a) < r < L (b)$ . Strict increase in [L1] then implies $a < b$ .

L2L1

2.1

The restriction of $L$ to $[a, b]$ is continuous by [L1], so [L3] gives $x \in (a, b)$ with $L (x) = r$ . Thus $L$ is surjective onto $R$ .

step 1.2L1L3

3.1

Steps 1.1 and 2.1 show that $L$ is a bijection, and continuity and strict increase are already supplied by [L1].

step 1.1step 2.1L1∎

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-13Open item page →

The integral exponential $E : R \to (0, \infty)$ as the inverse of $L$

Definition

Because

$L : (0, \infty) \to R$

is a bijection ( $L : (0, \infty) \to R$ is a continuous strictly increasing bijection), it has an inverse function in the sense of Injection, surjection, bijection. Define the integral exponential

$E : R \to (0, \infty), E : = L^{- 1} .$

Thus, for $x > 0$ and $y \in R$ ,

$E (L (x)) = x, L (E (y)) = y .$

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

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

Statement

For all $a, b \in R$ ,

$E (a + b) = E (a) E (b) .$

Facts & Assumptions

Given: $a, b \in R$ .

[F1]

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

[L1]

$L (x y) = L (x) + L (y)$ for positive $x, y$ (The integral logarithm satisfies $L (x y) = L (x) + L (y)$ for all positive $x$ and $y$ ).

Proof

technique · direct

1.1

Since $E (a), E (b) > 0$ , the product law gives $L (E (a) E (b)) = L (E (a)) + L (E (b)) = a + b .$

F1L1

2.1

Also $L (E (a + b)) = a + b$ . Injectivity of $L$ therefore gives $E (a + b) = E (a) E (b)$ .

F1step 1.1∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

The inverse $E$ is differentiable, $E^{'} = E$ , and $E (0) = 1$

Statement

The inverse function $E : R \to (0, \infty)$ is differentiable and

$E^{'} (y) = E (y) (y \in R), E (0) = 1.$

Facts & Assumptions

Given: $y \in R$ .

[F1]

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

[L1]

$L^{'} (x) = 1 / x$ for $x > 0$ , and $L (1) = 0$ (The integral logarithm satisfies $L^{'} (x) = 1 / x$ for $x > 0$ and $L (1) = 0$ ).

[L2]

If a continuous injective function on a nondegenerate interval has a nonzero derivative at $c$ , then its inverse is differentiable at $f (c)$ with derivative $1 / f^{'} (c)$ (Derivative of an inverse: if $f$ is continuous and injective on a nondegenerate interval $I$ and differentiable at $c \in I$ with $f^{'} (c) \neq 0$ , then the inverse $g$ is differentiable at $f (c)$ with $g^{'} (f (c)) = 1 / f^{'} (c)$ ; and if $f^{'} (c) = 0$ then $g$ is not differentiable at $f (c)$ ).

[L3]

A differentiable function is continuous (A function differentiable at $c$ is continuous at $c$ ).

Proof

technique · direct

1.1

The function $L$ is injective because it has inverse $E$ , and it is continuous by [L1] and [L3]. At $c = E (y) > 0$ its derivative is $L^{'} (c) = 1 / c \neq 0$ .

F1L1L3

1.2

Since $L (1) = 0$ , the inverse identity gives $E (0) = 1$ .

L1F1

2.1

Apply [L2] at $c = E (y)$ . Since $L (c) = y$ , $E^{'} (y) = \frac{1}{L^{'} (E (y))} = E (y) .$

step 1.1L2L1F1algebra

3.1

The arbitrary choice of $y$ , together with steps 2.1 and 1.2, proves all claims.

step 2.1step 1.2∎

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

The integral exponential $E$ is the published exponential function

Statement

For every $x \in R$ ,

$E (x) = \exp (x) .$

Facts & Assumptions

Given: The integral exponential $E$ constructed above.

[L1]

The function $E : R \to R$ is differentiable, satisfies $E^{'} = E$ , and has $E (0) = 1$ (The inverse $E$ is differentiable, $E^{'} = E$ , and $E (0) = 1$ ).

[L2]

Every differentiable $y : R \to R$ satisfying $y^{'} = y$ and $y (0) = 1$ equals the published exponential function (The exponential is the unique solution of $y^{'} = y$ with $y (0) = 1$ ).

Proof

technique · direct

1.1

By [L1], the function $E$ is differentiable, satisfies $E^{'} = E$ , and has $E (0) = 1$ .

2.1

The uniqueness theorem [L2] therefore gives $E (x) = \exp (x)$ for every real $x$ .

step 1.1L2∎

CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

The integral logarithm $L$ is the published natural logarithm

Statement

For every $x > 0$ ,

$L (x) = \log x .$

Facts & Assumptions

Given: $x > 0$ .

[F1]

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

[L1]

$E = \exp$ on $R$ (The integral exponential $E$ is the published exponential function).

[F2]

The natural logarithm is the inverse of the bijection $\exp : R \to (0, \infty)$ (The natural logarithm as the inverse of the exponential function).

Proof

technique · direct

1.1

By [F1] and [L1], $L$ is an inverse of $\exp$ .

F1L1

2.1

Inverse functions are unique, so [F2] and step 1.1 give $L (x) = \log x$ for every $x > 0$ .

step 1.1F2∎

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

The number $e$ is the unique $x > 0$ satisfying $\int_{1}^{x} \frac{d t}{t} = 1$

Statement

The number $e$ is the unique $x > 0$ such that

$\int_{1}^{x} \frac{d t}{t} = 1.$

Facts & Assumptions

Given: The published number $e$ and the integral function $L$ .

[F1]

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

[L1]

$E = \exp$ (The integral exponential $E$ is the published exponential function).

[L2]

$L$ is strictly increasing on $(0, \infty)$ (The integral logarithm is continuous and strictly increasing on $(0, \infty)$ ).

[F2]

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

Proof

technique · direct

1.1

By [F1] and [L1], $e = E (1)$ . The inverse identity [F2] gives $L (e) = L (E (1)) = 1$ .

F1L1F2algebra

2.1

Strict increase [L2] makes $L$ injective. Hence if $x > 0$ also satisfies $L (x) = 1 = L (e)$ , then $x = e$ .

L2step 1.1

3.1

The defining integral for $L$ converts steps 1.1 and 2.1 into the stated existence and uniqueness claim.

step 1.1step 2.1∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

$\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∎

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

$\log$ is the unique $f$ with $f (x y) = f (x) + f (y)$ that is differentiable at $1$ with $f^{'} (1) = 1$

Statement

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

$f (x y) = f (x) + f (y) (x, y > 0)$

that is differentiable at $1$ with $f^{'} (1) = 1$ .

Facts & Assumptions

Given: A function $f$ satisfying the displayed equation, differentiable at $1$ , with $f^{'} (1) = 1$ .

[F1]

The derivative is the limit of the difference quotient (The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set).

[L1]

$L^{'} (x) = 1 / x$ and $L (1) = 0$ (The integral logarithm satisfies $L^{'} (x) = 1 / x$ for $x > 0$ and $L (1) = 0$ ).

[L2]

$L (x y) = L (x) + L (y)$ (The integral logarithm satisfies $L (x y) = L (x) + L (y)$ for all positive $x$ and $y$ ).

[L3]

A differentiable function is continuous (A function differentiable at $c$ is continuous at $c$ ).

[L4]

A continuous function on an interval with zero derivative is constant (A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant).

[L5]

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

[L6]

Proof

technique · direct

1.1

Setting $x = y = 1$ in the functional equation gives $f (1) = 2 f (1)$ , hence $f (1) = 0$ .

givenalgebra

1.2

Conversely, [L2] and [L5] give the product equation for $\log$ , while [L1] and [L5] give differentiability at $1$ with derivative $1$ .

L2L1L5

2.1

Fix $x > 0$ . For $h$ sufficiently close to $0$ , $x + h > 0$ , and the functional equation gives $f (x + h) - f (x) = f (1 + h / x) - f (1) .$

step 1.1givenalgebra

3.1

For $h \neq 0$ , divide step 2.1 by $h$ : $\frac{f (x + h) - f (x)}{h} = \frac{1}{x} \frac{f (1 + h / x) - f (1)}{h / x} .$ As $h \to 0$ , [F1] and $f^{'} (1) = 1$ show that $f^{'} (x) = 1 / x$ .

step 2.1F1givenalgebra

4.1

Both $f$ and $L$ are differentiable on $(0, \infty)$ , so [L6] makes $f - L$ differentiable, and step 3.1 with [L1] gives $(f - L)^{'} = 0$ . By [L3], $f - L$ is continuous, so [L4] makes it constant.

step 3.1L1L3L4L6algebra

5.1

At $1$ , step 1.1 and [L1] give $(f - L) (1) = 0$ , so step 4.1 yields $f = L = \log$ by [L5].

step 1.1step 4.1L1L5

6.1

Steps 5.1 and 1.2 prove existence and uniqueness.

step 5.1step 1.2∎

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

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∎

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

The Mercator series, its value at $1$ and the product law determine $\log$ on all positive reals, while the series alone is only local

Statement

There is exactly one function $f : (0, \infty) \to R$ such that

$f (x y) = f (x) + f (y) (x, y > 0)$

and

$f (1 + u) = \sum_{n = 1}^{\infty} (- 1)^{n + 1} \frac{u^{n}}{n} (- 1 < u \leq 1) .$

That function is the natural logarithm. The series condition itself is local; the product law is the continuation rule.

Facts & Assumptions

Given: A function $f$ satisfying the two displayed conditions.

[L1]

For $- 1 < u \leq 1$ , $\log (1 + u) = \sum_{n = 1}^{\infty} (- 1)^{n + 1} u^{n} / n$ ([The power series for log(1+x) on (-1,1], including the Abel endpoint](/item/thm-log-one-plus-x-power-series)).

[L2]

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

[L3]

For every real $r$ , there is a natural $n \geq 1$ with $r < n$ (Every complete ordered field is Archimedean).

[F1]

Natural powers satisfy $x^{0} = 1$ and $x^{n + 1} = x^{n} x$ (Integer powers $a^{m}$ ).

[L4]

The induction principle proves a property for every natural once the base and successor steps are established (The principle of mathematical induction).

Proof

technique · direct

1.1

The published natural logarithm satisfies the local series condition by [L1] and the product law by [L2], so an extension exists.

L1L2

1.2

From [F1], induction gives $2^{n} \geq n + 1$ for every natural $n$ : equality holds at $n = 0$ , and $2^{n + 1} = 2 \cdot 2^{n} \geq 2 (n + 1) \geq n + 2$ .

F1L4algebra

1.3

Repeated use of the product law, justified by induction, gives $f (2^{k}) = k f (2)$ , and the series condition at $u = 1$ determines $f (2)$ .

F1L4given

2.1

Given $x > 0$ , use [L3] to choose $k \geq 1$ with $x < k$ . Then $2^{k} \geq k + 1 > k > x$ by step 1.2. Put $y = x / 2^{k}$ and $u = y - 1$ ; thus $0 < y < 1$ and $- 1 < u < 0$ .

L3step 1.2algebra

3.1

Since $x = 2^{k} y = 2^{k} (1 + u)$ , the product law and the local series condition force $f (x) = k f (2) + f (1 + u) = k \sum_{n = 1}^{\infty} \frac{(- 1)^{n + 1}}{n} + \sum_{n = 1}^{\infty} (- 1)^{n + 1} \frac{u^{n}}{n} .$

step 2.1step 1.3given

4.1

Formula 3.1 forces the value of any extension at every $x > 0$ , so at most one extension exists. Together with step 1.1, that unique extension is $\log$ .

step 3.1step 1.1∎

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Five characterisations of the natural logarithm are equivalent: inverse exponential, integral, continued Mercator series, Landau root limit and the normalised functional equation

Statement

The following five descriptions define the same function on $(0, \infty)$ :

the inverse of the published exponential function;
$x \mapsto \int_{1}^{x} d t / t$ ;
the unique product-to-sum function whose values on $1 + u$ for $- 1 < u \leq 1$ are the Mercator series;
$x \mapsto \lim_{n \to \infty} 2^{n} (x^{1 / 2^{n}} - 1)$ ;
the unique continuous product-to-sum function satisfying $f (e) = 1$ .

Each is the natural logarithm.

Facts & Assumptions

Given: The five descriptions listed in the statement.

[F1]

The natural logarithm is defined as the inverse of the exponential function (The natural logarithm as the inverse of the exponential function).

[L1]

The natural logarithm satisfies $\log x = \int_{1}^{x} d t / t$ and $\log^{'} (x) = 1 / x$ (The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t).

[L2]

The independently constructed integral function satisfies $L = \log$ (The integral logarithm $L$ is the published natural logarithm).

[L3]

The Mercator formula holds for $- 1 < u \leq 1$ ([The power series for log(1+x) on (-1,1], including the Abel endpoint](/item/thm-log-one-plus-x-power-series)), and exactly one product-law extension of those values exists, namely $\log$ (The Mercator series, its value at $1$ and the product law determine $\log$ on all positive reals, while the series alone is only local).

[L4]

For $x > 0$ , $\log x = \lim_{n \to \infty} 2^{n} (x^{1 / 2^{n}} - 1)$ (Landau's root limit: log x is the limit of 2^n times (x^(1/2^n) minus 1)).

[L5]

The natural logarithm is the unique continuous product-to-sum function with $f (e) = 1$ ( $\log$ is the unique continuous $f : (0, \infty) \to R$ with $f (x y) = f (x) + f (y)$ and $f (e) = 1$ ).

Proof

technique · direct

1.1

Description 1 is the natural logarithm by [F1].

1.2

Description 2 is the natural logarithm by the exact integral identity [L1], equivalently by the independently proved identification [L2].

L1L2

1.3

Description 3 first uses [L3]'s local series formula and then its product-law continuation theorem, which gives exactly the natural logarithm on the full positive domain.

1.4

Description 4 equals the natural logarithm pointwise by [L4].

1.5

Description 5 exists and is uniquely the natural logarithm by [L5].

2.1

Since each description gives the same function $\log$ , all five characterisations are equivalent. The third description includes its continuation rule; it does not assert convergence of the original series with $u = x - 1$ for every positive $x$ .

step 1.1step 1.2step 1.3step 1.4step 1.5∎

RemarkRemark: AI-adaptedProof: Not applicableaudited 2026-08-13Open item page →

Roadmap and non-circularity of the logarithm characterisations

Remark

The implication order is one-way until the bridge. The integral function $L$ is defined and proved differentiable, multiplicative-to-additive, unbounded, and bijective without using the published exponential or natural logarithm. Its inverse $E$ is then proved to satisfy $E^{'} = E$ and $E (0) = 1$ . Only at that point does IVP uniqueness identify $E$ with the published exponential; taking inverses identifies $L$ with the published natural logarithm.

After the bridge, Five characterisations of the natural logarithm are equivalent: inverse exponential, integral, continued Mercator series, Landau root limit and the normalised functional equation compares already proved descriptions: inverse exponential, the integral, the continued Mercator series, the Landau limit, and the regular functional equation. This does not use one description to establish a premise needed earlier in the chain. It is the inverse-function counterpart of the separate exponential roadmap in The power-series, product-limit, IVP, functional-equation, and Picard definitions agree.

The Integral Logarithm and the Equivalence of Its Characterisations

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

The integral logarithm L(x):=∫1xdttL(x):=∫1x​tdt​ for x>0x>0

Definition

The integral logarithm satisfies L′(x)=1/xL′(x)=1/x for x>0x>0 and L(1)=0L(1)=0

Statement

Facts & Assumptions

Proof

The integral logarithm is continuous and strictly increasing on (0,∞)(0,∞)

Statement

Facts & Assumptions

Proof

The integral logarithm satisfies L(xy)=L(x)+L(y)L(xy)=L(x)+L(y) for all positive xx and yy

Statement

Facts & Assumptions

Proof

L(1/x)=−L(x)L(1/x)=−L(x), L(xn)=nL(x)L(xn)=nL(x), and in particular L(2n)=nL(2)L(2n)=nL(2)

Statement

Facts & Assumptions

Proof

The integral logarithm is unbounded above and below

Statement

Facts & Assumptions

Proof

L:(0,∞)→RL:(0,∞)→R is a continuous strictly increasing bijection

Statement

Facts & Assumptions

Proof

The integral exponential E:R→(0,∞)E:R→(0,∞) as the inverse of LL

Definition

The inverse EE satisfies E(a+b)=E(a)E(b)E(a+b)=E(a)E(b)

Statement

Facts & Assumptions

Proof

The inverse EE is differentiable, E′=EE′=E, and E(0)=1E(0)=1

Statement

Facts & Assumptions

Proof

The integral exponential EE is the published exponential function

Statement

Facts & Assumptions

Proof

The integral logarithm LL is the published natural logarithm

Statement

Facts & Assumptions

Proof

The number ee is the unique x>0x>0 satisfying ∫1xdtt=1∫1x​tdt​=1

Statement

Facts & Assumptions

Proof

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

Statement

Facts & Assumptions

Proof

log⁡log is the unique ff with f(xy)=f(x)+f(y)f(xy)=f(x)+f(y) that is differentiable at 11 with f′(1)=1f′(1)=1

Statement

Facts & Assumptions

Proof

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

Statement

Facts & Assumptions

Proof

The Mercator series, its value at 11 and the product law determine log⁡log on all positive reals, while the series alone is only local

Statement

Facts & Assumptions

Proof

Five characterisations of the natural logarithm are equivalent: inverse exponential, integral, continued Mercator series, Landau root limit and the normalised functional equation

Statement

Facts & Assumptions

Proof

Roadmap and non-circularity of the logarithm characterisations

Remark

5 · Examples, counterexamples and false statements

Sources

Standard references

The integral logarithm $L (x) : = \int_{1}^{x} \frac{d t}{t}$ for $x > 0$

The integral logarithm satisfies $L^{'} (x) = 1 / x$ for $x > 0$ and $L (1) = 0$

The integral logarithm is continuous and strictly increasing on $(0, \infty)$

The integral logarithm satisfies $L (x y) = L (x) + L (y)$ for all positive $x$ and $y$

$L (1 / x) = - L (x)$ , $L (x^{n}) = n L (x)$ , and in particular $L (2^{n}) = n L (2)$

$L : (0, \infty) \to R$ is a continuous strictly increasing bijection

The integral exponential $E : R \to (0, \infty)$ as the inverse of $L$

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

The inverse $E$ is differentiable, $E^{'} = E$ , and $E (0) = 1$

The integral exponential $E$ is the published exponential function

The integral logarithm $L$ is the published natural logarithm

The number $e$ is the unique $x > 0$ satisfying $\int_{1}^{x} \frac{d t}{t} = 1$

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

$\log$ is the unique $f$ with $f (x y) = f (x) + f (y)$ that is differentiable at $1$ with $f^{'} (1) = 1$

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

The Mercator series, its value at $1$ and the product law determine $\log$ on all positive reals, while the series alone is only local