Alphabeta Math
PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24
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 punctured plane has fundamental group Z, while punctured Rn is simply connected for n≥3

Statement

For n≥2, put Pn=Rn∖{0} and let e0=(1,0,…,0).

  1. The punctured plane satisfies π1(P2,e0)≅Z.
  2. For every n≥3, the space Pn is path-connected and π1(Pn,x) is trivial for every x∈Pn; hence Pn is simply connected.

Facts & Assumptions

Given: A natural number n≥2, the punctured Euclidean space Pn, its unit sphere Sn−1, and the standard point e0∈Sn−1.

[L1]

For n≥1, radial normalization r(x)=x/∥x∥2 is a retraction Pn→Sn−1, and H(x,t)=((1−t)+t/∥x∥2)x is a deformation retraction of Pn onto Sn−1 (For n≥1, radial normalisation is a deformation retraction of Rn∖{0} onto Sn−1).

[L2]

If A is a deformation retract of X, the inclusion and retraction induce mutually inverse fundamental-group isomorphisms at every basepoint of A (A retract induces an injection on fundamental groups, and a deformation retract induces an isomorphism).

[L3]

The geometric unit circle based at e0=(1,0) has fundamental group isomorphic to Z (The trigonometric loops give π1({(x,y):x2+y2=1},(1,0))≅Z).

[L4]

For every m≥2, the sphere Sm is simply connected (Sn is simply connected for every n≥2).

[L5]

Loop concatenation makes each fundamental group a group, with constant-loop identity and path reversal representing inverses (Loop classes form the group π1(X,x0) under concatenation).

Proof

technique · direct
1.1L1L2L3F1

For n=2, [L1] and [L2] identify π1(P2,e0) with π1(S1,e0), and [L3] identifies the latter with Z.

1.2givenL1L2L4

Let n≥3 and y∈Sn−1. Since n−1≥2, [L4] says that Sn−1 is simply connected, so π1(Sn−1,y) is trivial; [L1] and [L2] therefore make π1(Pn,y) trivial.

2.1step 1.2L1L5construct

For an arbitrary x∈Pn, the path γx(t)=((1−t)+t/∥x∥2)x runs in Pn from x to r(x). Concatenating an endpoint-fixed homotopy with the fixed paths γ‾x and γx preserves it, so Φx([α])=[γ‾x∗α∗γx] is well defined. The piecewise formula K(s,t)=γx(2s(1−t)) for s≤1/2 and K(s,t)=γx(2(1−s)(1−t)) for s≥1/2 contracts γx∗γ‾x to the constant path at x; applying the same formula to γ‾x contracts γ‾x∗γx at r(x). Hence the product of Φx([α]) and Φx([β]) cancels its middle γx∗γ‾x and equals Φx([α∗β]), while [δ]↦[γx∗δ∗γ‾x] is a two-sided inverse. Thus Φx:π1(Pn,x)→π1(Pn,r(x)) is an isomorphism, and step 1.2 makes π1(Pn,x) trivial.

3.1step 2.1L1L4construct∎

Given x,z∈Pn, follow γx to r(x), a sphere path from r(x) to r(z) supplied by the path-connectedness in [L4], and the reverse of γz. This gives a path from x to z, so Pn is path-connected. Together with step 2.1, this proves simple connectedness and completes both clauses.

Depends on

Used by

Dependency tree · two levels

44 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