Alphabeta Math
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.

Lifts of circle-loop concatenations and reversals

Statement

Let α and β be based loops in R/Z, and let their lifts from zero be α~ and β~, with terminal values m and n. The lift of α∗β from zero is

α∗β~(t)={α~(2t),0≤t≤1/2,m+β~(2t−1),1/2≤t≤1,

and it ends at m+n. The lift of the reversed loop αˉ from zero is

αˉ~(t)=α~(1−t)−m,

and it ends at −m. Thus lifts of circle-loop concatenations and reversals have endpoints equal to the sum and the negative of the original endpoints.

Facts & Assumptions

Given: Based loops α,β, their lifts α~,β~ from zero, and terminal values m=α~(1) and n=β~(1).

[L1]

For a based circle loop γ with lift γ~ from zero, the terminal value γ~(1) is an integer and deg⁡(γ)=γ~(1) (The degree of a based circle loop).

[L2]

The product [α][β] traverses α first and β second, and is represented by α∗β (Based loops and the fundamental group).

[L3]

A path through a covering has a unique lift once its initial point is prescribed (Existence and uniqueness of path lifts through a covering map).

[L4]

Functions continuous on each member of a finite closed cover, and agreeing where the pieces meet, paste to a continuous function (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous).

[L5]

For the quotient projection p, one has p(x+k)=p(x) for every real x and integer k (The circle as S1=R/Z with basepoint [0]).

Proof

technique · direct
1.1L1L2L4L5L6

Define γ by the displayed two-piece formula. At t=1/2 the left value is α~(1)=m and the right value is m+β~(0)=m, so [L4] and [L6] make γ continuous. It starts at zero. By [L5], its first half projects to α(2t) and its second half to β(2t−1), in the order fixed by [L2], so p∘γ=α∗β; its endpoint is m+n.

1.2L1L5L6algebra

Define δ(t)=α~(1−t)−m. It is continuous by [L6], begins at m−m=0, and ends at 0−m=−m. Since m∈Z by [L1], [L5] gives p(δ(t))=p(α~(1−t))=α(1−t)=αˉ(t).

2.1step 1.1step 1.2L3∎

Both γ and δ are lifts with initial point zero, so uniqueness in [L3] identifies them with the defining lifts of α∗β and αˉ. Their endpoints are therefore m+n and −m, respectively.

Depends on

Used by

Dependency tree · two levels

38 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