ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-30

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.

Torus commutator polygon

Example

The square schema of Polygonal schemas and paired boundary edges with boundary word $a b a^{- 1} b^{- 1}$ realizes the torus $T^{2} = (R / Z)^{2}$ of The two-dimensional torus $T^{2} = (R / Z)^{2}$ . It is orientable and has $V = 1$ , $E = 2$ , $F = 1$ , hence $χ (T^{2}) = 1 - 2 + 1 = 0$ (Euler characteristic of a finite CW complex). This direct finite quotient uses no choice axiom.

Facts & Assumptions

Given: The square $Q = [0, 1]^{2}$ with sides paired by $(s, 0) \sim (s, 1)$ and $(0, t) \sim (1, t)$ , the one-polygon schema whose boundary word is $a b a^{- 1} b^{- 1}$ , and the quotient circle $S^{1} = R / Z$ with projection $p$ .

[L1]

A polygonal schema is finite data of oriented nondegenerate closed disks with sides paired by specified homeomorphisms, and its realization is the quotient; a connected surface schema has each edge class incident with exactly two face-sides and a single cyclic link at each vertex class; its realization is a nonempty compact connected boundaryless surface whose finite CW cells are the vertex classes, the edge pairs and the face disks; in a one-polygon word a pair with opposite exponents is orientation compatible and a pair with equal exponents is twisted (Polygonal schemas and paired boundary edges).

[L2]

The realization carries the quotient topology, for which a map out of the quotient is continuous exactly when its composite with the quotient map is continuous (The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection, Characteristic properties: a map into a space with the initial topology is continuous iff every composite with the defining family is, a map out of a space with the final topology is continuous iff every composite with the defining family is, and the two topologies are respectively the coarsest and the finest making that family continuous).

[L3]

The circle is $S^{1} = R / Z$ , where $p (x) = p (y)$ exactly when $x - y \in Z$ ; it is compact, path connected and Hausdorff (The circle as $S^{1} = R / Z$ with basepoint $[0]$ , $R / Z$ is compact and path-connected, $R / Z$ is Hausdorff).

[L4]

The torus is $T^{2} = S^{1} \times S^{1}$ with the product topology (The two-dimensional torus $T^{2} = (R / Z)^{2}$ ), products of Hausdorff spaces are Hausdorff (Arbitrary products preserve $T_{0}$ , $T_{1}$ , and Hausdorffness), and a map into a product is continuous exactly when its components are (The product set $\prod_{i \in I} X_{i}$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, A map into a product is continuous iff each of its components is; the projections are continuous and open; and each projection is surjective when every factor is nonempty, which for an infinite index set uses the Axiom of Choice).

[L5]

A continuous bijection from a compact space onto a Hausdorff space is a homeomorphism (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism).

[L6]

The Euler characteristic of a space with finitely many cells is $χ (X) = \sum_{n} (- 1)^{n} c_{n} (X)$ (Euler characteristic of a finite CW complex).

[L7]

An integral orientation is a continuous section of the local homology system whose value generates every fiber; the system is trivialized over coordinate balls, where a continuous generator section is locally constant, so a generator prescribed on the face continues across an edge exactly when the pairing is orientation compatible (R-orientation of a topological manifold, Orientation local system and orientation cover).

Verification

technique · direct

1.1L1

The bottom and top sides of $Q$ form one paired class and the left and right sides form a second; the four corners are all identified, since the horizontal pairing gives $(0, 0) \sim (0, 1)$ and $(1, 0) \sim (1, 1)$ while the vertical pairing gives $(0, 0) \sim (1, 0)$ and $(0, 1) \sim (1, 1)$ , so the four corner sectors join in the single cyclic link $(0, 0)$ – $(1, 0)$ – $(1, 1)$ – $(0, 1)$ – $(0, 0)$ . The square schema is therefore a connected surface schema with $V = 1$ , $E = 2$ , $F = 1$ , and its realization $Y$ is a nonempty compact connected boundaryless surface.

1.2givenL2L3L4

The map $f : Q \to T^{2}$ , $f (s, t) = (p (s), p (t))$ , is continuous because its two components $p \circ {p r}_{1}$ and $p \circ {p r}_{2}$ are continuous, and $f (s, t) = f (s^{'}, t^{'})$ holds exactly when $s - s^{'} \in Z$ and $t - t^{'} \in Z$ ; for $s, s^{'} \in [0, 1]$ this means $s = s^{'}$ or ${s, s^{'}} = {0, 1}$ , and likewise in the second coordinate, so the fibres of $f$ are precisely the classes of the relation on $Q$ generated by the two side pairings. Since $f$ is constant on those classes, it induces a continuous bijection $\overset{ˉ}{f} : Y \to T^{2}$ out of the quotient.

2.1L1L4L5step 1.2

The realization $Y$ is compact by [L1] and $T^{2}$ is Hausdorff by [L4], so the continuous bijection $\overset{ˉ}{f}$ is a homeomorphism by [L5]; hence the word $a b a^{- 1} b^{- 1}$ realizes the torus $T^{2}$ .

3.1L1L6step 1.1step 2.1

The cell counts of step 1.1 give $χ (Y) = V - E + F = 1 - 2 + 1 = 0$ by [L6], and this is the Euler characteristic of $T^{2}$ by step 2.1.

4.1L1L7step 1.1step 2.1∎

Each of the two letters occurs once with exponent $+ 1$ and once with exponent $- 1$ , so by [L1] both pairings are orientation compatible; the generator carried by the oriented face continues unchanged across both edge classes, and its locally constant generator classes supply the continuous generating section of [L7]. Hence $Y ≅ T^{2}$ is orientable. Every ingredient is a finite explicit map or pairing, so no choice axiom is used.

Remarks

The word $a b a^{- 1} b^{- 1}$ is the genus-one case $g = 1$ of the commutator word $\prod_{i = 1}^{g} a_{i} b_{i} a_{i}^{- 1} b_{i}^{- 1}$ , and the computation here is the $g = 1$ instance of the cell count used later on the A page.

Depends on

Used by

Equal Euler characteristic without homeomorphism Counterexample
Genus-two orientable polygon Example
Classification of compact connected surfaces Theorem

Dependency tree · two levels

58 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

Gallier and Xu, A Guide to the Classification Theorem for Compact Surfaces (standard reference, not scraped)
Koch, Classification of Surfaces (standard reference, not scraped)