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.
Collar neighborhood theorem
Statement
Assume . Every smooth manifold with boundary has a smooth collar.
Facts & Assumptions
Given: (The Axiom of Countable Choice ()) and a smooth manifold with boundary. Its boundary is a smooth manifold (The boundary of a positive-dimensional manifold is a closed embedded smooth (n-1)-manifold).
Under Countable Choice, there is a smooth field on an open neighbourhood of that points strictly inward at every boundary point (A global inward-pointing boundary vector field exists).
At every boundary point this field has a smooth local forward flow, remaining in for sufficiently small positive times (Inward-pointing fields have local forward semiflows at the boundary). Local flow solutions are unique and depend smoothly on their initial point and time (The fundamental theorem on flows).
Under Countable Choice, a countable open cover of admits a smooth locally finite partition of unity subordinate to it (Smooth partitions of unity exist on manifolds with boundary).
Proof
If , the empty map from is a collar. Otherwise take on from [F1]. Write wherever the local forward solution remains in . In a boundary chart, extend smoothly across the face to apply the ordinary local-flow theorem. At , the differential of has the face directions and the strictly inward vector as its columns, so it is invertible. The Euclidean inverse function theorem gives a local diffeomorphism of ambient chart neighbourhoods. Since the boundary coordinate of vanishes for and has positive -derivative near , it has the sign of there. Thus the restriction to is a smooth local collar with image relatively open in . [F1, F2, The Euclidean inverse function theorem]
No positive-time trajectory in starting on can meet again. If for , choose a boundary defining coordinate near . Strict inwardness gives on a smaller neighbourhood. For all sufficiently small , the trajectory on lies there, so the one-variable mean-value theorem gives , a contradiction.
The flow map is injective wherever these forward trajectories are defined in . If with , uniqueness applied backwards along the common terminal segment of length gives . If , this contradicts step 1.2. If , uniqueness back to time zero gives . This argument uses only uniqueness along already existing trajectories; it does not claim a negative-time flow inside .
For , let be the union of all relatively open boundary sets on which the smooth forward flow exists, stays in , and is smooth for times in . Smooth dependence and local existence in [F2] make open; as grows, the cover . Apply [F3] to this countable cover, obtaining a smooth locally finite partition with . Set . It is positive and smooth. At each only finitely many terms are nonzero. If is the least active index, then and , so exists in for every . No selection from an uncountable family of local widths is used.
Put . The map is smooth and injective by steps 2.1–2.2. It is a local diffeomorphism at by step 1.1. At , follow a sufficiently short initial part of the trajectory from a local collar chart in step 1.1, then use the ordinary local flow near the remaining interior trajectory to transport that chart; uniqueness makes the composition equal to near . Hence is a local diffeomorphism there too. Its image is relatively open in and contains ; the local inverses agree by injectivity, so is a smooth embedding onto this open neighbourhood.
The map is a smooth diffeomorphism from onto , with inverse . Composing it with gives a smooth embedding with open image and . By Smooth collars of a manifold boundary, this is a smooth collar.
Depends on
The Axiom of Countable Choice ()
The boundary of a positive-dimensional manifold is a closed embedded smooth (n-1)-manifold
A global inward-pointing boundary vector field exists
Inward-pointing fields have local forward semiflows at the boundary
The fundamental theorem on flows
Smooth collars of a manifold boundary
Smooth partitions of unity exist on manifolds with boundary
The Euclidean inverse function theorem