ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-02

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.

Oriented bases and ${S L}_{2} (Z)$

Example

Let $Λ = Z + i Z = {m + n i : m, n \in Z}$ .

The pairs $(1, i)$ and $(1 + i, i)$ are bases of $Λ$ of positive complex orientation and differ by an integer change-of-basis matrix of determinant $1$ ;
the pair $(i, 1)$ is a basis of $Λ$ of negative orientation, and it differs from $(1, i)$ by an integer matrix of determinant $- 1$ ;
all three pairs are bases of the same lattice, so they all define the same complex torus $C / Λ$ and the same compact Riemann surface.

Facts & Assumptions

Given: The lattice $Λ = Z + i Z$ , whose elements are the numbers $m + n i$ with $m, n \in Z$ and whose real-linear independence datum is $i / 1 = i \notin R$ .

[F1]

A basis of a lattice $Λ$ is a pair $(ω_{1}, ω_{2})$ with $Λ = Z ω_{1} + Z ω_{2}$ and $ω_{1}, ω_{2}$ real-linearly independent; it is oriented when $Im (ω_{2} / ω_{1}) > 0$ ; two bases of the same lattice differ by a matrix in ${G L}_{2} (Z)$ , and two oriented bases by a matrix in ${S L}_{2} (Z)$ ; the quotient torus and all its structure depend on the set $Λ$ alone (Complex lattice and quotient torus).

[F2]

For a full lattice $Λ$ the quotient $T_{Λ} = C / Λ$ is a compact Riemann surface with the quotient topology of the class map $π$ , which is a holomorphic covering map (The quotient $C / Λ$ is a compact Riemann surface).

Verification

1.1F1

The pair $(1, i)$ is a basis of $Λ$ : by definition $Λ = Z \cdot 1 + Z \cdot i$ , and $1, i$ are real-linearly independent since $i \notin R$ ; its orientation is positive because $Im (i / 1) = 1 > 0$ .

1.2F1algebra

The pair $(1 + i, i)$ is a basis of the same lattice: $1 + i, i \in Λ$ , so $Z (1 + i) + Z i \subseteq Λ$ , while $1 = (1 + i) - i$ and $i = i$ show the reverse inclusion; the change-of-basis matrix, whose columns are the new vectors in the old basis, expressing $(1 + i, i) = (ω_{1} + ω_{2}, ω_{2})$ in the basis $(1, i)$ is $(\begin{matrix} 1 & 0 \\ 1 & 1 \end{matrix})$ , of determinant $1$ , so the orientation is positive as well, and independently $Im (i / (1 + i)) = Im ((1 + i) / 2) = \frac{1}{2} > 0$ .

1.3F1algebra

The pair $(i, 1)$ is a basis of $Λ$ with change-of-basis matrix $(\begin{matrix} 0 & 1 \\ 1 & 0 \end{matrix})$ relative to $(1, i)$ , of determinant $- 1$ ; its orientation is negative because $Im (1 / i) = Im (- i) = - 1 < 0$ .

2.1F1F2step 1.1step 1.2step 1.3∎

By steps 1.1, 1.2 and 1.3 the three pairs are bases of the same lattice $Λ$ , so they give the same quotient $C / Λ$ and the same lattice sums, and by [F2] this quotient is a compact Riemann surface with holomorphic covering map $π$ , independently of which basis is used to describe $Λ$ .

The example illustrates that orientation is a property of an ordered basis, not of the lattice: $(1, i)$ and $(1 + i, i)$ are related by the unipotent matrix $(\begin{matrix} 1 & 0 \\ 1 & 1 \end{matrix}) \in {S L}_{2} (Z)$ , whereas swapping the two vectors multiplies the orientation sign by $- 1$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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

J. S. Milne, Modular Functions and Modular Forms, Ch. 3, pp. 41-47 (standard reference, not scraped)
C. T. McMullen, Advanced Complex Analysis, Math 213a course notes, Ch. 5 §5.1, pp. 79-90 (standard reference, not scraped)

Oriented bases and SL2(Z)SL2​(Z)