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

✓ 7 results · all verified · 6 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Fundamental Group of the Circle — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17Open item page →

An interval of length one need not embed under p:R→R/Z

Statement refuted

The strict bound in The quotient map is open, and every interval shorter than one embeds in R/Z cannot be replaced uniformly by length at most one. In particular, the claim that p∣J is a homeomorphism onto its image for every open, closed, or half-open interval J of length at most one is false.

Facts & Assumptions

Given: The quotient map p:R→R/Z and the intervals [0,1) and [0,1].

[L1]

The continuous quotient projection has p(x)=[x], with p(x)=p(y) exactly when x−y∈Z (The circle as S1=R/Z with basepoint [0]).

[L5]

Every real x has a unique integer m with m≤x<m+1 (Integer part: for every real x there is exactly one integer m with m≤x<m+1).

[L6]

For a continuous bijection, being a homeomorphism is equivalent to being an open map (A continuous bijection is a homeomorphism iff it is open iff it is closed, and homeomorphy is an equivalence relation on spaces).

[L7]

The quotient map is open, and every interval shorter than one embeds in R/Z (The quotient map is open, and every interval shorter than one embeds in R/Z).

Counterexample

technique · direct
1.1L1L3L5algebra

The restriction f=p∣[0,1) is continuous by [L1] and [L3]. It is surjective: for x∈R, [L5] gives r=x−⌊x⌋∈[0,1) with p(r)=p(x). It is injective: if r,s∈[0,1) and p(r)=p(s), then [L1] gives r−s∈Z and ∣r−s∣<1, so r=s. Thus f is a continuous bijection onto R/Z.

2.1step 1.1L1L2L4L6

The set A=[0,1/2) is relatively open in [0,1), since A=(−1/2,1/2)∩[0,1) by [L4]. Its image satisfies p−1(p[A])=⋃n∈Z[n,n+1/2) by [L1]. This union is not open at any integer, in particular at 0, so [L2] says p[A] is not open in the quotient. Hence the continuous bijection f is not open and is not a homeomorphism by [L6].

3.1L1L7algebra∎

The other endpoint convention fails differently: on [0,1] one has p(0)=p(1) by [L1], so the restriction is not injective and cannot be a homeomorphism onto its image. Both intervals have length one, which refutes the proposed replacement of the strict bound in [L7] by length at most one.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-17Open item page →

A loop that traverses the circle once and then pauses is homotopic to the standard loop

Example

Define u:I→R by

u(t)={2t,0≤t≤1/2,1,1/2≤t≤1,

and put α=p∘u. Then α traverses the quotient circle once during the first half of the parameter interval and remains at [0] during the second half. It is path-homotopic to ω1.

Facts & Assumptions

Given: The displayed function u and the loop α=p∘u.

[L1]

For every integer n, define ω~n(t)=nt and ωn=p∘ω~n (The standard circle loops ωn(t)=[nt] for n∈Z).

[L3]

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).

[L4]

Degree is the endpoint of the unique lift beginning at zero (The degree of a based circle loop).

[L5]

deg⁡(ωn)=n for every integer n (deg⁡(ωn)=n for every integer n).

[L6]

Straight-line interpolation between two continuous real-valued maps is a continuous homotopy (For continuous maps into a convex subset of Rn, the straight-line formula defines a continuous homotopy).

[L7]

The quotient projection is continuous, p(0)=[0], and p(1)=[0] (The circle as S1=R/Z with basepoint [0]).

Verification

technique · direct
1.1L3L4L7L8

The two formulas for u agree at t=1/2, where both equal 1, and each piece is continuous by [L8], so [L3] makes u continuous. It has u(0)=0 and u(1)=1, hence [L7] makes α=p∘u a based loop. Since u starts at zero and projects to α, it is the defining lift and [L4] gives deg⁡(α)=u(1)=1.

2.1step 1.1L1L5

By [L1], the standard loop ω1 is the projection of v(t)=t, and [L5] gives deg⁡(ω1)=1=deg⁡(α).

3.1step 1.1step 2.1L6L7∎

The formula K(t,s)=(1−s)u(t)+st is a continuous homotopy from u to v by [L6]. Since u(0)=v(0)=0 and u(1)=v(1)=1, it fixes both endpoints for every s. Postcomposing with p gives the explicit path homotopy H(t,s)=p(K(t,s)) from α to ω1, relative to t=0,1.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17Open item page →

A surjective circle loop can have degree zero and be nullhomotopic

Example

Define u:I→R by

u(t)={2t,0≤t≤1/2,2−2t,1/2≤t≤1,

and put α=p∘u. The loop α is surjective and nonconstant, but it has degree zero and is nullhomotopic.

Facts & Assumptions

Given: The displayed out-and-back function u and its projection α=p∘u.

[L1]

The continuous quotient projection satisfies p(x)=p(y) exactly when x−y∈Z, and p−1([0])=Z (The circle as S1=R/Z with basepoint [0]).

[L2]

Degree is the terminal value of the unique lift beginning at zero (The degree of a based circle loop).

[L3]

A based circle loop is nullhomotopic exactly when its degree is zero (A based circle loop is nullhomotopic exactly when its degree is zero).

[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).

[L6]

Every real x has a unique integer m with m≤x<m+1 (Integer part: for every real x there is exactly one integer m with m≤x<m+1).

Verification

technique · direct
1.1L4L5algebra

At t=1/2 both formulas give 1. Each piece is continuous by [L5], so [L4] makes u continuous. Its values at the boundary are u(0)=0, u(1/2)=1, and u(1)=0.

2.1step 1.1L1L2L7

By [L1] and [L7], α=p∘u is a continuous based loop at [0]. The function u is a lift of α beginning at zero, so [L2] gives deg⁡(α)=u(1)=0.

3.1step 1.1step 2.1L1L6algebra

Let [x]∈R/Z. By [L6], r=x−⌊x⌋∈[0,1) and p(r)=p(x). For t=r/2∈[0,1/2), the first formula gives u(t)=r, so α(t)=[x]; hence α is surjective. It is nonconstant because α(0)=[0] while α(1/4)=[1/2]≠[0], the latter inequality following from 1/2∉Z in [L1].

4.1step 2.1step 3.1L3∎

Step 2.1 gives degree zero, so the reverse direction of [L3] makes α nullhomotopic. Step 3.1 shows that nullhomotopy here neither forces constancy nor prevents surjectivity.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17Open item page →

The geometric loops t↦(cos⁡2πnt,sin⁡2πnt) have degree n

Example

For every integer n, the based geometric loop

γn(t)=(cos⁡2πnt,sin⁡2πnt)

has degree n, where degree is transported from the quotient-circle model by the based homeomorphism.

Facts & Assumptions

Given: An integer n and the quotient-circle dictionary.

[L1]

[t]↦(cos⁡2πt,sin⁡2πt) is a homeomorphism from R/Z to the unit circle and sends [0] to (1,0) ([t]↦(cos⁡2πt,sin⁡2πt) is a homeomorphism from R/Z to the unit circle).

[L2]

deg⁡(ωn)=n for every integer n (deg⁡(ωn)=n for every integer n).

[L3]

For every integer n, ωn(t)=[nt] (The standard circle loops ωn(t)=[nt] for n∈Z).

Verification

technique · direct
1.1L1L3algebra

Under the homeomorphism of [L1], the loop in [L3] has image t↦(cos⁡(2πnt),sin⁡(2πnt))=γn(t).

2.1step 1.1L2∎

The quotient loop has degree n by [L2], so the transported degree of its geometric image γn is also n. At n=0 this is the constant loop, and the same computation covers every negative n.

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17Open item page →

Based circle loops with the same endpoints need not be path-homotopic

Statement refuted

The claim that any two based circle loops with the same initial and terminal points are path-homotopic relative to those endpoints is false.

Facts & Assumptions

Given: The standard loops ω0 and ω1 in R/Z.

[L1]

A based loop at x0 is a path whose values at both endpoints are x0 (Based loops and the fundamental group).

[L2]

A based circle loop is nullhomotopic exactly when its degree is zero (A based circle loop is nullhomotopic exactly when its degree is zero).

[L3]

deg⁡(ωn)=n for every integer n (deg⁡(ωn)=n for every integer n).

[L4]

For every integer n, ωn(t)=[nt], and ω0 is constant (The standard circle loops ωn(t)=[nt] for n∈Z).

Counterexample

technique · direct
1.1L1L3L4

By [L4], ω0(0)=ω0(1)=[0] and ω1(0)=[0]=[1]=ω1(1), so both satisfy the two endpoint equalities in [L1]. Their degrees are 0 and 1 by [L3].

2.1step 1.1L2L3algebra∎

If ω0 and ω1 were path-homotopic relative to the endpoints, then ω1 would be path-homotopic to the constant loop and hence nullhomotopic. But [L2] and [L3] rule this out because deg⁡(ω1)=1≠0. Thus equal endpoints do not imply path homotopy.

ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17Open item page →

A covering quotient of a simply connected space need not be simply connected

Example

The real line is simply connected, but its quotient by integer translations is not. The canonical projection

p:R⟶R/Z

is both a quotient map and a covering map. Thus neither a quotient map nor a covering map transfers simple connectedness from its total space to its base in general.

Facts & Assumptions

Given: The real line, its integer-translation quotient, and the canonical projection p.

[L1]

If n≥1 and C⊆Rn is nonempty and convex, then C is simply connected (Every nonempty convex subset of Rn is simply connected).

[L2]

p:R→R/Z is the quotient projection defining the quotient circle (The circle as S1=R/Z with basepoint [0]).

[L4]

R/Z is not simply connected (R/Z is not simply connected).

Verification

technique · direct
1.1L1

The real line is a nonempty convex subset of R1, so [L1] with n=1 makes R simply connected.

1.2L2L3

The same explicit map p is a quotient map by [L2] and a covering map by [L3].

2.1step 1.1step 1.2L4∎

Its base is not simply connected by [L4], whereas its total space is simply connected by step 1.1. Step 1.2 therefore supplies both announced failures of preservation.

False statementConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17Open item page →

FALSE: every continuous self-map of the circle is nullhomotopic

Statement

False claim: every continuous map f:R/Z→R/Z is nullhomotopic.

The identity map is a counterexample.

Facts & Assumptions

Given: The identity map of S1=R/Z.

[A1]

A map f:X→Y is nullhomotopic if it is homotopic to a constant map cy0:X→Y for some y0∈Y (Nullhomotopic maps and contractible spaces).

[L2]

A homotopy H:Y×I→B through a covering has a unique lift extending any prescribed lift of H(−,0) (Existence and uniqueness of homotopy lifts through a covering map).

[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]

The standard loop ω1 is t↦[t] (The standard circle loops ωn(t)=[nt] for n∈Z).

[L5]

For the quotient projection, p(x)=p(y) exactly when x−y∈Z, and p(x+n)=p(x) for every integer n (The circle as S1=R/Z with basepoint [0]).

Refutation

technique · contradiction
1.1A1assume-contra

Suppose, for contradiction, that the identity is nullhomotopic. By [A1], there are c∈R/Z and a homotopy H with H(y,0)=y and H(y,1)=c. Reverse its time coordinate to obtain K(y,t)=H(y,1−t), so K(y,0)=c and K(y,1)=y.

2.1step 1.1L1L2choose

Since p is surjective, choose a∈R with p(a)=c. The constant map y↦a lifts K(−,0), so [L1] and [L2] give a lift K~:(R/Z)×I→R. Define s(y)=K~(y,1). Then s is continuous and p(s(y))=K(y,1)=y, so p∘s is the identity: s is a section of p.

3.1step 2.1L3L4L5L6

The path s∘ω1 is a lift of ω1 because p∘s is the identity, and it is closed because ω1(0)=ω1(1)=[0]. Put m=s([0])∈Z by [L5]. The path t↦m+t is another lift of ω1 starting at m, since [L4] and [L5] give p(m+t)=[t]; it is continuous by [L6]. Uniqueness in [L3] forces s(ω1(t))=m+t, whose endpoint is m+1≠m, contradicting that s∘ω1 is closed.

4.1step 1.1step 2.1step 3.1discharge-contradiction∎

The contradiction discharges the assumption of step 1.1. Hence the identity is not nullhomotopic, and the universal claim is false.

Sources