ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-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 square and hexagonal tori have j-invariants 1728 and 0

Example

For the square lattice $Λ_{i} = Z + Z i$ and the hexagonal lattice $Λ_{ω} = Z + Z ω$ , $ω = e^{2 π i / 3}$ : $j (Λ_{i}) = 1728, j (Λ_{ω}) = 0.$ Moreover $j (Λ) = 1728$ if and only if $Λ$ is homothetic to $Z [i]$ , and $j (Λ) = 0$ if and only if $Λ$ is homothetic to $Z [ω]$ . Multiplication by $i$ (respectively $ω$ ) induces an automorphism of the corresponding torus of order $4$ (respectively $3$ ).

Facts & Assumptions

Given: The lattices $Λ_{i} = Z + Z i$ and $Λ_{ω} = Z + Z ω$ with $ω = e^{2 π i / 3}$ , their tori $T_{Λ} = C / Λ$ and class maps $π_{Λ}$ (Complex lattice and quotient torus, The quotient $C / Λ$ is a compact Riemann surface); the modular function $j$ of The modular discriminant and the j-invariant; and the zeros of $E_{4}, E_{6}$ (The zeros of E4 and E6 at the elliptic points).

[F1]

For a full lattice $Λ$ with oriented basis $(ω_{1}, ω_{2})$ the value $j (Λ) : = j (ω_{2} / ω_{1})$ is independent of the choice of oriented basis; moreover $Λ^{'} = c Λ$ for some $c \in C^{\times}$ , biholomorphy of $T_{Λ}$ and $T_{Λ^{'}}$ , and $j (Λ^{'}) = j (Λ)$ are equivalent (The j-invariant classifies complex tori).

[F2]

$j (i) = 1728$ and $j (ω) = 0$ ; on $H$ the function $j$ is holomorphic and $P S L_{2} (Z)$ -invariant, and $j (τ) = j (τ^{'})$ only when $τ, τ^{'}$ lie in one $P S L_{2} (Z)$ -class (The modular discriminant and the j-invariant, The j-invariant uniformizes X(1), The zeros of E4 and E6 at the elliptic points).

[F3]

The class map $π_{Λ} : C \to T_{Λ}$ is a holomorphic covering; for $a \in C^{\times}$ with $a Λ \subseteq Λ$ the formula $m_{a} ([z]) : = [a z]$ is well defined on $T_{Λ}$ because $z - w \in Λ$ implies $a (z - w) \in Λ$ , and $m_{a}$ is holomorphic since $π_{Λ} \circ (a \cdot) = m_{a} \circ π_{Λ}$ ; when $a Λ = Λ$ it is a biholomorphism with inverse $m_{a^{- 1}}$ (The quotient $C / Λ$ is a compact Riemann surface, Complex lattice and quotient torus).

Verification

1.1F1F2givenalgebra

Oriented bases. The pair $(1, i)$ is an oriented basis of $Λ_{i} = Z + Z i$ : $i \notin R$ and $Im (i / 1) = 1 > 0$ . Hence $Λ_{i}$ has parameter $τ = i$ and, by [F1] and the first value in [F2], $j (Λ_{i}) = j (i) = 1728$ . Likewise $(1, ω)$ is an oriented basis of $Λ_{ω} = Z + Z ω$ , since $Im ω = \sin (2 π / 3) = \sqrt{3} / 2 > 0$ , so $Λ_{ω}$ has parameter $ω$ and $j (Λ_{ω}) = j (ω) = 0$ by [F2].

2.1F1F2step 1.1givenalgebra

The level sets of $1728$ and $0$ . Let $Λ$ be a full lattice. By [F1], $j (Λ) = j (Λ_{i})$ holds if and only if $Λ$ is homothetic to $Λ_{i}$ , and by 1.1 the value on the right is $j (Λ_{i}) = 1728$ ; hence $j (Λ) = 1728$ if and only if $Λ$ is homothetic to $Z [i] = Λ_{i}$ . The same argument with $Λ_{ω}$ gives: by [F1] and 1.1, $j (Λ) = j (Λ_{ω}) = 0$ if and only if $Λ$ is homothetic to $Λ_{ω} = Z [ω]$ . Equivalently, both statements say that the level set of each of the two special values is a single homothety class, as also follows from the injectivity of $j$ on $P S L_{2} (Z)$ -classes recorded in [F2].

3.1F3givenalgebra∎

Automorphisms of order $4$ and $3$ . Multiplication by $i$ preserves $Λ_{i}$ : $i (m + n i) = - n + m i$ with $- n, m \in Z$ ; hence $i Λ_{i} = Λ_{i}$ (equality, since $i$ is invertible and $i Λ_{i} \subseteq Λ_{i}$ with the same argument applied to $- i$ ), and [F3] provides the biholomorphic automorphism $m_{i} ([z]) = [i z]$ of $T_{Λ_{i}}$ . Its fourth power is the identity, $m_{i}^{4} = m_{i^{4}} = m_{1} = id$ , while $m_{i}^{2} = m_{- 1}$ is not the identity because $[1 / 3] \neq [- 1 / 3]$ : their difference would require $2 / 3 \in Λ_{i}$ , and no element $m + n i$ of $Λ_{i}$ with $n = 0$ equals $2 / 3 \notin Z$ ; so the order of $m_{i}$ divides $4$ but not $2$ , hence is exactly $4$ . Similarly $ω Λ_{ω} \subseteq Λ_{ω}$ because $ω \cdot 1 = ω$ and $ω \cdot ω = ω^{2} = - 1 - ω$ lie in $Λ_{ω}$ , and $ω Λ_{ω} = Λ_{ω}$ by the same inverse argument with $ω^{- 1} = ω^{2}$ ; so [F3] gives the automorphism $m_{ω} ([z]) = [ω z]$ . Its cube is $m_{ω}^{3} = m_{ω^{3}} = m_{1} = id$ since $ω^{3} = 1$ , and $m_{ω}$ is not the identity because $[ω / 2] \neq [1 / 2]$ : $(ω - 1) / 2 = - \frac{1}{2} + \frac{1}{2} ω$ is not of the form $m + n ω$ with $m, n \in Z$ ; so the order of $m_{ω}$ divides $3$ but is not $1$ , hence is exactly $3$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

70 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

C. T. McMullen, Advanced Complex Analysis, Math 213a course notes (Harvard, 2010) (standard reference, not scraped)
J. S. Milne, Modular Functions and Modular Forms (v1.31, 2017) (standard reference, not scraped)
D. Zagier, Elliptic Modular Forms and Their Applications, in The 1-2-3 of Modular Forms (Universitext, Springer, 2008) (standard reference, not scraped)