ExampleConstruction: Literature-sourcedVerification: 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 2$ from four characterisations: hyperbolic area, the alternating harmonic series, Landau iterates and $\exp^{- 1} (2)$

Example

The number $\log 2$ has the four equal descriptions

$\int_{1}^{2} \frac{d t}{t} = \sum_{n = 1}^{\infty} \frac{(- 1)^{n + 1}}{n} = \lim_{n \to \infty} 2^{n} (2^{1 / 2^{n}} - 1) = \exp^{- 1} (2) .$

Facts & Assumptions

Given: The positive input $2$ .

[L1]

The inverse-exponential, integral, continued Mercator, Landau-limit, and normalised functional-equation characterisations all define $\log$ (Five characterisations of the natural logarithm are equivalent: inverse exponential, integral, continued Mercator series, Landau root limit and the normalised functional equation).

[L2]

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

[L3]

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)).

[F1]

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

Verification

technique · direct

1.1

Apply the integral characterisation in [L1] at $x = 2$ to obtain $\log 2 = \int_{1}^{2} d t / t$ .

1.2

Apply [L2] to obtain the alternating harmonic series value.

1.3

Apply [L3] at $x = 2$ to obtain the Landau limit.

1.4

By [F1], $\log 2$ is the unique real $y$ with $\exp (y) = 2$ , namely $\exp^{- 1} (2)$ .

2.1

Steps 1.1 through 1.4 identify all four displayed quantities with the same value, as asserted by the equivalence theorem [L1].

step 1.1step 1.2step 1.3step 1.4L1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

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

OpenStax, Calculus Volume 1, Section 6.7 (standard reference, not scraped)

log⁡2log2 from four characterisations: hyperbolic area, the alternating harmonic series, Landau iterates and exp⁡−1(2)exp−1(2)