ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-01

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 standard circle and its annular tubular neighbourhood

Example

For the unit circle

S^{1} = {p \in R^{2} : ∥ p ∥ = 1},

the normal line at $p$ is the radial line $R p$ . Thus the normal bundle is identified with

S^{1} \times R, (p, t) \leftrightarrow (p, t p),

and the normal addition map is

E (p, t) = (1 + t) p .

For $∣ t ∣ < 1 / 2$ , the image is the annulus

{x \in R^{2} : 1 / 2 < ∥ x ∥ < 3 / 2},

and the tubular retraction is radial normalization

r (x) = \frac{x}{∥ x ∥} .

Facts & Assumptions

Given: The unit circle $S^{1} \subseteq R^{2}$ with its Euclidean normal bundle.

Verification

technique · direct

1.1

Every vector orthogonal to $T_{p} S^{1}$ is a scalar multiple of $p$ , so the displayed identification of the normal bundle is correct. Under that identification the normal addition map is $E (p, t) = p + t p = (1 + t) p$ .

givenalgebra

2.1

If $∣ t ∣ < 1 / 2$ , then $1 / 2 < 1 + t < 3 / 2$ , so $E$ lands in the stated annulus. Conversely, every nonzero $x$ in that annulus can be written uniquely as $x = ∥ x ∥ \frac{x}{∥ x ∥} = E ⁣ (\frac{x}{∥ x ∥}, ∥ x ∥ - 1) .$ Hence this is exactly the tubular neighbourhood promised by The Euclidean tubular neighbourhood theorem.

step 1.1

3.1

The inverse formula in step 2.1 sends $x$ to $(x / ∥ x ∥, ∥ x ∥ - 1)$ , so the associated retraction is $r (x) = x / ∥ x ∥$ , in agreement with A closed Euclidean submanifold has a smooth neighborhood retraction.

step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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

John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Tubular Neighborhoods (standard reference, not scraped)