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

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∎

Depends on

Used by

Dependency tree · next 3 levels

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