Alphabeta Math
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 Morse complex of the two-sphere

Example

Assume AC. Let f:S2→R be the height function of the round two-sphere and let X be the normalized positive multiple of its round downward gradient constructed below; this preserves its meridian orbits. Then (f,X) is Morse--Smale with exactly two critical points: a maximum N of index 2 and a minimum S of index 0 (Morse functions and excellent Morse functions, Nondegenerate critical points, nullity, index, and coindex). Consequently CM1(f,X;Z/2)=0 and CM1(f,X;Z)=0, and every differential vanishes for degree reasons: ∂2 has target CM1=0 and ∂1 has source CM1=0 (The mod-two Morse differential, The signed Morse differential over the integers). The only nonempty trajectory moduli space between distinct critical points is M(N,S); by No Morse--Smale trajectories for nonpositive index drop no moduli space with nonpositive index drop is nonempty, so no index-one differential can receive a contribution. Both complexes have homology Z/2 in degrees 0 and 2 (respectively Z in degrees 0 and 2).

Facts & Assumptions

Given: AC and the round sphere with f=z, using the normalized field of step 1.1; choose either orientation of each unstable manifold for the integral complex.

[F1]

The height function on the round two-sphere is Morse with exactly two nondegenerate critical points, the poles N of index 2 and S of index 0, and it is Morse--Smale for the round metric (Morse functions and excellent Morse functions, Nondegenerate critical points, nullity, index, and coindex, Morse--Smale pairs).

[F2]

The chain groups are free modules on the critical points of each index, so they vanish when there are no critical points of that index, and the differentials have the degrees −1 of The mod-two Morse differential and The signed Morse differential over the integers (The mod-two Morse chain group).

[F3]

Smooth cutoffs exist and the normalized local field is required by the downward gradient-like convention (A smooth bump between concentric Euclidean balls, Downward gradient-like vector fields for a Morse function). The differential suppliers carry AC (The Axiom of Choice). Under AC, a smooth vector field on a compact manifold is complete (Every smooth vector field on a compact manifold is complete).

Verification

technique · direct, by degree reasons
1.1F1F2F3givenconstructalgebra

In polar coordinates f=cos⁡θ and the round downward gradient is sin⁡θ ∂θ. Multiply it by a smooth positive function of f equal to 4/(1+f) near N and 4/(1−f) near S, using cutoffs from [F3] and the positive constant 2 elsewhere. In the Cartesian radial Morse coordinates of radius 1−f at N and 1+f at S, the resulting field is 2w and −2w, respectively; explicitly they are w=(x,y)/1+z near N and w=(x,y)/1−z near S, hence smooth local Cartesian coordinates with nonsingular derivative at the pole. Thus X satisfies the normalized local model and strictly decreases f elsewhere. The only critical points are N,S, with Hessians negative and positive definite and hence indices 2,0. The unstable set of N and stable set of S are the complementary-pole open disks; the other two sets are single points, so all nonempty stable--unstable intersections are transverse. The smooth field is complete by [F3], so the pair is Morse--Smale. The chain groups in degree one are free on the empty set and are zero.

2.1F2step 1.1

The differentials out of and into degree one vanish identically: ∂2:CM2→CM1 has zero target and ∂1:CM1→CM0 has zero source. The remaining differentials ∂0 and ∂3 have zero target and zero source respectively. So all differentials are zero.

3.1F2step 1.1step 2.1

Although every meridian from N to S is a connecting trajectory, its index drop is two. The differential definition in [F2] counts index drop one only, so these trajectories supply no coefficient.

4.1step 2.1step 3.1∎

With zero differentials and one generator in degree 2 and one in degree 0, the mod-two complex has homology Z/2 in degrees 0 and 2 and zero elsewhere, and the integral complex has homology Z in degrees 0 and 2 and zero elsewhere.

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