ExampleConstruction: Literature-sourcedVerification: 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 Hawaiian earring retracts onto each of its circles

Example

For every $n \geq 1$ , the Hawaiian earring admits a retraction onto its circle $C_{n}$ .

Facts & Assumptions

Given: The Hawaiian earring $H = ⋃_{m \geq 1} C_{m}$ and a fixed integer $n \geq 1$ .

[F1]

For every integer $m \geq 1$ , $C_{m}$ is the circle of radius $1 / m$ centred at $(1 / m, 0)$ , and $H = ⋃_{m \geq 1} C_{m}$ (The Hawaiian earring is compact and path-connected).

[F2]

A continuous map $r : X \to A$ that restricts to the identity on $A$ is a retraction (Retractions and deformation retracts, with a deformation retraction required to fix the retract pointwise).

[L1]

A function is continuous exactly when the preimage of every open set is open (For a map of spaces the following agree: continuity at every point, preimages of open sets open, preimages of closed sets closed, preimages of subbasic open sets open, and $f (\overline{A}) \subseteq \overline{f (A)}$ ).

[F3]

Open subsets of a subspace are intersections with ambient open sets (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace).

[L2]

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

[L3]

The Euclidean norm satisfies the reverse triangle inequality $∣ ∥ u ∥_{2} - ∥ v ∥_{2} ∣ \leq ∥ u - v ∥_{2}$ (The finite and reverse triangle inequalities for a norm; and for $n \geq 1$ every norm $N$ on $R^{n}$ satisfies $N (x) \leq C ∥ x ∥_{1}$ and is Lipschitz, hence continuous, for $d_{2}$ ).

Verification

technique · constructive

1.1givenF1constructalgebra

Define $r_{n} : H \to C_{n}$ by $r_{n} (x) = x$ for $x \in C_{n}$ and $r_{n} (x) = 0$ for $x \in C_{m}$ with $m \neq n$ . Distinct circles meet only at $0$ : subtracting their equations $x_{1}^{2} + x_{2}^{2} = 2 x_{1} / m$ and $x_{1}^{2} + x_{2}^{2} = 2 x_{1} / k$ gives $x_{1} = x_{2} = 0$ . Thus the clauses agree and define a function.

2.1step 1.1F1L2L3algebra

Let $x \in C_{m} ∖ {0}$ and put $d = ∥ x ∥_{2} > 0$ . By [L2], choose $N$ with $2 / N < d / 2$ ; then every $C_{k}$ with $k \geq N$ lies in $B (0, d / 2)$ and is disjoint from $B (x, d / 2)$ . For each of the finitely many $k < N$ with $k \neq m$ , the positive number $∣ ∥ x - (1 / k, 0) ∥_{2} - 1 / k ∣$ and [L3] give a ball about $x$ missing $C_{k}$ ; intersect these finitely many balls with $B (x, d / 2)$ . The resulting relative neighbourhood in $H$ meets only $C_{m}$ , so there $r_{n}$ is the identity when $m = n$ and the constant map $0$ when $m \neq n$ .

3.1step 1.1step 2.1F3L1

Let $V \subseteq C_{n}$ be open and let $x \in r_{n}^{- 1} [V]$ . If $x \neq 0$ and $x \in C_{m}$ , step 2.1 gives a relative open neighbourhood $N$ of $x$ meeting only $C_{m}$ . When $m = n$ , write $V = O \cap C_{n}$ by [F3] and replace $N$ by $N \cap O$ ; the identity clause of $r_{n}$ then maps it into $V$ . When $m \neq n$ , one has $r_{n} (x) = 0 \in V$ and the constant clause maps all of $N$ into $V$ . If $x = 0$ , then $0 \in V$ ; write $V = O \cap C_{n}$ and choose an ambient open neighbourhood $W$ of $0$ with $W \subseteq O$ . Every point of $W \cap C_{n}$ is fixed and every point of $W \cap C_{m}$ for $m \neq n$ maps to $0$ , so $W \cap H \subseteq r_{n}^{- 1} [V]$ . Thus every point of $r_{n}^{- 1} [V]$ has a relative open neighbourhood inside it, making that preimage open. The criterion [L1] now shows that $r_{n}$ is continuous.

4.1step 3.1F2discharge-construct∎

The continuous map $r_{n}$ restricts to the identity on $C_{n}$ , so it is a retraction of $H$ onto $C_{n}$ .

Depends on

Used by

FALSE: every compact path-connected subset of ℝ² has a universal cover False statement

Dependency tree · two levels

49 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, Example 1.25 (standard reference, not scraped)