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.
Morse-Sard for smooth manifolds
Statement
Assume the Axiom of Countable Choice. Let be a smooth map between smooth manifolds. Then the critical value set of is a null subset of .
Facts & Assumptions
Given: Countable Choice and a smooth map .
The empty fibre case is regular, so if every differential is surjective then every value of is regular (Regular and critical points and values).
The empty subset of any manifold is null (Null subsets of a smooth manifold).
The critical value set is the image of the critical locus (The critical locus and critical value set).
A countable chart cover detects manifold nullity, and countable unions of manifold null sets are null (A countable chart cover detects manifold null sets, Countable unions and subsets of manifold null sets are null).
In Euclidean charts, the critical value set of a smooth map is null (Morse-Sard for Euclidean maps).
Under Countable Choice, smooth manifolds admit countable smooth atlases with relatively compact domains (Assuming Countable Choice, every smooth manifold admits a countable smooth atlas with relatively compact domains).
Proof
If , then every differential is surjective, so [F1] makes every value of regular. Thus the critical value set is empty, which is null by [F2]. Assume henceforth that .
By [L3] under Countable Choice, take countable smooth atlases on and on ; the latter detects nullity by [L1]. The countable open overlaps cover .
For each pair , the coordinate representative on is smooth between Euclidean open sets with positive-dimensional target. A point of is critical for exactly when its coordinate representative is critical for , because the chart maps have invertible differentials. By [L2], is null.
Fix . The chart image of the critical value set inside is the countable union over of the null sets from step 2.1. By the countable-union clause of [L1] in Euclidean coordinates, this chart image is null. Since this holds for every , [L1] detects the critical value set of as null in .
Depends on
Morse-Sard for Euclidean maps
Countable unions and subsets of manifold null sets are null
A countable chart cover detects manifold null sets
Assuming Countable Choice, every smooth manifold admits a countable smooth atlas with relatively compact domains
The Axiom of Countable Choice ()
The critical locus and critical value set
Regular and critical points and values
Null subsets of a smooth manifold