LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17

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.

Based circle loops of equal degree are path-homotopic

Statement

Based circle loops of equal degree are path-homotopic.

Facts & Assumptions

Given: Based loops $α, β : I \to R / Z$ at $[0]$ with $\deg (α) = \deg (β)$ .

[L1]

Each based circle loop $γ$ has a unique lift $\tilde{γ}$ beginning at zero, with $\deg (γ) = \tilde{γ} (1)$ (The degree of a based circle loop).

[L2]

If $n \geq 1$ , $C \subseteq R^{n}$ is convex, and $f, g : X \to C$ are continuous, then $H (x, t) = (1 - t) f (x) + t g (x)$ is a continuous homotopy from $f$ to $g$ (For continuous maps into a convex subset of $R^{n}$ , the straight-line formula defines a continuous homotopy).

[L3]

If $v : Y \to Z$ is continuous and $f ≃_{A} g$ , then $v \circ f ≃_{A} v \circ g$ (Precomposition and postcomposition by continuous maps preserve homotopies, including their relative form).

[L4]

The quotient projection $p : R \to R / Z$ is continuous (The circle as $S^{1} = R / Z$ with basepoint $[0]$ ).

Proof

technique · direct

1.1givenL1

Let $\tilde{α}$ and $\tilde{β}$ be the lifts from [L1]. Both begin at zero, and the degree hypothesis with [L1] gives $\tilde{α} (1) = \tilde{β} (1)$ .

2.1step 1.1L2algebra

Since $R$ is convex, [L2] makes $H (t, s) = (1 - s) \tilde{α} (t) + s \tilde{β} (t)$ continuous. Step 1.1 gives $H (0, s) = 0$ and $H (1, s) = \tilde{α} (1) = \tilde{β} (1)$ for every $s$ , so this homotopy fixes both endpoints.

3.1step 2.1L1L3L4∎

Postcomposing with the continuous quotient projection, [L3] and [L4] give an endpoint-fixed homotopy $p \circ H$ . The defining lift equations in [L1] identify its endpoints as $p \circ \tilde{α} = α$ and $p \circ \tilde{β} = β$ . Hence the loops are path-homotopic.

Depends on

Used by

Two based circle loops are path-homotopic if and only if they have equal degree Theorem

Dependency tree · two levels

17 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, Ch. 1, Section 1.1 (standard reference, not scraped)
J. Peter May, A Concise Course in Algebraic Topology, Ch. 1, Section 5 (standard reference, not scraped)