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 boundary of a positive-dimensional manifold is a closed embedded smooth (n-1)-manifold
Statement
If has dimension , the restrictions of boundary charts to their faces give the structure of a closed embedded smooth boundaryless -manifold. For , .
Facts & Assumptions
Given: A smooth -manifold with boundary.
The boundary and interior defined in boundary charts are intrinsic (Smooth invariance of the manifold boundary).
Boundary-chart transition maps are smooth in the local-extension sense (Smooth charts, atlases, and structures with boundary).
A submanifold with boundary is embedded when its inclusion into the ambient manifold is a smooth embedding (Embedded smooth submanifolds with boundary).
Proof
Suppose . Restrict each boundary chart to the face . By [L1] these restrictions cover exactly . Their images are open subsets of , and [L2] makes their transition maps smooth restrictions of extensions of the ambient transitions. They therefore define a smooth boundaryless -manifold structure on .
In a boundary chart the inclusion is the coordinate map , so it is a smooth injective immersion and a homeomorphism onto its subspace image. Thus it is a smooth embedding, and [L3] gives the asserted embedded submanifold. The complement is locally , hence open, so is closed. When , the boundary is empty by the stated convention.