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 elliptic points of the modular group and their images under j

Example

In $P S L_{2} (Z) \ H$ there are exactly two elliptic classes: the class of $i$ , with stabiliser of order $2$ generated by $S$ , and the class of $ω = e^{2 π i / 3}$ , with stabiliser of order $3$ generated by $S T$ ; every other stabiliser is trivial. The corresponding orbifold points have orders $2$ and $3$ ; the quotient map $H \to X (1)$ has local degrees $2$ at $i$ and $3$ at $ω$ , and $j (i) = 1728$ , $j (ω) = 0$ .

Facts & Assumptions

Given: The action of $G = P S L_{2} (Z)$ on $H$ with $S \cdot z = - 1 / z$ , $T \cdot z = z + 1$ and the closure $\overline{D} = {τ : ∣ ℜ τ ∣ \leq 1 / 2, ∣ τ ∣ \geq 1}$ of the standard fundamental domain (The standard fundamental domain, boundary identifications and elliptic stabilisers); the quotient map $π : H \to Y (1) \subset X (1)$ with its local charts at the elliptic points, where it is $z \mapsto z^{ν}$ in a centred coordinate (Local charts and the Riemann surface structure of a modular quotient, The j-invariant uniformizes X(1)); the modular function $j = E_{4}^{3} / Δ$ with $Δ = (E_{4}^{3} - E_{6}^{2}) / 1728$ nonvanishing on $H$ (The modular discriminant and the j-invariant).

[F1]

Every $G$ -orbit meets $\overline{D}$ ; the only points of $\overline{D}$ with nontrivial $G$ -stabiliser are $i$ , $ω$ and $ω + 1$ , with $Stab (i) = ⟨ S ⟩$ of order $2$ , $Stab (ω) = ⟨ S T ⟩$ of order $3$ and $Stab (ω + 1) = ⟨ T S ⟩$ of order $3$ , while every other point of $\overline{D}$ has trivial stabiliser; $T \cdot ω = ω + 1$ (The standard fundamental domain, boundary identifications and elliptic stabilisers, Local charts and the Riemann surface structure of a modular quotient).

[F2]

In the quotient chart at an elliptic point a generator of the stabiliser acts by $z \mapsto e^{2 π i / ν} z$ and $π$ becomes the map $z \mapsto z^{ν}$ ; for $G$ this is $ν = 2$ at $i$ and $ν = 3$ at $ω$ and $ω + 1$ , so $π$ has local degree $2$ at $i$ and $3$ at $ω$ and $ω + 1$ , representatives of the two elliptic classes; the same local degrees hold at all their modular translates (Local charts and the Riemann surface structure of a modular quotient, The j-invariant uniformizes X(1)).

[F3]

$E_{4}$ has a simple zero at the class of $ω$ and no other zeros, and $E_{6}$ has a simple zero at the class of $i$ and no other zeros; in particular $E_{6} (i) = 0$ , $E_{4} (i) \neq 0$ , $E_{4} (ω) = 0$ and $E_{6} (ω) \neq 0$ (The zeros of E4 and E6 at the elliptic points).

[F4]

$Δ = (E_{4}^{3} - E_{6}^{2}) / 1728$ has no zeros on $H$ and $j = E_{4}^{3} / Δ$ is a holomorphic $G$ -invariant function with $j (i) = 1728$ and $j (ω) = 0$ (The modular discriminant and the j-invariant).

Verification

1.1F1givenalgebra

Exactly two elliptic classes. Let $τ \in H$ have nontrivial stabiliser in $G$ . By [F1] there is $γ \in G$ with $γ \cdot τ \in \overline{D}$ , and $Stab (γ \cdot τ) = γ Stab (τ) γ^{- 1}$ is then nontrivial, so $γ \cdot τ \in {i, ω, ω + 1}$ by [F1]. Since $T \cdot ω = ω + 1$ , every point with nontrivial stabiliser is $G$ -equivalent to $i$ or to $ω$ . The classes of $i$ and $ω$ are distinct: if $ω = γ \cdot i$ , then conjugation would give $Stab (ω) = γ Stab (i) γ^{- 1}$ , a group of order $2$ , whereas $Stab (ω) = ⟨ S T ⟩$ has order $3$ by [F1]. So there are exactly two elliptic classes, the classes of $i$ and $ω$ , and their stabilisers are of orders $2$ and $3$ generated by $S$ and $S T$ ; every point outside these two classes has trivial stabiliser, since a point with nontrivial stabiliser is equivalent to $i$ or $ω$ and all other points of $\overline{D}$ have trivial stabiliser [F1].

2.1F2step 1.1givenalgebra

By [F2], the quotient map has local degree $2$ at $i$ and $3$ at $ω$ and $ω + 1$ . For every $γ \in G$ , $π \circ γ = π$ and $γ$ is a biholomorphism, so the local degree is unchanged at $γ i$ or $γ ω$ . Thus its ramification locus is exactly $G \cdot i \cup G \cdot ω$ , with local degrees $2$ and $3$ respectively; outside these orbits the stabiliser is trivial by 1.1 and the quotient chart is a local inverse of $π$ , giving degree $1$ .

3.1F3F4givenalgebra∎

Special values. At $τ = i$ , [F3] gives $E_{6} (i) = 0$ and $E_{4} (i) \neq 0$ , so $Δ (i) = (E_{4} (i)^{3} - 0) / 1728 = E_{4} (i)^{3} / 1728 \neq 0$ and $j (i) = E_{4} (i)^{3} / Δ (i) = 1728$ . At $τ = ω$ , [F3] gives $E_{4} (ω) = 0$ , so $j (ω) = 0 / Δ (ω) = 0$ , the denominator being nonzero by [F4]; the same two values are recorded in [F4].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

42 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 (v1.31, 2017) (standard reference, not scraped)
C. T. McMullen, Advanced Complex Analysis, Math 213a course notes (Harvard, 2010) (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)