LemmaStatement: AI-adaptedProof: 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.

An antipodal circle map has odd lift increment and is not nullhomotopic

Statement

On $S^{1} = R / Z$ , define the antipodal involution by $a ([u]) = [u + 1 / 2]$ . If a continuous map $h : S^{1} \to S^{1}$ satisfies $h \circ a = a \circ h$ , then every lift $\tilde{h} : [0, 1] \to R$ of $t \mapsto h ([t])$ has

$\tilde{h} (1) - \tilde{h} (0) = 2 k + 1$

for some integer $k$ . Thus the lift increment is odd, possibly negative, and the loop $t \mapsto h ([t])$ is not nullhomotopic.

Facts & Assumptions

Given: A continuous map $h : S^{1} \to S^{1}$ with $h \circ a = a \circ h$ .

[F1]

For the quotient map $p : R \to R / Z$ , one has $p (x) = p (y)$ exactly when $x - y \in Z$ , and $p (x + m) = p (x)$ for every integer $m$ (The circle as $S^{1} = R / Z$ with basepoint $[0]$ ).

[L1]

The quotient map $p : R \to R / Z$ is a covering map ( $p : R \to R / Z$ is a covering map with translated interval sheets).

[L2]

A path in the base of a covering has a unique lift after its initial lift point is fixed (Existence and uniqueness of path lifts through a covering map).

[L3]

Endpoint-fixed homotopic paths have lifts with the same endpoint whenever their lifts begin at the same point (The endpoint of a lifted path depends only on its endpoint-fixed homotopy class).

Proof

technique · contradiction

1.1

If $[u] = [v]$ , then $(u + 1 / 2) - (v + 1 / 2) = u - v \in Z$ , so $a ([u]) = [u + 1 / 2]$ is well defined by [F1]; moreover $a (a ([u])) = [u + 1] = [u]$ , so $a$ is an involution.

F1algebra

1.2

Suppose the loop $t \mapsto h ([t])$ were endpoint-fixed homotopic to the constant loop at $h ([0])$ .

assume-contra

2.1

Let $y \in R$ be arbitrary subject to $p (y) = h ([0])$ . By [L1] and [L2], the loop $t \mapsto h ([t])$ has a unique lift $\tilde{h}$ with $\tilde{h} (0) = y$ . Antipodality gives $p (\tilde{h} (1 / 2)) = h ([1 / 2]) = p (y + 1 / 2)$ , so [F1] gives a unique integer $k$ with $\tilde{h} (1 / 2) = y + k + 1 / 2$ .

step 1.1givenF1L1L2

3.1

For $0 \leq t \leq 1 / 2$ , the paths $t \mapsto \tilde{h} (t + 1 / 2)$ and $t \mapsto \tilde{h} (t) + k + 1 / 2$ project to the same path because $h ([t + 1 / 2]) = a (h ([t]))$ , and they agree at $t = 0$ by step 2.1. Lift uniqueness gives $\tilde{h} (t + 1 / 2) = \tilde{h} (t) + k + 1 / 2$ , so at $t = 1 / 2$ one obtains $\tilde{h} (1) = y + 2 k + 1$ .

step 2.1F1L2algebra

4.1

The constant loop at $h ([0])$ has the constant lift beginning at $y$ , so [L3] and step 1.2 would force $\tilde{h} (1) = y$ . Step 3.1 instead gives $\tilde{h} (1) = y + 2 k + 1 \neq y$ for every integer $k$ , including negative $k$ . This contradiction shows that the loop is not nullhomotopic and completes the odd-increment claim.

step 3.1step 1.2L3algebradischarge-contradiction∎

Depends on

Used by

Borsuk–Ulam theorem in dimension two 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, proof of Theorem 1.10 (standard reference, not scraped)