Alphabeta Math
False statementConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

FALSE: every compact path-connected subset of R2 has a universal cover

Statement

Every compact path-connected subset of R2 admits a universal covering space.

Facts & Assumptions

Given: The Hawaiian earring H=n1CnR2, based at the common point 0.

[F1]

The Hawaiian earring is a compact and path-connected subset of R2 (The Hawaiian earring is compact and path-connected).

[F2]

For every n1, the Hawaiian earring admits a retraction onto its circle Cn (The Hawaiian earring retracts onto each of its circles).

[F3]

A space is semilocally simply connected at x when some neighbourhood U of x has inclusion-induced homomorphism π1(U,x)π1(X,x) trivial (Semilocally simply connected spaces with explicit basepoint convention).

[L1]

If a space admits a universal covering, then it is semilocally simply connected (A space admitting a universal covering is semilocally simply connected).

[L2]

Under the isomorphism from the geometric unit circle's fundamental group to Z, the once-around loop t(cos2πt,sin2πt) corresponds to 1 and is therefore nontrivial (The trigonometric loops give π1({(x,y):x2+y2=1},(1,0))Z).

[L3]

Induced maps on fundamental groups are functorial, so a homomorphism with a left inverse is injective (Induced fundamental-group maps are well defined, functorial and invariant under based homotopy).

[F5]

In a metric topology, every open set contains a metric ball about each of its points (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).

[L4]

For every real ε>0 there is an integer N1 with 1/N<ε (For every ε>0 in a complete ordered field there is a natural n1 with 1/n<ε).

Refutation

technique · direct
1.1

By [F1], H satisfies the compactness and path-connectedness hypotheses of the proposed statement.

F1
1.2

Let U be any neighbourhood of 0 in H. By [F4], there is an ambient open set OR2 with 0O and OHU. By [F5], choose ε>0 with B(0,ε)O, so HB(0,ε)U. Since CnB2(0,2/n), [L4] gives an n1 with CnU.

F1F4F5L4algebra
2.1

Let j:CnH be inclusion and rn:HCn the retraction of [F2]. Functoriality gives (rn)j=id, so j is injective. The pointed affine homeomorphism z(1/n,0)(1/n)z carries the geometric unit circle based at (1,0) onto Cn based at 0 and carries the once-around loop of [L2] to a loop n in Cn. By [L2] and [L3], [n]1 in π1(Cn,0); injectivity of j therefore makes its image nontrivial in π1(H,0). Since CnU, the same n is a loop in U.

step 1.2F2L2L3
3.1

Since every neighbourhood U of 0 contains such a loop, no inclusion-induced map π1(U,0)π1(H,0) is trivial. Thus H is not semilocally simply connected at 0.

step 1.2step 2.1F3
4.1

By [L1], the Hawaiian earring has no universal cover. Together with step 1.1, it is a compact path-connected planar counterexample to the proposed universal claim.

step 1.1step 3.1L1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

40 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