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.

Square and hexagonal lattice invariants

Example

For the square lattice $Λ_{s q} = Z + i Z$ one has $g_{3} (Λ_{s q}) = 0$ and $g_{2} (Λ_{s q}) \neq 0$ . For the hexagonal lattice $Λ_{h e x} = Z + Z ρ$ with $ρ = e^{2 π i / 3}$ one has $g_{2} (Λ_{h e x}) = 0$ and $g_{3} (Λ_{h e x}) \neq 0$ . In both cases $Δ \neq 0$ . The argument is a symmetry argument under multiplication by $i$ respectively by $ρ$ : no numerical value of any Eisenstein sum is evaluated.

Facts & Assumptions

Given: The lattices $Λ_{s q} : = Z + i Z$ and $Λ_{h e x} : = Z + Z ρ$ with $ρ : = e^{2 π i / 3}$ , their invariants $g_{2} = 60 G_{4}$ , $g_{3} = 140 G_{6}$ and discriminants $Δ = g_{2}^{3} - 27 g_{3}^{2}$ (Weierstrass p function, Weierstrass cubic differential equation, Nonvanishing of the lattice discriminant).

[F1]

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$ , so one of the two orderings is oriented (Complex lattice and quotient torus). The sums defining the Weierstrass data depend only on the lattice $Λ$ , not on the oriented basis chosen to describe it (Weierstrass p function).

[F2]

$G_{4} (Λ) = \sum_{ω \in Λ ∖ {0}} ω^{- 4}$ and $G_{6} (Λ) = \sum_{ω \in Λ ∖ {0}} ω^{- 6}$ are the unordered finite-subset sums over the lattice; both families are absolutely summable, so $G_{4} (Λ)$ and $G_{6} (Λ)$ are well-defined complex numbers, and the invariants are $g_{2} = 60 G_{4}$ , $g_{3} = 140 G_{6}$ (Weierstrass cubic differential equation).

[F3]

For every full complex lattice the discriminant $Δ = g_{2}^{3} - 27 g_{3}^{2}$ satisfies $Δ \neq 0$ (Nonvanishing of the lattice discriminant).

[F4]

The complex exponential satisfies $\exp (z + w) = \exp (z) \exp (w)$ for all $z, w$ , is nowhere zero, has kernel $\ker (\exp) = 2 π i Z$ , and $∣ \exp (i y) ∣ = 1$ for every real $y$ (The complex exponential by its power series, $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential, $\ker (\exp) = 2 π i Z$ , and $\exp z = \exp w$ exactly when $z - w \in 2 π i Z$ , $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

[F5]

$C$ is a field with $i^{2} = - 1$ , every complex number has a unique form $a + b i$ with $a, b \in R$ , and a product of two nonzero complex numbers is nonzero ( $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})$ , The complex numbers as $R [x] / (x^{2} + 1)$ , with the real embedding and imaginary unit $i$ ).

[F6]

For $z \in C$ one has $z = Re z + i Im z$ with $∣ z ∣^{2} = (Re z)^{2} + (Im z)^{2}$ , and $∣ z w ∣ = ∣ z ∣ ∣ w ∣$ for all $z, w$ (Real and imaginary parts, complex conjugation, and modulus, Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F7]

For nonzero $z, w \in C$ and integers $m, n$ one has $z^{m + n} = z^{m} z^{n}$ , $(z w)^{n} = z^{n} w^{n}$ and $z^{- n} = (z^{n})^{- 1}$ (Integer powers in the complex field).

Verification

1.1F4F5F6F7algebra

(The element $ρ$ , its inverse power and non-reality.) By [F4] and [F5], $ρ = e^{2 π i / 3}$ satisfies $ρ^{3} = e^{2 π i} = 1$ , and $ρ \neq 1$ because $2 π / 3 \notin 2 π Z$ ; also $ρ \neq - 1$ , since $(- 1)^{3} = - 1 \neq 1$ . Expanding $t^{3} - 1 = (t - 1) (t^{2} + t + 1)$ and using that $C$ is a field gives $0 = ρ^{3} - 1 = (ρ - 1) (ρ^{2} + ρ + 1)$ with $ρ - 1 \neq 0$ , hence $ρ^{2} + ρ + 1 = 0$ and $ρ^{2} = - 1 - ρ$ . Moreover $1 - ρ^{2} \neq 0$ : if $ρ^{2} = 1$ then $(ρ - 1) (ρ + 1) = 0$ , and a field has no zero divisors, so $ρ = 1$ or $ρ = - 1$ , both excluded. Finally $ρ \notin R$ : if $ρ$ were real, then $∣ ρ ∣^{2} = ρ^{2}$ by [F6], while $∣ ρ ∣ = ∣ \exp (2 π i / 3) ∣ = 1$ by [F4], so $ρ^{2} = 1$ and again $ρ = \pm 1$ , a contradiction. For the power law, $ρ^{- 4} = ρ^{- 4} (ρ^{3})^{2} = ρ^{- 4} ρ^{6} = ρ^{2}$ by [F7] and $ρ^{3} = 1$ .

1.2F2F7algebra

(Scaling identity for the lattice sums.) Let $Λ = Z ω_{1} + Z ω_{2}$ be a full lattice and $c \in C^{\times}$ . Then $c Λ = Z (c ω_{1}) + Z (c ω_{2})$ is again a full lattice: real-linear independence is preserved because $a (c ω_{1}) + b (c ω_{2}) = c (a ω_{1} + b ω_{2})$ vanishes only if $a ω_{1} + b ω_{2} = 0$ . For $k \in {4, 6}$ and every finite $E \subseteq Λ ∖ {0}$ one has $\sum_{ω \in E} (c ω)^{- k} = c^{- k} \sum_{ω \in E} ω^{- k}$ by [F7]; the map $E \mapsto c E$ is an order-isomorphism from the directed set of finite subsets of $Λ ∖ {0}$ onto that of $c Λ ∖ {0}$ , and the sum over $c Λ$ is the net of these finite sums by [F2]. Hence the net for $c Λ$ is the constant multiple $c^{- k}$ of the convergent net for $Λ$ , so it converges and $G_{k} (c Λ) = c^{- k} G_{k} (Λ)$ .

2.1F1F5step 1.1algebra

(The two lattices.) Since every complex number is uniquely $a + b i$ , the pair ${1, i}$ is a real basis of $C$ , so $Λ_{s q}$ is a full complex lattice with oriented basis $(1, i)$ ( $Im (i / 1) = 1 > 0$ ); and $i Λ_{s q} = Λ_{s q}$ : indeed $i \cdot 1 = i \in Λ_{s q}$ and $i \cdot i = - 1 \in Λ_{s q}$ , so $i Λ_{s q} \subseteq Λ_{s q}$ , while multiplication by $i$ is a bijection of $C$ with inverse multiplication by $i^{- 1} = - i$ , which likewise preserves $Λ_{s q}$ . Also $i^{- 6} = (i^{2})^{- 3} = (- 1)^{- 3} = - 1$ . For the hexagonal lattice: ${1, ρ}$ is real-linearly independent because $ρ \notin R$ by step 1.1, so $Λ_{h e x}$ is a full complex lattice and one of the orderings of $(1, ρ)$ is oriented by [F1]; and $ρ Λ_{h e x} = Λ_{h e x}$ because $ρ \cdot 1 = ρ \in Λ_{h e x}$ and $ρ \cdot ρ = ρ^{2} = - 1 - ρ \in Λ_{h e x}$ show $ρ Λ_{h e x} \subseteq Λ_{h e x}$ , while multiplication by $ρ$ is invertible on $C$ with inverse multiplication by $ρ^{- 1} = ρ^{2}$ , and $ρ^{2} Λ_{h e x} \subseteq Λ_{h e x}$ since $ρ^{2} \cdot 1 = ρ^{2} = - 1 - ρ \in Λ_{h e x}$ and $ρ^{2} \cdot ρ = ρ^{3} = 1 \in Λ_{h e x}$ .

3.1F2F5step 1.2step 2.1algebra

( $g_{3} (Λ_{s q}) = 0$ .) By step 2.1, $i Λ_{s q} = Λ_{s q}$ , hence $G_{6} (Λ_{s q}) = G_{6} (i Λ_{s q}) = i^{- 6} G_{6} (Λ_{s q}) = - G_{6} (Λ_{s q})$ by step 1.2 with $c = i$ ; therefore $2 G_{6} (Λ_{s q}) = 0$ and, since $C$ is a field, $G_{6} (Λ_{s q}) = 0$ , so $g_{3} (Λ_{s q}) = 140 \cdot 0 = 0$ .

3.2F2F5step 1.1step 1.2step 2.1algebra

( $g_{2} (Λ_{h e x}) = 0$ .) By step 2.1, $ρ Λ_{h e x} = Λ_{h e x}$ , hence $G_{4} (Λ_{h e x}) = G_{4} (ρ Λ_{h e x}) = ρ^{- 4} G_{4} (Λ_{h e x}) = ρ^{2} G_{4} (Λ_{h e x})$ by step 1.2 with $c = ρ$ and step 1.1; therefore $(1 - ρ^{2}) G_{4} (Λ_{h e x}) = 0$ , and since $1 - ρ^{2} \neq 0$ by step 1.1 and $C$ is a field, $G_{4} (Λ_{h e x}) = 0$ , so $g_{2} (Λ_{h e x}) = 60 \cdot 0 = 0$ .

4.1F3F5step 3.1step 3.2algebra

(The complementary invariants and the discriminant.) By [F3] the discriminant is nonzero for both lattices. For $Λ_{s q}$ step 3.1 gives $Δ (Λ_{s q}) = g_{2}^{3} - 27 \cdot 0^{2} = g_{2}^{3}$ , which is nonzero, so $g_{2} (Λ_{s q}) \neq 0$ in the field $C$ . For $Λ_{h e x}$ step 3.2 gives $Δ (Λ_{h e x}) = 0^{3} - 27 g_{3}^{2} = - 27 g_{3}^{2}$ with $- 27 \neq 0$ , and a nonzero discriminant forces $g_{3}^{2} \neq 0$ , hence $g_{3} (Λ_{h e x}) \neq 0$ .

5.1

(Assembly.) Step 3.1 gives $g_{3} (Λ_{s q}) = 0$ and step 4.1 gives $g_{2} (Λ_{s q}) \neq 0$ ; step 3.2 gives $g_{2} (Λ_{h e x}) = 0$ and step 4.1 gives $g_{3} (Λ_{h e x}) \neq 0$ ; step 4.1 also gives $Δ \neq 0$ in both cases. These are exactly the assertions of the example. ∎

Remarks

The two symmetries are the only inputs: $i Λ_{s q} = Λ_{s q}$ reindexes the $G_{6}$ -sum into its negative, and $ρ Λ_{h e x} = Λ_{h e x}$ reindexes the $G_{4}$ -sum into $ρ^{2}$ times itself. The complementary invariant is then forced to be nonzero by $Δ \neq 0$ , so no Eisenstein sum is evaluated numerically and no transcendental input about the elliptic integral is used. The hexagonal case is the equianharmonic one: its cubic $4 x^{3} - g_{3}$ of Nonvanishing of the lattice discriminant has no $x$ -term, while the square lattice is the one whose cubic has no constant term.

Depends on

Used by

Half-period values of the square lattice Example

Dependency tree · two levels

63 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 (standard reference, not scraped)