LemmaStatement: 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.

Splitting one Morse coordinate preserves the residual Hessian

Statement

Let $F$ be smooth near $(0, 0) \in R \times R^{m}$ , assume $d F_{(0, 0)} = 0$ , and suppose there is a smooth local coordinate system $(s, y)$ centered at $(0, 0)$ , obtained from $(u, y)$ by a change of variables of the form $(u, y) \mapsto (s, y)$ , together with a smooth function $H$ near $0 \in R^{m}$ such that, in these coordinates,

$\tilde{F} (s, y) : = F (u (s, y), y) = F (0, 0) + ε s^{2} + H (y), ε \in {\pm 1} .$

Then $0$ is a critical point of $H$ , the Hessian of $H$ at $0$ is the restriction of the Hessian of $F$ at $(0, 0)$ to the $y$ -coordinate subspace in the $(s, y)$ chart, and if ${Hess}_{(0, 0)} (F)$ is nondegenerate then so is ${Hess}_{0} (H)$ .

Facts & Assumptions

Given: The smooth function $F$ , the local coordinates $(s, y)$ , and the decomposition $\tilde{F} (s, y) = F (0, 0) + ε s^{2} + H (y)$ from the statement.

[F1]

The Hessian at a critical point is represented by the matrix of second partial derivatives in any chart (The intrinsic Hessian of a smooth function at a critical point).

Proof

technique · direct local comparison

1.1

Because the coordinate change fixes $(0, 0)$ , the coordinate representative $\tilde{F}$ also satisfies $d {\tilde{F}}_{(0, 0)} = 0$ . Setting $s = 0$ in the displayed decomposition gives $\tilde{F} (0, y) = F (0, 0) + H (y)$ . Differentiating at $y = 0$ therefore shows $d H_{0} = 0$ , so $0$ is a critical point of $H$ .

givenalgebra

2.1

In the coordinates $(s, y)$ , the function $\tilde{F}$ has no mixed $s y$ term and no term linear in $s$ , so its Hessian matrix at $(0, 0)$ has block form $(\begin{array}{cc} 2 ε & 0 \\ 0 & {Hess}_{0} (H) \end{array})$ . By [F1], this is the Hessian of $F$ at $(0, 0)$ in the $(s, y)$ chart, and the lower-right block is exactly its restriction to the $y$ -coordinate subspace.

F1step 1.1algebra

3.1

If ${Hess}_{0} (H)$ had a nonzero kernel vector $v$ , then $(0, v)$ would lie in the kernel of the block matrix from step 2.1. Hence a nondegenerate Hessian for $F$ forces ${Hess}_{0} (H)$ to be nondegenerate.

step 2.1algebra

4.1

Thus splitting one signed square preserves the residual critical Hessian.

step 1.1step 2.1step 3.1∎

Depends on

Used by

Morse lemma Theorem

Dependency tree · two levels

5 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

Michele Audin and Mihai Damian, Morse Theory and Floer Homology (standard reference, not scraped)