ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16

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 quotient $R \to R / Z$ is a covering with integer translations as deck transformations

Example

For the quotient by integer translation, $q : R \to R / Z$ is a covering map, and every deck transformation is a unique translation $x \mapsto x + n$ with $n \in Z$ .

Facts & Assumptions

Given: The objects, hypotheses, and choice principles stated above.

[F1]

For a covering-space action of $G$ on $E$ , the orbit map $E \to E / G$ is a covering. If $E$ is path-connected, the deck group of this covering consists exactly of the transformations supplied by $G$ . (The orbit map of a covering-space action is a covering, with the acting group equal to the deck group when the total space is path-connected).

[F2]

For a covering $p : E \to B$ , a deck transformation is an isomorphism $h : E \to E$ over $B$ , so $p \circ h = p$ (def-map-and-isomorphism-of-covering-spaces). Deck transformations form the deck group $Deck (p)$ under composition, and this group acts on $E$ by evaluation (def-group, def-group-action). (Deck transformations and the deck-transformation group of a covering).

[F3]

The quotient topology. Let $(X, T)$ be a topological space (def-topological-space), let $Y$ be a set and let $q : X \to Y$ be a surjection (def-injection-surjection-bijection). The quotient topology on $Y$ induced by $q$ is the final topology of the one-element family $(q)$ (def-initial-and-final-topology): $T_{q} : = {V \subseteq Y : q^{- 1} [V] \in T} .$ That this is a topology is discharged in def-initial-and-final-topology, where every final topology is verified to satisfy (T1), (T2) and (T3). Dually, $C \subseteq Y$ is closed in $T_{q}$ exactly when $q^{- 1} [C]$ is closed in $X$ , because $q^{- 1} [Y ∖ V] = X ∖ q^{- 1} [V]$ . (The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection).

[F4]

On the set $N \times N$ of pairs of natural numbers, define $(a, b) \sim (c, d) ⟺ a + d = b + c .$ This is an equivalence relation (lem-int-equivalence). The integers are the quotient $Z : = (N \times N) / \sim,$ and we write $[(a, b)]$ for the equivalence class of $(a, b)$ . (The integers as equivalence classes of pairs of naturals).

[F5]

Identify $Z$ with its canonical copy inside $R$ along the embeddings $N \to Z \to Q \to R$ ; then for every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ , written $⌊ x ⌋$ (Integer part: for every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ ).

Verification

technique · direct

1.1

By [F5] the integers sit inside $R$ as a subgroup under the ordered-field operations, so $x \sim y$ iff $x - y \in Z$ is an equivalence relation on $R$ ; [F4] supplies only the abstract construction of $Z$ and not its copy in $R$ , so the embedding of [F5] is what makes the relation and the translations below meaningful. Take the quotient topology of [F3] on $R / Z$ .

givenF3F4F5

2.1

For an open interval $I$ of length below $1$ the translates $I + k$ , $k \in Z$ , are pairwise disjoint, since two points of $I$ differ by less than $1$ while distinct integer translates differ by at least $1$ in the order of [F5]; the preimage $q^{- 1} (q [I]) = ⋃_{k \in Z} (I + k)$ is then a union of open sets, so $q [I]$ is open and evenly covered. Openness of $I$ is required and not cosmetic: for $I = [0, \frac{1}{2}]$ the preimage $⋃_{k \in Z} [k, k + \frac{1}{2}]$ is not open, so $q [I]$ is not even a neighbourhood.

step 1.1F3F4F5

3.1

Verify directly that translations are deck transformations and that every deck transformation is the unique integer translation determined by the image of zero, without computing the fundamental group of the quotient.

step 2.1F2F3F1

4.1

The preceding construction and implications establish the assertion.

step 3.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 94 results over 20 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Allen Hatcher, Algebraic Topology, §1.3 (standard reference, not scraped)
Marco Gualtieri, MAT1300 Week 4 Term 2, §1.6 (standard reference, not scraped)
Omar Antolín Camarena, Proper local homeomorphisms and covering maps (standard reference, not scraped)

The quotient R→R/ZR→R/Z is a covering with integer translations as deck transformations