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.

Changing an unstable orientation changes two sets of basis signs

Example

Assume AC. Fix a Morse--Smale pair on a closed manifold and orientations $o r_{s}$ of all unstable manifolds, giving the signed differential $\partial$ of The signed Morse differential over the integers. Flip the orientation of a single critical point $r$ (replace $o r_{r}$ by its opposite) and keep all other orientations, obtaining $\partial^{'}$ . Then:

every coefficient $n (x, r)$ of the boundary of a basis element $x$ above $r$ changes sign, and every coefficient $n (r, y)$ in $\partial r$ changes sign;
all other coefficients are unchanged;
consequently $\partial^{'} = T \partial T^{- 1}$ , where $T$ is the basis change $r \mapsto - r$ and $p \mapsto p$ for $p \neq r$ ; in particular $\partial^{' 2} = 0$ and the homology is unchanged. On the circle example $r = p$ (the maximum) the two arcs change sign simultaneously, so $\partial p = 0$ is again obtained.

Facts & Assumptions

Given: A Morse--Smale pair on a closed manifold, orientations $o r_{s}$ of all unstable manifolds, a critical point $r$ , and the Axiom of Choice as carried by the cited finiteness and differential results.

[F1]

An orientation of a critical point is a ray in the determinant line of its unstable manifold, and changing the ray to its opposite reverses the co-orientation it induces on the stable manifold (The orientation line of a Morse critical point, Unstable orientations induce orientations of the trajectory moduli spaces).

[F2]

The comparison sign $ϵ (γ)$ is determined by comparing the orientation induced on the parametrized moduli space with the positive flow orientation; reversing $o r_{r}$ reverses $ϵ$ for exactly those trajectories whose oriented moduli spaces use $o r_{r}$ , namely the spaces $M (r, y)$ with $λ (y) = λ (r) - 1$ (where $o r_{r}$ orients the source unstable manifold) and the spaces $M (x, r)$ with $λ (x) = λ (r) + 1$ (where $o r_{r}$ co-orients the target stable manifold) (Unstable orientations induce orientations of the trajectory moduli spaces).

[F3]

The signed differential is $\partial p = \sum_{q} (\sum_{γ \in M (p, q)} ϵ (γ)) q$ over the integers, with finite sums (The signed Morse differential over the integers, The integers as equivalence classes of pairs of naturals).

[F4]

The integral Morse differential squares to zero (The integral Morse differential squares to zero).

[F5]

In the circle example the maximum $p$ has two outgoing trajectories $γ_{1}, γ_{2}$ with $ϵ (γ_{1}) = - ϵ (γ_{2})$ , so their contributions cancel (The Morse complex of the circle).

Verification

technique · direct

1.1F2F3F5

The normalized positive multiple of the round circle gradient in [F5] preserves the two arcs, and its flow directions are opposite relative to one orientation of the unstable interval. Thus their comparison signs are opposite and their signed sum is zero.

1.2F1F2F3

By [F2], reversing $o r_{r}$ reverses the comparison sign of every trajectory in the two families $M (x, r)$ with $λ (x) = λ (r) + 1$ and $M (r, y)$ with $λ (y) = λ (r) - 1$ , and of no other trajectory: every other moduli space is built from orientations of unstable manifolds different from $r$ . Consequently the coefficient $n (x, r)$ of $r$ in $\partial x$ and the coefficient $n (r, y)$ of $y$ in $\partial r$ change sign, by [F3], while all other coefficients are unchanged. This proves claims (1) and (2).

2.1F3step 1.2algebra

Let $T$ be the linear automorphism of the integral chain groups sending the basis element $r$ to $- r$ and every other basis element to itself; it is invertible with $T^{- 1} = T$ . Compare $T \partial T^{- 1}$ with $\partial^{'}$ on basis elements. On $r$ : $T \partial T^{- 1} (r) = - T (\partial r) = - \partial r$ , because $\partial r$ has no $r$ -component (its terms are critical points of index one less than $λ (r)$ ) and $T$ fixes every other basis element, while $\partial r = T (\partial r)$ holds as $T$ also fixes $r$ 's own absent component; by step 1.2, $\partial^{'} r = - \partial r$ . On a basis element $x$ with $λ (x) = λ (r) + 1$ : $T \partial (x) = T (\sum_{y} n (x, y) y) = \sum_{y \neq r} n (x, y) y - n (x, r) r$ , which is $\partial^{'} x$ by step 1.2. On every other basis element $x$ : $\partial x$ has no $r$ -component, so $T \partial (x) = \partial x = \partial^{'} x$ by step 1.2 and claim (2). Hence the two linear maps agree on a basis.

3.1F4step 2.1algebra

Since $T$ is an invertible linear map, $\partial^{' 2} = T \partial T^{- 1} T \partial T^{- 1} = T \partial^{2} T^{- 1}$ , so $\partial^{' 2} = 0$ by [F4] and $T$ restricts to an isomorphism of the homologies of $\partial$ and $\partial^{'}$ . This proves claim (3).

4.1F5step 1.2step 3.1∎

For the circle instance, take $r = p$ , the maximum. The two arcs $γ_{1}, γ_{2}$ of $M (p, q)$ both use $o r_{p}$ , so by step 1.2 both comparison signs flip and their sum remains zero by [F5]; hence the integral differential still vanishes and the homology is unchanged, in agreement with the general statement.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

50 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 Ch. 3, complete author PDF (standard reference, not scraped)
Alberto Abbondandolo and Pietro Majer, Lectures on the Morse Complex for Infinite-Dimensional Manifolds, complete PDF (standard reference, not scraped)
Liviu I. Nicolaescu, An Invitation to Morse Theory, 2nd ed., complete PDF (standard reference, not scraped)