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.
Smooth partitions of unity exist on manifolds with boundary
Statement
Assume . Every open cover of a smooth manifold with boundary admits a smooth partition of unity subordinate to it.
Facts & Assumptions
Given: , a smooth manifold with boundary, and an open cover.
Relatively compact coordinate balls and half-balls form a basis at interior and boundary points (Relatively compact coordinate balls and half-balls form a boundary-manifold basis).
Under (The Axiom of Countable Choice ()), second countability gives a countable subcover of every open cover (Assuming countable choice, every second countable space is Lindelöf).
Under , a countable relatively compact boundary coordinate cover has an at-most-countable locally finite shrinking (A countable boundary coordinate cover has a locally finite shrinking).
A compact set inside an open Euclidean set has a smooth -valued bump equal to one near it and supported inside the open set (A Euclidean bump for a compact set inside an open set). Its proof constructs the support inside a finite union of bounded closed balls, so that support is compact.
Smoothness in half-space charts uses local smooth extension and is preserved by smooth composition (Smooth functions on relatively open half-space sets, Chain rule for smooth half-space maps).
The boundary partition contract requires smoothness in half-space charts, locally finite supports subordinate to the indexed cover, and sum one (Smooth partition of unity on a manifold with boundary).
Proof
Form the set of all pairs where indexes a member of the given cover, is a coordinate ball or half-ball with compact closure, and . By [L1] the balls in these pairs cover , without choosing one pair for every point. By [L2], their projection to balls has an at-most-countable subcover . Use to choose for each listed an index witnessing . If , the empty partition already satisfies [L6]; henceforth assume it is nonempty, repeating one selected pair if the subcover is finite.
Apply [L3] to , obtaining an at-most-countable family with , , and locally finite. Assign each to the original cover index from step 1.1.
Fix . A chart for identifies the compact set with a compact subset of a relatively open set . Choose an open with . For , [L4] gives a smooth Euclidean bump equal to one near and supported inside . Its support is compact by the finite-ball construction in [L4], so its intersection with the closed half-space is compact and lies inside . Restrict the bump to , pull it back through the chart, and extend by zero outside . Its support is a compact subset of , so this extension is smooth both at the manifold boundary and across the edge of by [L5]. It is a -valued smooth function , equal to one on and supported inside . For , use the constant-one function on the singleton chart , extended by zero outside it.
The nonempty set of valid bumps in step 3.1 is specified independently for each in an at-most-countable family. Use once to select all (finite choice if is finite). Because and is locally finite, is locally a finite smooth sum. It is positive everywhere because the cover and on . By [L5], is smooth in boundary charts: near each point a smooth local extension of stays positive after shrinking the chart, so the ordinary reciprocal composes smoothly. Set .
For each original cover index , put , taking the zero function when there are no such . The family is locally finite because the are, and every is smooth and nonnegative. The union of the locally finite closed supports assigned to is closed and lies in , so . Also , and each . By [L6], this is a smooth partition subordinate to the original cover. The empty case was handled in step 1.1.
Depends on
The Axiom of Countable Choice ()
Smooth charts, atlases, and structures with boundary
Smooth functions on relatively open half-space sets
Smooth partition of unity on a manifold with boundary
Relatively compact coordinate balls and half-balls form a boundary-manifold basis
Assuming countable choice, every second countable space is Lindelöf
A countable boundary coordinate cover has a locally finite shrinking
A Euclidean bump for a compact set inside an open set
Chain rule for smooth half-space maps