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
Statement
Assume the Axiom of Countable Choice . Every open cover of a smooth manifold admits a smooth partition of unity subordinate to it.
Facts & Assumptions
Given: Countable Choice (The Axiom of Countable Choice ()), a smooth manifold , and an indexed open cover of .
Under Countable Choice, the cover has an at-most-countable subordinate cover by relatively compact coordinate balls (Every open cover of a manifold has a countable relatively compact coordinate-ball subcover).
Under Countable Choice, such a cover has an at-most-countable locally finite shrinking indexed by a possibly finite or empty set , with (A countable coordinate-ball cover has a countable locally finite shrinking).
For every compact set inside an open set there is a smooth manifold bump equal to on a neighbourhood of that compact set and supported in the open set (A manifold bump for a compact set inside an open set).
A locally finite nonnegative smooth family that is pointwise positive normalizes to a partition of unity (A locally finite positive smooth family normalizes to a partition of unity).
Countable Choice also selects one [L3] bump for each when is infinite; finite choice handles a finite , and no choice is needed when is empty.
Proof
Apply [L1] and then [L2] to obtain an at-most-countable index set , open sets and coordinate balls for such that , the family is locally finite, and each lies in a selected cover member . The set is allowed to be finite or empty.
For each , [L3] gives a nonempty set of smooth functions equal to near and supported in . Use [A1] to select one for each . The family is locally finite and pointwise positive because every point lies in some . When is empty, may be empty and the partition claim is vacuous.
Normalize by [L4]; the resulting nonnegative smooth family has locally finite supports, sums to one, and satisfies for every .
To index the partition by the original cover as required by Smooth partitions of unity subordinate to an open cover, put for each . Every sum is locally finite and smooth; the family is locally finite, since near any point only finitely many have support. Nonnegativity and local finiteness give , and . Thus is the required subordinate partition.
Depends on
The Axiom of Countable Choice ()
Every open cover of a manifold has a countable relatively compact coordinate-ball subcover
A countable coordinate-ball cover has a countable locally finite shrinking
A manifold bump for a compact set inside an open set
A locally finite positive smooth family normalizes to a partition of unity
Smooth partitions of unity subordinate to an open cover