ExampleConstruction: Literature-sourcedVerification: AI-generatedPipeline-generatedprecheck passaudited 2026-09-07

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 closed ball and its sphere boundary

Example

For $n \geq 1$ , the closed ball $B^{n}$ is a manifold with boundary $S^{n - 1}$ , and $ρ (x) = 1 - ∣ x ∣^{2}$ is a boundary-defining function.

Facts & Assumptions

Given: An integer $n \geq 1$ , the closed unit ball $B^{n} = {x \in R^{n} : ∣ x ∣ \leq 1}$ , its sphere $S^{n - 1} = {x : ∣ x ∣ = 1}$ , and $ρ : B^{n} \to [0, \infty)$ defined by $ρ (x) = 1 - ∣ x ∣^{2}$ .

[L1]

A smooth Euclidean map with invertible derivative is a diffeomorphism between suitable open neighbourhoods (The Euclidean inverse function theorem).

[L2]

A compatible covering atlas by relatively open half-space charts defines a smooth manifold with boundary (Smooth charts, atlases, and structures with boundary).

[L3]

A boundary-defining function is smooth and nonnegative, has the boundary as its zero set, and has nonzero differential there (Boundary-defining functions).

Verification

technique · direct

1.1

Let $p \in S^{n - 1}$ and choose $k$ with $p_{k} \neq 0$ . The map $H (x) = (x_{1}, \dots, \hat{x_{k}}, \dots, x_{n}, ρ (x))$ has invertible derivative at $p$ , since $\partial ρ / \partial x_{k} (p) = - 2 p_{k} \neq 0$ . By [L1], $H$ is a diffeomorphism near $p$ . Because $B^{n} = {ρ \geq 0}$ , its restriction is a half-space chart near $p$ ; ordinary Euclidean charts cover ${∣ x ∣ < 1}$ . Every transition between these charts is the restriction of a composition of the corresponding Euclidean diffeomorphisms and their inverses, so the covering atlas is compatible. Thus [L2] makes $B^{n}$ a smooth manifold with boundary, and the chart calculation identifies its boundary with $S^{n - 1}$ .

givenL1L2algebra

2.1

By construction, $ρ \geq 0$ on $B^{n}$ , $ρ^{- 1} (0) = S^{n - 1} = \partial B^{n}$ , and $d ρ_{x} (v) = - 2 ⟨ x, v ⟩$ is nonzero when $∣ x ∣ = 1$ . Hence $ρ$ satisfies [L3].

givenL3step 1.1algebra∎

Depends on

Used by

Boundary orientation of the unit sphere by the outward normal Example
The double of a disk is a sphere Example
The standard collar of a closed ball Example

Dependency tree · two levels

20 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

Ioan Mărcuț, Manifolds (2017 lecture notes), §§14.5, 15.1 (standard reference, not scraped)
Will Merry, Differential Geometry (2021), Lecture 24 (standard reference, not scraped)