ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21

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 once-punctured two-sphere has trivial fundamental group and the twice-punctured two-sphere has fundamental group $Z$

Example

Let $N = (0, 0, 1)$ and $S = (0, 0, - 1)$ in $S^{2}$ . Point $S^{2} ∖ {N}$ at any point corresponding under stereographic projection to $0 \in R^{2}$ , and point $S^{2} ∖ {N, S}$ at the point corresponding to $(1, 0)$ . Then

$π_{1} (S^{2} ∖ {N}) = 1, π_{1} (S^{2} ∖ {N, S}) ≅ Z .$

Facts & Assumptions

Given: The two punctured spaces and basepoints in the Example.

[L1]

Stereographic projection identifies a pole complement in $S^{2}$ with $R^{2}$ and the double pole complement with $R^{2} ∖ {0}$ (Antipodal complements cover $S^{n}$ by simply connected sets with path-connected overlap for $n \geq 2$ ).

[F1]

Every nonempty convex subset of Euclidean space is simply connected (Every nonempty convex subset of $R^{n}$ is simply connected).

[L2]

The punctured plane pointed at $(1, 0)$ has fundamental group isomorphic to $Z$ ( $π_{1} (R^{2} ∖ {0}) ≅ Z$ ).

[F2]

A pointed homeomorphism induces a fundamental-group isomorphism (Induced fundamental-group maps are well defined, functorial and invariant under based homotopy).

Verification

technique · direct

1.1L1

By [L1], stereographic projection is a pointed homeomorphism $S^{2} ∖ {N} ≅ R^{2}$ for the chosen basepoints.

1.2L1

The same stereographic projection restricts by [L1] to a pointed homeomorphism $S^{2} ∖ {N, S} ≅ R^{2} ∖ {0}$ .

2.1step 1.1F1F2

The plane is nonempty and convex, so [F1] makes its fundamental group trivial; [F2] transports that calculation through step 1.1.

3.1step 1.2L2F2∎

By [L2] the latter space has fundamental group $Z$ , and [F2] transports this group through step 1.2.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

24 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

Allen Hatcher, Algebraic Topology, Proposition 1.14 and Chapter 1 examples (standard reference, not scraped)

The once-punctured two-sphere has trivial fundamental group and the twice-punctured two-sphere has fundamental group ZZ