Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge 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.

The circle as S1=R/Z with basepoint [0]

Definition

Use the canonical copy of Z inside R fixed in Integer part: for every real x there is exactly one integer m with m≤x<m+1. For x,y∈R, put

x∼y⟺x−y∈Z.

This is an equivalence relation. Indeed, x−x=0∈Z; if x−y∈Z, then y−x=−(x−y)∈Z; and if x−y,y−z∈Z, then x−z=(x−y)+(y−z)∈Z. The closure facts used here are part of the additive-group structure supplied by The integers form a commutative ring, and the quotient-set construction is that of The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection.

Let [x] denote the equivalence class of x. Let p:R→R/Z be the canonical projection, p(x)=[x]. Thus

p(x)=p(y)⟺x−y∈Z.

Let R/Z carry the quotient topology induced by p. The circle is S1:=R/Z with the quotient topology induced by p(x)=[x] and basepoint [0]; moreover p−1([0])=Z and p(x+n)=p(x) for every real x and integer n.

The last assertions follow directly from the displayed fibre criterion: p(x)=[0] exactly when x∈Z, while (x+n)−x=n∈Z.

Depends on

Used by

Dependency tree · two levels

34 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