ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 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.

Half-period values of the square lattice

Example

Let $Λ_{s q} = Z + i Z$ be the square lattice with its oriented basis $(1, i)$ , let $℘ = ℘_{Λ_{s q}}$ with invariants $g_{2}, g_{3}$ , put $h : = (1 + i) / 2$ , and let $e_{1} : = ℘ (1 / 2)$ , $e_{2} : = ℘ (i / 2)$ , $e_{3} : = ℘ (h)$ be the three half-period values. Then:

$℘ (h) = 0$ , so $e_{3} = 0$ ;
the other two half-period values $e_{1}$ and $e_{2}$ are the two elements of the pair $\pm \sqrt{g_{2}} / 2$ of roots of $4 x^{3} - g_{2} x$ ; with the normalisation $\sqrt{g_{2}} : = 2 e_{1}$ one has $e_{1} = \sqrt{g_{2}} / 2$ and $e_{2} = - \sqrt{g_{2}} / 2$ literally, and $g_{2} \neq 0$ ;
the four branch values of the torus form $\overset{ˉ}{℘} : T_{Λ_{s q}} \to \hat{C}$ of $℘$ — the images of its critical points (Ramification index, ramification order and branch value) — are exactly $0$ , $\pm \sqrt{g_{2}} / 2$ and $\infty$ .

The verification below evaluates no Eisenstein sum: it uses the scaling identity $℘_{c Λ} (c z) = c^{- 2} ℘_{Λ} (z)$ at $c = i$ , the symmetry $i Λ_{s q} = Λ_{s q}$ , and the cubic differential equation.

Facts & Assumptions

Given: The square lattice $Λ_{s q} = Z + i Z$ with its basis $(1, i)$ , the Weierstrass function $℘ = ℘_{Λ_{s q}}$ and its derivative $℘^{'}$ , the invariants $g_{2} = 60 G_{4}$ , $g_{3} = 140 G_{6}$ , the torus $T_{Λ_{s q}} = C / Λ_{s q}$ with class map $π$ , the torus form $\overset{ˉ}{℘}$ characterised by $\overset{ˉ}{℘} \circ π = ℘$ , the half-periods $h_{1} = 1 / 2$ , $h_{2} = i / 2$ , $h_{3} = (1 + i) / 2 = h$ and the values $e_{j} = ℘ (h_{j})$ .

[F1]

$C$ is a field; every complex number has a unique form $a + b i$ with $a, b \in R$ ; and $(a + b i) (u + v i) = (a u - b v) + (a v + b u) i$ for real $a, b, u, v$ ( $C = R [x] / (x^{2} + 1)$ is a field, every element is uniquely $a + b i$ , and every nonzero element has inverse $(a - b i) / (a^{2} + b^{2})$ ).

[F2]

A full complex lattice is a subgroup $Λ = Z ω_{1} + Z ω_{2} \subseteq C$ with $ω_{1}, ω_{2}$ real-linearly independent, and $(ω_{1}, ω_{2})$ is oriented when $Im (ω_{2} / ω_{1}) > 0$ ; for either ordering, real-linear independence is equivalent to $Im (ω_{2} / ω_{1}) \neq 0$ (Complex lattice and quotient torus).

[F3]

$℘_{Λ} (z) = z^{- 2} + \sum_{ω \in Λ ∖ {0}} ((z - ω)^{- 2} - ω^{- 2})$ on $C ∖ Λ$ , the sum being the unordered finite-subset sum over the directed set of finite subsets of $Λ ∖ {0}$ ; the value depends only on the lattice (Weierstrass p function).

[F4]

For every full lattice the sum defining $℘_{Λ}$ converges absolutely at every $z \in C ∖ Λ$ and uniformly on compact subsets; $℘_{Λ}$ is holomorphic on $C ∖ Λ$ and $Λ$ -periodic, $℘_{Λ} (z + λ) = ℘_{Λ} (z)$ for every $λ \in Λ$ and every $z \in C$ with poles matched (Normal convergence, parity and periodicity of the Weierstrass p function).

[F5]

With the invariants $g_{2} = 60 G_{4}$ and $g_{3} = 140 G_{6}$ one has $(℘^{'})^{2} = 4 ℘^{3} - g_{2} ℘ - g_{3}$ on $C ∖ Λ$ (Weierstrass cubic differential equation).

[F6]

For the square lattice $g_{3} (Λ_{s q}) = 0$ and $g_{2} (Λ_{s q}) \neq 0$ (Square and hexagonal lattice invariants).

[F7]

For a full lattice $Λ = Z ω_{1} + Z ω_{2}$ with $h_{1} = ω_{1} / 2$ , $h_{2} = ω_{2} / 2$ , $h_{3} = (ω_{1} + ω_{2}) / 2$ one has $℘^{'} (h) = 0$ for every $h \in C ∖ Λ$ with $2 h \in Λ$ , and the zeros of $℘^{'}$ are precisely the $Λ$ -translates of $h_{1}, h_{2}, h_{3}$ , each of order one (Degree two of ℘ and its four branch points).

[F8]

For the same data the classes $[h_{1}], [h_{2}], [h_{3}]$ are three distinct nonzero half-period classes, the values $e_{1}, e_{2}, e_{3}$ are three distinct complex numbers, and the torus form $\overset{ˉ}{℘} : T_{Λ} \to \hat{C}$ of $℘$ has critical points exactly $[0], [h_{1}], [h_{2}], [h_{3}]$ , with branch values $\overset{ˉ}{℘} ([0]) = \infty$ and $e_{1}, e_{2}, e_{3}$ (Degree two of ℘ and its four branch points).

[F9]

For a nonconstant holomorphic map $f : X \to Y$ of Riemann surfaces, a branch value of $f$ is a point $y \in Y$ for which there is a critical point $x \in X$ with $f (x) = y$ , and the set of all branch values is the branch locus of $f$ (Ramification index, ramification order and branch value).

Verification

1.1F1F2F8givenalgebra

(The square lattice, its symmetry and its half-periods.) Since every complex number is uniquely $a + b i$ with $a, b \in R$ , the pair ${1, i}$ spans $C$ over $R$ and $a + b i = 0$ forces $a = b = 0$ , so $1, i$ are real-linearly independent and $Λ_{s q} = Z + i Z$ is a full complex lattice with oriented basis $(1, i)$ , as $Im (i / 1) = 1 > 0$ ; multiplication by $i$ maps $Λ_{s q}$ into itself because $i \cdot 1 = i$ and $i \cdot i = - 1$ both lie in it, and multiplication by $i$ is a bijection of $C$ with inverse multiplication by $i^{- 1} = - i$ (as $i \cdot (- i) = 1$ ), which also preserves $Λ_{s q}$ , so $i Λ_{s q} = Λ_{s q}$ ; with the oriented basis $(1, i)$ the half-periods of the degree-two lemma are $h_{1} = 1 / 2$ , $h_{2} = i / 2$ , $h_{3} = (1 + i) / 2 = h$ , and these are nonzero classes, so $h \notin Λ_{s q}$ ; moreover $2 h_{1} = 1$ , $2 h_{2} = i$ and $2 h_{3} = 1 + i$ lie in $Λ_{s q}$ , and $h - i h = \frac{1}{2} (1 + i) (1 - i) = \frac{1}{2} (1 - i^{2}) = 1$ .

1.2F1F2F3F4algebra

(The scaling identity for the $℘$ -series.) Let $Λ = Z ω_{1} + Z ω_{2}$ be a full lattice, $c \in C^{\times}$ and $z \in C ∖ Λ$ ; then $c Λ = Z (c ω_{1}) + Z (c ω_{2})$ is again a full lattice, because $a (c ω_{1}) + b (c ω_{2}) = c (a ω_{1} + b ω_{2})$ vanishes for real $a, b$ only if $a ω_{1} + b ω_{2} = 0$ , and $ω \mapsto c ω$ is a bijection $Λ \to c Λ$ ; for every finite $F \subseteq Λ ∖ {0}$ one has $\sum_{ω \in F} ((c z - c ω)^{- 2} - (c ω)^{- 2}) = c^{- 2} \sum_{ω \in F} ((z - ω)^{- 2} - ω^{- 2})$ by the multiplication formula and $(c ζ)^{- 2} = c^{- 2} ζ^{- 2}$ ; the finite subsets of $c Λ ∖ {0}$ are exactly the image sets $c F$ , so the finite-subset net defining $℘_{c Λ} (c z)$ is the constant $(c z)^{- 2} = c^{- 2} z^{- 2}$ plus $c^{- 2}$ times the finite-subset net defining $℘_{Λ} (z)$ , which converges at $z \notin Λ$ by the absolute-convergence clause; hence $℘_{c Λ} (c z) = c^{- 2} ℘_{Λ} (z)$ .

2.1step 1.1step 1.2algebra

(The scaling identity at $c = i$ .) Taking $c = i$ and $Λ = Λ_{s q}$ in step 1.2, and using $i Λ_{s q} = Λ_{s q}$ from step 1.1 as well as $i^{- 2} = (i^{2})^{- 1} = (- 1)^{- 1} = - 1$ , gives $℘ (i z) = - ℘ (z)$ for every $z \in C ∖ Λ_{s q}$ .

2.2F5F6F7givenalgebra

(The cubic relation at each half-period.) Fix $j \in {1, 2, 3}$ : by step 1.1, $h_{j} \notin Λ_{s q}$ and $2 h_{j} \in Λ_{s q}$ , so the degree-two lemma gives $℘^{'} (h_{j}) = 0$ ; since $h_{j} \in C ∖ Λ_{s q}$ , the differential equation may be evaluated there, giving $0 = (℘^{'} (h_{j}))^{2} = 4 ℘ (h_{j})^{3} - g_{2} ℘ (h_{j}) - g_{3} = 4 e_{j}^{3} - g_{2} e_{j} - g_{3}$ , and with $g_{3} = 0$ for the square lattice this reads $e_{j} (4 e_{j}^{2} - g_{2}) = 0$ .

3.1F1F4step 1.1step 2.1algebra

(The vanishing $℘ (h) = 0$ .) By step 1.1, $h \notin Λ_{s q}$ and $h = i h + 1$ with $1 \in Λ_{s q}$ ; hence $h$ lies in the domain of $℘$ and the periodicity and step 2.1 give $℘ (h) = ℘ (i h + 1) = ℘ (i h) = - ℘ (h)$ , so $2 ℘ (h) = 0$ , and since $C$ is a field in which $2 \neq 0$ this forces $℘ (h) = 0$ ; thus $e_{3} = ℘ (h_{3}) = ℘ (h) = 0$ .

4.1F1F6F8step 3.1step 2.2algebra

(The two nonzero half-period values and the factorisation of the cubic.) By step 3.1, $e_{3} = 0$ , and by the degree-two lemma $e_{1}, e_{2}, e_{3}$ are pairwise distinct, so $e_{1}, e_{2} \neq 0$ ; step 2.2 for $j = 1, 2$ then gives $e_{j} (4 e_{j}^{2} - g_{2}) = 0$ with $e_{j} \neq 0$ , hence $4 e_{1}^{2} = g_{2} = 4 e_{2}^{2}$ and $e_{1}^{2} = e_{2}^{2}$ , that is $(e_{1} - e_{2}) (e_{1} + e_{2}) = 0$ in the field $C$ , so $e_{1} - e_{2} \neq 0$ forces $e_{1} + e_{2} = 0$ and $e_{2} = - e_{1}$ ; consequently $g_{2} = 4 e_{1}^{2} \neq 0$ , and substituting $g_{2} = 4 e_{1}^{2}$ and $g_{3} = 0$ gives the polynomial identity $4 x^{3} - g_{2} x - g_{3} = 4 x^{3} - 4 e_{1}^{2} x = 4 x (x - e_{1}) (x + e_{1})$ , so the cubic $4 x^{3} - g_{2} x - g_{3}$ has exactly the roots $0, e_{1}, - e_{1}$ , which are pairwise distinct; with the normalisation $\sqrt{g_{2}} : = 2 e_{1}$ one has $(\sqrt{g_{2}})^{2} = 4 e_{1}^{2} = g_{2}$ and $\pm \sqrt{g_{2}} / 2 = \pm e_{1}$ , so the other two half-period values $e_{1} = ℘ (1 / 2)$ and $e_{2} = ℘ (i / 2) = - e_{1}$ are exactly the two distinct roots $\pm \sqrt{g_{2}} / 2$ of $4 x^{3} - g_{2} x$ .

5.1F8F9step 4.1algebra

(The four branch values.) By the degree-two lemma the torus form $\overset{ˉ}{℘}$ of $℘$ has critical points exactly $[0], [h_{1}], [h_{2}], [h_{3}]$ , with branch values $\overset{ˉ}{℘} ([0]) = \infty$ and $e_{1}, e_{2}, e_{3}$ , so by the definition of a branch value its branch locus is the four-element set ${\infty, e_{1}, e_{2}, e_{3}}$ ; by step 4.1 this set is ${\infty, 0, e_{1}, - e_{1}} = {\infty, 0, \pm \sqrt{g_{2}} / 2}$ with $e_{1} \neq 0$ , so the branch locus of $\overset{ˉ}{℘}$ consists exactly of the four distinct values $\infty, 0, \sqrt{g_{2}} / 2, - \sqrt{g_{2}} / 2$ .

6.1step 3.1step 4.1step 5.1

(Assembly.) Step 3.1 proves $℘ (h) = 0$ for $h = (1 + i) / 2$ , so the half-period value $e_{3}$ is $0$ ; step 4.1 proves that $e_{1}$ and $e_{2}$ are the two distinct roots $\pm \sqrt{g_{2}} / 2$ of $4 x^{3} - g_{2} x$ for the normalisation $\sqrt{g_{2}} = 2 e_{1}$ , and that $g_{2} \neq 0$ ; step 5.1 proves that the branch values of the torus form of $℘$ are exactly $0, \pm \sqrt{g_{2}} / 2, \infty$ . These are the three assertions of the example. ∎

Remarks

The sign in $℘ (h) = 0$ comes from the scaling identity alone: $i$ is a similarity of the square lattice, and under it $℘$ is multiplied by $i^{- 2} = - 1$ , while $h$ and $i h$ differ by the period $1$ . The remaining half-period values are then forced by the cubic: everything is a root of $4 x^{3} - g_{2} x$ because $g_{3} = 0$ , and the two nonzero roots sum to zero, matching $e_{2} = - e_{1}$ . The four branch values of the degree-two map $\overset{ˉ}{℘} : T_{Λ_{s q}} \to \hat{C}$ are consequently $\infty$ and the three finite values $0, \pm \sqrt{g_{2}} / 2$ — the two-element pair beyond $0$ being exactly the pair of nonzero roots, without any need to evaluate $g_{2}$ numerically.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

62 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)
NIST Digital Library of Mathematical Functions, §23.2 and §23.3 (standard reference, not scraped)