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

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.

Freudenthal stable range for spheres

Example

For $n \geq 1$ , suspension gives an isomorphism $π_{i} (S^{n}) \to π_{i + 1} (S^{n + 1})$ for $1 \leq i < 2 n - 1$ and a surjection for $i = 2 n - 1$ . The degree-zero map is a bijection of singleton pointed sets. For a fixed integer $k \geq 0$ , every transition in the sequence $π_{n + k} (S^{n}) \to π_{n + k + 1} (S^{n + 1}) \to \dots$ is an isomorphism once $n > k + 1$ . At $n = k + 1$ the theorem promises only surjectivity. These statements are choice-free and do not compute any additional unstable group.

Facts & Assumptions

[F1]

Freudenthal suspension theorem gives the exact isomorphism range and surjective endpoint for an $(n - 1)$ -connected based CW space, using its unreduced two-cone suspension based at the lower apex, without AC.

[F2]

The adjunction space $Y \cup_{f} X$ glued along a continuous map, and, for a nonempty space, the cone and the suspension as quotients of $X \times [0, 1]$ gives the quotient model with two distinct apices, here rescaled to the height interval $[- 1, 1]$ .

[F3]

The singleton case of The first potentially nonzero homotopy group of a wedge of higher spheres has its cell basis, including its proof's CW construction, makes $S^{n}$ a path-connected CW complex with $π_{j} (S^{n}) = 0$ for $0 < j < n$ , for $n \geq 2$ . Only this connectivity clause is used.

[F4]

Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line gives compactness of $S^{n} \times [- 1, 1]$ as a closed bounded Euclidean subset. In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones makes a continuous bijection from its compact quotient to a Hausdorff space a homeomorphism, by the closed-image argument.

[F5]

Higher homotopy basepoint transport and moving homotopies gives the explicit choice-free change-of-basepoint isomorphisms if different sphere basepoints are specified.

Verification

Given: $n \geq 1$ . Begin with any specified source sphere basepoint and use the lower apex on its suspension.

1.1

For $n \geq 2$ , [F3] supplies exactly the $(n - 1)$ -connectivity and CW hypotheses of [F1]. For $n = 1$ , the circle is the quotient of one closed interval with its endpoints identified, with one vertex and one open edge. Its characteristic interval is a quotient map, so this is its finite CW weak topology; path connectedness follows from its interval parametrization. Thus it is $0$ -connected, which is all [F1] requires in this case. The constant loops and the sole component are included; no positive connectivity is claimed for $S^{1}$ .

F1F3given

2.1

The map $Φ : Σ S^{n} ⟶ S^{n + 1}, [x, t] ⟼ (\sqrt{1 - t^{2}} x, t)$ is well defined and continuous by [F2]: at either endpoint the first coordinates vanish independently of $x$ . It is bijective, since for $- 1 < t < 1$ the inverse recovers $t$ as the last coordinate and $x$ by division by $\sqrt{1 - t^{2}}$ , while the two poles have precisely their respective apex preimages. Its source is compact as a quotient of the compact set in [F4], so [F4] makes it a homeomorphism. The lower apex goes to $(0, \dots, 0, - 1)$ . Postcomposition with this homeomorphism and its inverse gives inverse maps on based homotopy classes and preserves concatenation, so [F1] and step 1.1 give the asserted sphere ranges. If a different target basepoint is desired, a specified sphere path and [F5] transport these isomorphism or surjectivity assertions. At $t = \pm 1$ no division formula is used.

F1F2F4F5step 1.1

3.1

Put $i = n + k$ with $k \geq 0$ . The inequality $i < 2 n - 1$ is exactly $n + k < 2 n - 1$ , or $n > k + 1$ . If it holds, it continues to hold with $n$ replaced by $n + r$ for every $r \geq 0$ , so every subsequent suspension transition is an isomorphism by step 2.1. Thus the sequence is constant up to these specified isomorphisms from that index onward. At equality $n = k + 1$ , $i = 2 n - 1$ is precisely the surjective endpoint, with no injectivity conclusion supplied. For example $k = 0$ is in the isomorphism range for $n \geq 2$ and only the surjective endpoint at $n = 1$ ; $k = 1$ is in the isomorphism range for $n \geq 3$ and at the endpoint for $n = 2$ . Degree zero consists of the singleton components and the trivial target fundamental group by [F1]. The case $n = 0$ is outside this assertion. Neither these arithmetic bounds nor the compact quotient and basepoint comparisons introduce AC.

F1F5step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

66 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 Corollary 4.24; May Chapter 11 §2 (standard reference, not scraped)