ExampleConstruction: Literature-sourcedVerification: AI-adaptedverified 2026-09-26 (gpt-6-sol)

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 maps $[x] \mapsto [m x]$ on $R / Z$ are $m$ -sheeted coverings for $m \geq 1$

Example

For every integer $m \geq 1$ , the map $P_{m} : R / Z \to R / Z$ given by $P_{m} ([x]) = [m x]$ is a well-defined $m$ -sheeted covering.

Facts & Assumptions

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

[F1]

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

[F2]

A covering map is a continuous surjection $p : E \to B$ such that every $b \in B$ has an open neighbourhood $U$ for which $p^{- 1} (U)$ is a disjoint union of open sets $V_{j}$ , called sheets, and each restriction $p ∣_{V_{j}} : V_{j} \to U$ is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a $U$ is evenly covered, and $p^{- 1} (b)$ is the fibre over $b$ . A covering is trivial when it is isomorphic over $B$ to a product projection $B \times F \to B$ with $F$ discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).

[F3]

For a covering $p : E \to B$ , the cardinality of $p^{- 1} (b)$ is locally constant as a function of $b \in B$ . If $B$ is connected, all fibres are equinumerous. (The cardinality of a covering fibre is locally constant and is constant on a connected base).

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

Let $a, b \in Z$ with $b > 0$ . Then there exist integers $q$ and $r$ with $a = q b + r$ and $0 \leq r < b$ , and this pair is unique (Division with remainder in $Z$ : for $a \in Z$ and $b > 0$ there are unique $q, r \in Z$ with $a = q b + r$ and $0 \leq r < b$ ).

Verification

technique · direct

1.1givenF1

If $[x] = [x + n]$ with $n \in Z$ , then $[m (x + n)] = [m x]$ , so $P_{m}$ is well defined. Since $P_{m} \circ q = q \circ (x \mapsto m x)$ and $q$ is a quotient map, $P_{m}$ is continuous. It is surjective because $P_{m} ([y / m]) = [y]$ .

2.1F1F2F5step 1.1

Fix $[a]$ and choose $I = (a - δ, a + δ)$ with $0 < δ < 1 / 2$ . The quotient map $q$ is open, since $q^{- 1} (q (O)) = ⋃_{n \in Z} (O + n)$ is open for every open $O \subseteq R$ . Thus $U = q (I)$ is open, and $q ∣_{I}$ is a homeomorphism onto $U$ . For $0 \leq r < m$ , put $V_{r} = q ((I + r) / m)$ . Each $V_{r}$ is open, and $P_{m} ∣_{V_{r}}$ is a homeomorphism onto $U$ , with inverse $q (u) \mapsto q ((u + r) / m)$ for $u \in I$ . If points from $V_{r}$ and $V_{s}$ coincide, then $u - v + r - s$ is a multiple of $m$ for some $u, v \in I$ . Since $∣ u - v ∣ < 1$ and $r - s$ is an integer between $- (m - 1)$ and $m - 1$ , this forces $r = s$ and $u = v$ . Finally, if $P_{m} ([x]) \in U$ , then $m x = u + n$ for some $u \in I$ and $n \in Z$ ; write $n = k m + r$ with $0 \leq r < m$ by [F5], giving $[x] \in V_{r}$ . Hence $P_{m}^{- 1} (U)$ is the disjoint union of exactly $m$ sheets.

3.1step 2.1

At $m = 1$ the map is the identity, so no zero-sheet or division-by-zero case is hidden.

4.1step 3.1∎

The preceding construction and implications establish the assertion.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

27 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, §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 maps [x]↦[mx][x]↦[mx] on R/ZR/Z are mm-sheeted coverings for m≥1m≥1