TheoremStatement: Literature-sourcedProof: Literature-sourcedjudge pass (gpt-5.6-terra)audited 2026-09-04

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 lemma

Statement

Let $f : M \to R$ be smooth, let $p$ be a nondegenerate critical point of $f$ , and let $λ$ be the index of $p$ . If $n = \dim M$ , then there are local coordinates $(x^{1}, \dots, x^{n})$ centered at $p$ in which

$f = f (p) - \sum_{i = 1}^{λ} (x^{i})^{2} + \sum_{i = λ + 1}^{n} (x^{i})^{2} .$

For $n = 0$ , both sums are empty.

Facts & Assumptions

Given: A smooth function $f : M \to R$ , a nondegenerate critical point $p$ , and its index $λ$ .

[F1]

Index and nondegeneracy are defined from the critical Hessian (Nondegenerate critical points, nullity, index, and coindex).

[L1]

Sylvester's law gives a linear coordinate change that puts any symmetric Hessian matrix into diagonal normal form with its positive, negative, and zero counts recorded on the diagonal (Sylvester's law of inertia: every real symmetric form is congruent to $diag (I_{p}, - I_{q}, 0_{r})$ , and $(p, q, r)$ is unique).

[L2]

The chartwise inertia counts of the Hessian equal the intrinsic index, coindex, and nullity (Sylvester inertia makes the Morse index intrinsic).

[L3]

A nonzero second derivative in one chosen coordinate splits off a signed square after a local coordinate change (A nonzero second derivative splits off a signed square with a smooth parameter).

[L4]

After splitting one signed square, the remaining Hessian is the restricted residual Hessian (Splitting one Morse coordinate preserves the residual Hessian).

Proof

technique · dimension induction

1.1

If $n = 0$ , the manifold is locally a point, so $f$ is locally constant at $p$ . The Hessian acts on the zero vector space, hence $λ = 0$ by [F1], and the displayed formula is exactly $f = f (p)$ with both sums empty.

F1givenbase

1.2

Assume the theorem proved in dimensions $< n$ , where $n > 0$ . Choose local coordinates $u = (u^{1}, \dots, u^{n})$ centered at $p$ and write $g : = f \circ u^{- 1} - f (p)$ . By [L1], after a linear change of the $u$ -coordinates the Hessian matrix of $g$ at $0$ is diagonal with entries in ${1, - 1, 0}$ . Since $p$ is nondegenerate and has index $λ$ , [F1] and [L2] force exactly $λ$ negative diagonal entries, exactly $n - λ$ positive diagonal entries, and no zero entry. Reorder the coordinates so the first diagonal entry is negative when $λ > 0$ and positive when $λ = 0$ ; in particular $\partial^{2} g / \partial (u^{1})^{2} (0) \neq 0$ . [F1, L1, L2, given, assume-case[ positive-dimension], construct]

2.1

Apply [L3] to the first coordinate $u^{1}$ , taking the remaining variables as parameters. After shrinking the chart there are new coordinates $(v^{1}, y)$ with $g (v^{1}, y) = ε (v^{1})^{2} + H (y)$ , where $ε \in {\pm 1}$ , $y \in R^{n - 1}$ , and $0$ is a critical point of $H$ .

L3step 1.2construct

3.1

By [L2], the Hessian of $g$ in the $(v^{1}, y)$ chart still has index $λ$ . By [L4], the Hessian of $H$ at $0$ is the restriction to the $y$ -coordinates, and the split $v^{1}$ -direction contributes one negative square exactly when $ε = - 1$ . Therefore ${Hess}_{0} (H)$ is nondegenerate, with index $λ - 1$ when $ε = - 1$ and index $λ$ when $ε = 1$ .

L2L4step 2.1algebra

4.1

Apply the induction hypothesis to $H$ on $R^{n - 1}$ . It yields local coordinates $(v^{2}, \dots, v^{n})$ putting $H$ into its Morse normal form, and adjoining $v^{1}$ contributes one additional negative square exactly when $ε = - 1$ . Therefore the full expression for $g$ has exactly $λ$ negative squares and $n - λ$ positive squares.

ihstep 3.1construct

5.1

Combining steps 2.1 and 4.1 proves the displayed normal form for dimension $n$ , and step 1.1 covers the base case.

step 1.1step 2.1step 4.1discharge-induction∎

Depends on

Used by

The critical level is a quadratic cone in Morse coordinates Corollary
The Morse index detects local extrema and saddles Corollary
The standard quadratic form realizes every Morse index Example

Dependency tree · two levels

16 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

Liviu I. Nicolaescu, An Invitation to Morse Theory, 2nd ed. (standard reference, not scraped)
Michele Audin and Mihai Damian, Morse Theory and Floer Homology (standard reference, not scraped)