ExampleConstruction: Literature-sourcedVerification: Literature-sourcedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

The height function on a sphere is perfect

Example

Assume ${A C}_{ω}$ . For $n \geq 1$ let $h : S^{n} \to R, h (x) = x_{n + 1},$ be the height function on the unit sphere (Euclidean spheres and closed balls as subspaces of $R^{n}$ ). Its only critical points are the two poles $\pm e_{n + 1}$ , nondegenerate of indices $0$ and $n$ , so $M_{h} (t) = 1 + t^{n}, # Crit (h) = 2.$ Over every field $F$ , the homology of spheres gives $b_{0} (S^{n}; F) = b_{n} (S^{n}; F) = 1$ and $b_{k} (S^{n}; F) = 0$ otherwise, hence $P_{S^{n}, F} (t) = 1 + t^{n} = M_{h} (t) :$ the height function is $F$ -perfect for every $F$ , with correction polynomial $Q = 0$ , and every weak inequality is an equality. For $n = 1$ this is the circle with one minimum and one maximum.

Facts & Assumptions

Given: An integer $n \geq 1$ , the height function $h (x) = x_{n + 1}$ on the unit sphere $S^{n}$ , and a field $F$ .

[F1]

Critical points, nondegeneracy, index, and the Hessian have the meanings of the local Morse definitions (Critical points and critical values of a smooth function, Nondegenerate critical points, nullity, index, and coindex, The intrinsic Hessian of a smooth function at a critical point).

[F2]

The Morse numbers are $m_{k} (h) = # {p \in Crit (h) : ind (p) = k}$ and $M_{h} (t) = \sum_{k} m_{k} (h) t^{k}$ (Morse numbers and the Morse polynomial).

[F3]

$P_{X, F} (t) = \sum_{k} \dim_{F} H_{k} (X; F) t^{k}$ is the Poincare polynomial over $F$ and $b_{k} (X; F) = \dim_{F} H_{k} (X; F)$ the $F$ -Betti numbers (Poincare polynomial of a space and of a pair over a field).

[L1]

For $n \geq 1$ , ${\tilde{H}}_{k} (S^{n}; G)$ is $G$ for $k = n$ and $0$ otherwise; in particular $H_{0} (S^{n}; G) ≅ G$ . (Homology of spheres).

[F4]

There is a unique $Q \in Z [t]$ with nonnegative coefficients and $M_{h} (t) = P_{S^{n}, F} (t) + (1 + t) Q (t)$ (Morse polynomial identity).

[F5]

$h$ is $F$ -perfect when $m_{k} (h) = b_{k} (S^{n}; F)$ for all $k$ , equivalently when $M_{h} = P_{S^{n}, F}$ (Perfect Morse function over a field).

Verification

technique · direct-local-model

1.1F1givenalgebra

If $x \in S^{n}$ is not a pole, put $v : = e_{n + 1} - x_{n + 1} x$ . Then $x \cdot v = x_{n + 1} - x_{n + 1} (x \cdot x) = 0$ , so $v \in T_{x} S^{n}$ , and $d h_{x} (v) = v_{n + 1} = 1 - x_{n + 1}^{2} \neq 0$ because $x_{n + 1}^{2} < 1$ off the poles. Hence only the poles can be critical points of $h$ .

2.1F1F2step 1.1

Near the north pole write the upper hemisphere as $u \mapsto (u, \sqrt{1 - ∥ u ∥^{2}})$ , so that $h (u) = \sqrt{1 - ∥ u ∥^{2}} = 1 - \frac{1}{2} ∥ u ∥^{2} + O (∥ u ∥^{4})$ ; the Hessian at $u = 0$ is $- I_{n}$ , hence the north pole is a nondegenerate critical point of index $n$ . Near the south pole write $u \mapsto (u, - \sqrt{1 - ∥ u ∥^{2}})$ , so that $h (u) = - \sqrt{1 - ∥ u ∥^{2}} = - 1 + \frac{1}{2} ∥ u ∥^{2} + O (∥ u ∥^{4})$ ; the Hessian at $u = 0$ is $I_{n}$ and the south pole has index $0$ . Therefore $Crit (h) = {\pm e_{n + 1}}$ and, by [F2], $M_{h} (t) = 1 + t^{n}, # Crit (h) = 2.$

3.1L1F3step 2.1

By [L1] read in unreduced form, $b_{0} (S^{n}; F) = b_{n} (S^{n}; F) = 1$ and $b_{k} (S^{n}; F) = 0$ for $k \notin {0, n}$ ; hence by [F3] $P_{S^{n}, F} (t) = 1 + t^{n} = M_{h} (t) .$

4.1F4F5step 2.1step 3.1∎

The correction polynomial of the Morse polynomial identity is unique [F4]; since $Q = 0$ satisfies $M_{h} = P_{S^{n}, F} + (1 + t) Q$ , the actual correction polynomial is $Q = 0$ and $m_{k} (h) = b_{k} (S^{n}; F)$ for every $k$ . By [F5] the height function is $F$ -perfect, for every field $F$ , and every weak inequality $m_{k} \geq b_{k}$ is an equality.

Remarks

Endpoint indices. The example realizes the extreme indices $0$ and $n$ and shows that the equality case of every inequality occurs simultaneously; it is the simplest perfect Morse function.
The case $n = 1$ . For the circle the two poles are a minimum and a maximum of indices $0$ and $1$ , and $M_{h} (t) = 1 + t = P_{S^{1}, F} (t)$ over every field.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

42 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, Part I Chapter 4 Section 4.4, printed pp. 88-91 (PDF pp. 98-100) (standard reference, not scraped)
Liviu Nicolaescu, An Invitation to Morse Theory (2nd ed.), Chapter 2 Section 2.3, printed pp. 46-53 (PDF pp. 56-63) (standard reference, not scraped)