Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adapted
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 F:M→N be a smooth map between smooth manifolds. Then the critical value set of F is a null subset of N.

Facts & Assumptions

Given: Countable Choice and a smooth map F:M→N.

[F1]

The empty fibre case is regular, so if every differential dFp is surjective then every value of F is regular (Regular and critical points and values).

[F2]

The empty subset of any manifold is null (Null subsets of a smooth manifold).

[F3]

The critical value set is the image of the critical locus (The critical locus and critical value set).

[L1]

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).

[L2]

In Euclidean charts, the critical value set of a smooth map is null (Morse-Sard for Euclidean maps).

[L3]

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

technique · direct
1.1F1F2givencases

If dim⁡N=0, then every differential dFp:TpM→TF(p)N={0} is surjective, so [F1] makes every value of F regular. Thus the critical value set is empty, which is null by [F2]. Assume henceforth that dim⁡N>0.

1.2L1L3given

By [L3] under Countable Choice, take countable smooth atlases {(Ui,φi)} on M and {(Vj,ψj)} on N; the latter detects nullity by [L1]. The countable open overlaps Uij=Ui∩F−1(Vj) cover M.

2.1L2step 1.2algebra

For each pair (i,j), the coordinate representative fij:=ψj∘F∘φi−1 on φi(Uij) is smooth between Euclidean open sets with positive-dimensional target. A point of Uij is critical for F exactly when its coordinate representative is critical for fij, because the chart maps have invertible differentials. By [L2], ψj(F(Crit⁡(F)∩Uij)) is null.

3.1F3L1step 1.2step 2.1∎

Fix j. The chart image of the critical value set inside Vj is the countable union over i 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 j, [L1] detects the critical value set of F as null in N.

Depends on

Dependency tree · 2 levels

Sources