ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14

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.

Homology of the loop space of an odd sphere

Statement

For every $m \geq 1$ , $H_{k} (Ω S^{2 m + 1}; Z) ≅ {\begin{cases} Z, & 2 m ∣ k, \\ 0, & 2 m ∤ k, \end{cases} (k \geq 0) .$ This is an additive calculation. It does not assert a Pontryagin-ring identification, and it uses no choice principle.

Facts & Assumptions

Given: $m \geq 1$ , $N = 2 m + 1$ , a basepoint of $S^{N}$ , and integral coefficients.

[F1]

Mapping path factorization supplies the Hurewicz path fibration $Ω S^{N} \to P S^{N} \to S^{N}$ . Its explicit path total space contracts by rescaling paths.

[F2]

$S^{n}$ is simply connected for every $n \geq 2$ says that $S^{N}$ is simply connected. In particular the based loop space is path connected: a nullhomotopy relative to the loop basepoint is a path to the constant loop.

[F3]

Homological Serre spectral sequence supplies the choice-free integral homological sequence, its bidegree, constant-coefficient clause, and strong convergence.

[F4]

Homology of spheres gives the two nonzero base homology groups. Contractible nonempty spaces have the homology of a point computes the path-space abutment.

Verification

technique · the contractible abutment makes the only possible family of differentials isomorphisms, yielding a recurrence for the unknown fiber groups

1.1

The path-space formula is $P S^{N} = {γ : I \to S^{N} : γ (0) = *}, p (γ) = γ (1) .$ The homotopy $H_{s} (γ) (t) = γ (s t)$ contracts it to the constant path; the compact-open exponential law makes this formula continuous. By [F2], any based loop has a based nullhomotopy, whose slices give a path in $Ω S^{N}$ , so $H_{0} (Ω S^{N}; Z) = Z$ .

F1F2F4

2.1

Write $G_{q} = H_{q} (Ω S^{N}; Z)$ . Since the base is simply connected, [F3, F4] give $E_{p, q}^{2} = {\begin{cases} G_{q}, & p = 0, N, \\ 0, & otherwise . \end{cases}$ The homological bidegree $(- r, r - 1)$ shows that every differential before page $N$ is zero and that the only possibly nonzero family is $d_{N} : E_{N, q}^{N} = G_{q} ⟶ E_{0, q + N - 1}^{N} = G_{q + N - 1} .$ There are no nonzero differentials after page $N$ . The contractibility in step 1.1 and [F4] say that the stable page is $Z$ at $(0, 0)$ and zero in every positive total degree.

F3F4step 1.1

3.1

For every $q \geq 0$ , the source $(N, q)$ has zero stable term, so $d_{N}$ has zero kernel. Its target has positive total degree $q + N - 1$ , so that stable term is also zero and $d_{N}$ has zero cokernel. Thus $G_{q} \overset{≅}{\to} G_{q + N - 1} = G_{q + 2 m} (q \geq 0) .$ For $0 < j < N - 1$ , the group $G_{j}$ in position $(0, j)$ has no possible incoming differential and must vanish. Together with $G_{0} = Z$ , induction on the quotient and remainder of $k$ by $N - 1 = 2 m$ gives exactly the displayed groups.

F3step 1.1step 2.1

4.1

When $m = 1$ , the recurrence has period two and gives $Z$ in every even degree and zero in every odd degree. Degree zero is the surviving $G_{0} = Z$ , not a target required to vanish. The proof also covers the zero groups, the first gap $1 \leq j < 2 m$ , the first isomorphism, both columns, both endpoints of every $d_{N}$ , and every remainder class. Each construction uses one supplied basepoint or one finite chain representative; neither an infinite family of choices nor AC is used. There is no ring claim, converse, or extension splitting.

F1F2F3F4step 1.1step 2.1step 3.1∎

Source notes

Hatcher, Example 5.5, printed p. 528, gives this complete two-column path-space calculation for $Ω S^{N}$ . The kernel, cokernel, and low-degree gap arguments are written separately in step 3.1 to make the induction and its endpoints explicit.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

35 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

Hatcher, Algebraic Topology, Example 5.5 (standard reference, not scraped)