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

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∎

Depends on

Used by

Dependency tree · two levels

10 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

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