Alphabeta MathHow 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--Smale metrics are residual for a fixed Morse function
Statement
Assume the Axiom of Choice (The Axiom of Choice). Let be closed and Morse. The set of smooth Riemannian metrics for which is Morse--Smale is residual in the metric space.
Facts & Assumptions
Given: The Axiom of Choice, a closed manifold , and a fixed Morse function .
A fixed pair of critical points is transverse for a residual set of smooth metrics (Baire diagonal passage from finite regularity to smooth metrics).
A Morse function on a compact manifold has finitely many critical points.
Proof
By [F2], there are only finitely many ordered pairs of critical points. For each pair, take the residual set of metrics supplied by [F1].
Their finite intersection is residual and consists exactly of metrics for which every is transverse to every , namely the Morse--Smale metrics.
Thus the conclusion is residual in the smooth metric space. No openness or simultaneous statement about varying functions or continuation families has been used.
Depends on
- The Axiom of Choice
- Morse--Smale pairs
- Riemannian metrics, symmetric cotangent-bundle connections, and covariant Hessians
- Nowhere dense, meagre, residual, and comeagre subsets of a topological space
- Sard--Smale residual regular values for Fredholm maps
- The universal metric--trajectory projection is Fredholm
- Baire diagonal passage from finite regularity to smooth metrics
Used by
Dependency tree · two levels
26 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Alberto Abbondandolo and Pietro Majer, Lectures on the Morse Complex, §2.12 (standard reference, not scraped)