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.

A closed cylinder as a finitely patched oriented surface

Example

For $R, H > 0$ , the boundary of the cylinder $x^{2} + y^{2} \leq R^{2}$ , $0 \leq z \leq H$ , has a compatible outward-oriented presentation by its side and two caps. Its area is $2 π R H + 2 π R^{2}$ . For $F (x, y, z) = (x, y, 0)$ , its outward flux is $2 π R^{2} H$ .

Facts & Assumptions

Given: The lateral parametrization $σ (θ, z) = (R \cos θ, R \sin θ, z)$ and the two polar cap parametrizations, with outward orientations.

[L1]

Cross products are computed by the coordinate formula, and the standard trigonometric derivative and Pythagorean identities hold (The cross product in $R^{3}$ , The derivatives of sine and cosine are cosine and minus sine, Parity and the Pythagorean identity for sine and cosine, Quarter-turn values and shifts by pi/2 and pi).

[L2]

A compatible finite presentation sums patch integrals, and content-zero boundary overlaps do not change them (Finitely patched regular surfaces, their area, scalar integrals, and flux, Content-zero parameter-boundary exceptions do not affect surface integrals); Jordan-Fubini and the fundamental theorem evaluate the rectangle and disc parameter integrals (Fubini over a bounded Jordan set when all but a content-zero family of sections are integrable, 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)$ ).

[L3]

The area of a regular patch is $\int_{D} J_{φ}$ with $J_{φ} = ∥ φ_{u} \times φ_{v} ∥_{2}$ , and the flux of a continuous field $F$ in the orientation induced by $φ$ is $\int_{D} (F \circ φ) \cdot (φ_{u} \times φ_{v})$ (Surface area and scalar surface integrals on a regular patch, The surface area density is the norm of the cross product of the parameter tangents, Unit normal fields, orientations, and flux through a regular surface patch).

Verification

technique · direct

1.1

Using [L1], $σ_{θ} \times σ_{z} = (R \cos θ, R \sin θ, 0)$ is the outward side area vector, whose norm is the density $R$ of [L3]. The cap area vectors are vertical with density $ρ$ in polar parameters, directed down at $z = 0$ and up at $z = H$ .

givenL1L3algebra

1.2

The patch intersections are boundary circles, whose preimages lie in parameter boundaries and have content zero. Thus [L2] makes these patches a compatible presentation.

givenL2

2.1

By [L3] the patch areas are the integrals of those densities, giving side area $2 π R H$ and cap area $π R^{2}$ each; [L2] sums them to the total area $2 π R H + 2 π R^{2}$ .

step 1.1step 1.2L2L3algebra

2.2

By [L3] each patch flux is the integral of $F$ dotted with that patch's area vector. The field $F$ has zero dot product with both vertical cap area vectors, while on the side its dot product with the outward area vector is $R^{2}$ ; integration and [L2] give total flux $2 π R^{2} H$ .

step 1.1step 1.2L2L3algebra

3.1

Summing the compatible patch values proves both formulas.

step 2.1step 2.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

47 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

University of Toronto MAT237 notes, Section 5.3, Example 2 (standard reference, not scraped)