ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-24

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.

Gabriel's horn has unbounded truncated lateral area

Example

Rotate $r (x) = 1 / x$ about the $x$ -axis for $x \geq 1$ . If $A (T)$ is the lateral area of the compact truncation $1 \leq x \leq T$ , then $A (T)$ is unbounded as $T \to \infty$ .

Facts & Assumptions

Given: A real $T > 1$ and the radius $r (x) = 1 / x$ on $[1, T]$ .

[L1]

The surface-of-revolution formula gives $A (T) = 2 π \int_{1}^{T} r (x) \sqrt{1 + r^{'} (x)^{2}} d x$ , and derivative algebra gives $r^{'} (x) = - x^{- 2}$ (The surface of revolution has area $2 π \int_{a}^{b} r (s) \sqrt{1 + r^{'} (s)^{2}} d s$ , 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$ ).

[L2]

Integral monotonicity preserves pointwise inequalities, $L (T) = \int_{1}^{T} d x / x$ is the integral logarithm, and $L$ is unbounded above (If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ , The integral logarithm $L (x) : = \int_{1}^{x} \frac{d t}{t}$ for $x > 0$ , The integral logarithm is unbounded above and below).

Verification

technique · direct

1.1

By [L1], $A (T) = 2 π \int_{1}^{T} x^{- 1} \sqrt{1 + x^{- 4}} d x$ .

givenL1algebra

2.1

Since $\sqrt{1 + x^{- 4}} \geq 1$ for $x \geq 1$ , [L2] gives $A (T) \geq 2 π \int_{1}^{T} d x / x = 2 π L (T)$ .

step 1.1L2algebra

3.1

The lower bound is unbounded by [L2], so the family of compact-truncation areas is unbounded. The noncompact horn itself was not treated as one compact patch.

step 2.1L2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

30 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

APEX Calculus II, Section 7.4, Example 216 (standard reference, not scraped)