ExampleConstruction: AI-adaptedVerification: 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.

Radial normalization retracts the punctured disk, but it cannot extend to the disk

Example

Let $D^{2} = {\overline{B}}_{2} (0, 1)$ and define

$ρ : D^{2} ∖ {0} ⟶ S^{1}, ρ (x) = \frac{x}{∥ x ∥_{2}} .$

This map retracts the punctured disk onto the unit circle, but it has no continuous extension to all of $D^{2}$ .

Facts & Assumptions

Given: The punctured closed disk $D^{2} ∖ {0}$ and radial normalization $ρ$ .

[L1]

On $R^{2} ∖ {0}$ , radial normalization is a retraction onto $S^{1}$ and is part of a deformation retraction (For $n \geq 1$ , radial normalisation is a deformation retraction of $R^{n} ∖ {0}$ onto $S^{n - 1}$ ).

[L2]

There is no continuous retraction $D^{2} \to S^{1}$ (There is no retraction of the closed disk onto the unit circle).

[F1]

The closed unit disk and unit circle are ${\overline{B}}_{2} (0, 1)$ and $S_{2} (0, 1)$ (Euclidean spheres and closed balls as subspaces of $R^{n}$ ).

Verification

technique · direct

1.1givenF1L1

Restricting the retraction in [L1] to $D^{2} ∖ {0}$ gives a continuous map into $S^{1}$ , and every $x \in S^{1}$ satisfies $ρ (x) = x$ . Thus $ρ$ retracts the punctured disk onto the unit circle.

2.1step 1.1L2

If a continuous extension $\overset{ˉ}{ρ} : D^{2} \to S^{1}$ existed, it would still satisfy $\overset{ˉ}{ρ} (x) = x$ on $S^{1}$ , so it would be a retraction, contrary to [L2].

3.1step 1.1algebra∎

The failure at the missing point is also visible directly: for every $0 < t \leq 1$ , $ρ (t, 0) = (1, 0)$ while $ρ (- t, 0) = (- 1, 0)$ . The two radial approaches to $0$ therefore have different constant images, so $ρ$ has no limit at $0$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 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, proof of Theorem 1.9 (standard reference, not scraped)
J. Peter May, A Concise Course in Algebraic Topology, Chapter 1, §6 (standard reference, not scraped)