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.

The lateral area of a right circular cone is $π R \sqrt{R^{2} + H^{2}}$

Example

For $R, H > 0$ , the lateral surface area of a right circular cone with base radius $R$ and height $H$ is $π R \sqrt{R^{2} + H^{2}} .$

Facts & Assumptions

Given: The radius profile $r (s) = R s / H$ on $0 \leq s \leq H$ .

[L1]

The surface-of-revolution area is $2 π \int_{0}^{H} r (s) \sqrt{1 + r^{'} (s)^{2}} d s$ when the radius is positive in the open interval and may vanish at an endpoint (The surface of revolution has area $2 π \int_{a}^{b} r (s) \sqrt{1 + r^{'} (s)^{2}} d s$ ).

[L2]

Derivative algebra gives $r^{'} (s) = R / H$ , and the fundamental theorem evaluates the remaining linear integral (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$ , The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ ).

Verification

technique · direct

1.1

The profile is positive for $0 < s \leq H$ and vanishes only at the apex endpoint $s = 0$ , so [L1] applies.

givenalgebra

2.1

By [L1] and [L2], the area is $2 π (R / H) \sqrt{1 + R^{2} / H^{2}} \int_{0}^{H} s d s = π R H \sqrt{1 + R^{2} / H^{2}}$ .

step 1.1L1L2algebra

3.1

Since $H > 0$ , this equals $π R \sqrt{R^{2} + H^{2}}$ . The apex is a parameter-boundary point and contributes no separate term.

step 2.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

26 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

S. Cañez, Northwestern Math 320-3 lecture notes, cone example (standard reference, not scraped)
University of Toronto MAT237 notes, Section 5.3 (standard reference, not scraped)

The lateral area of a right circular cone is πRR2+H2πRR2+H2​