Division values (Milla, Appendix A) #
Division points of a period lattice, the functions F_m = σ(mz)/σ(z)^{m²}, and the
two outputs consumed by Appendix B (PLAN B1):
theowpsum:∑_{u ∈ DIV(m)} ℘(u) = 0;theomwpu:m·℘(u)(andm/2·℘(u)for evenm) is integral overℤ[¼g₂, ¼g₃].
The m-division points in the fundamental parallelogram are indexed by pairs
(k, l) ∈ (ℤ/m)² \ {0} via u = (k/m)·ω₁ + (l/m)·ω₂ (paper Lemma lemmm:
there are m² − 1 of them).
TODO (PLAN B1): the division polynomials P_m ∈ ℤ[x, h₂, h₃] with their four-case
recursion, Baker's factorization thmbaker
(m²·∏_{u ∈ DIV(m)} (x − ℘(u)) = P_m(x)² · (4(x³ − h₂x − h₃))^{[m even]}) and the
structure lemmas propindu, from which the two theorems below follow.
The σ-transformation law (paper Prop. trafosigma) #
We derive the transformation law of the Weierstrass σ-function in a single period direction
ω (with ω/2 ∉ L), and its n-fold iterate. This is the local copy referred to in the
plan (parallel to the derivation in Fourier.lean, which we cannot import here).
Milla's F_m(z) = σ(mz)/σ(z)^{m²} (Lemma lemdefifm): an elliptic function with
a pole of order m² − 1 on L and simple zeros exactly at the m-division points.
Equations
- L.Fm m z = L.weierstrassSigma (↑m * z) / L.weierstrassSigma z ^ m ^ 2
Instances For
The multiplication formula and theowpsum (the ζ-trick) #
We prove ∑_{v ≠ 0} ℘(u_v) = 0 (theowpsum) directly, without the division polynomials.
The argument has three steps:
- the multiplication formula
∑_{v} ℘(z + u_v) = m²·℘(mz) + c(the difference is entire and doubly periodic, hence constant by the first Liouville theorem — the removable singularities at them-torsion points are handled algebraically viaweierstrassPExcept); - the constant
cvanishes, via the ζ-function∑_v ζ(z+u_v) − m·ζ(mz), whose derivative is the multiplication difference and which is doubly periodic (quasi-periods cancel); - evaluation of the multiplication formula at
z = 0.
Milla's theowpsum: the sum of ℘ over all m-division points vanishes.
(From the vanishing of the second-highest coefficient in thmbaker.)
lemwpsigma: the σ-quotient formula for ℘(v) − ℘(u) #
We prove ℘(v) − ℘(u) = σ(u+v)σ(u−v)/(σ(u)²σ(v)²) (paper Lemma lemwpsigma) by the paper's
direct argument: fix v ∉ L; the difference F(u) := σ(u+v)σ(u−v)/(σ(u)²σ(v)²) + ℘(u) − ℘(v)
is elliptic in u, has its two double poles at u ∈ L cancel (Laurent computation via the
trailing coefficient σ'(0) = 1 and the evenness F(−u) = F(u)), hence is entire and constant
(first Liouville theorem), and F(v) = 0 since σ(0) = 0.
Assembly of lemwpsigma (paper Lemma lemwpsigma) #
℘(v) − ℘(u) = σ(u+v)·σ(u−v)/(σ(u)²σ(v)²) for u, v ∉ L, via the workhorse lemma:
the σ-quotient A(u) = σ(u+v)σ(u−v)/σ(u)² and g(u) = ℘(u) − ℘(v) are elliptic in u
with identical divisors, so A = c·g up to a codiscrete set; the constant is pinned by
the trailing coefficients at u = 0 (c = −σ(v)²), and the identity upgrades to all
u ∉ L by the identity theorem on the connected set Lᶜ.
Milla's lemwpsigma: for u, v ∉ L,
℘(v) − ℘(u) = σ(u+v)·σ(u−v)/(σ(u)²·σ(v)²).
propfmprod: F_m(z)² = m²·∏_{v ≠ 0} (℘(z) − ℘(u_v)) (paper Thm. propfmprod) #
Proved by the same workhorse scheme: both sides are elliptic with identical divisors
(−2(m²−1) on L, total order 2 on each nonzero m-torsion class, 0 elsewhere),
and the constant is pinned by the trailing coefficients at 0
(F_m ≈ m·z^{−(m²−1)} and each factor ℘ − ℘(u_v) ≈ z⁻²).
Milla's propfmprod: for z ∉ L,
F_m(z)² = m²·∏_{v ≠ 0} (℘(z) − ℘(u_v)).
Milla's lemwpnz: ℘(nz) = ℘(z) − F_{n−1}(z)·F_{n+1}(z)/F_n(z)² for z, nz ∉ L
(from lemwpsigma with u = z, v = nz, σ-oddness and the definition of F_k).
The division polynomials P_m (paper Def. defipm) #
Integer polynomials in x (outer variable) and h₂ = ¼g₂, h₃ = ¼g₃ (inner variables
X 0, X 1 of the coefficient ring ℤ[h₂, h₃]), defined by Milla's four-case recursion.
Verified (sympy, numerically to m = 15) against the classical elliptic division
polynomials ψ_m for y² = x³ + ax + b with a = −h₂, b = −h₃:
P_m = ψ_m for odd m and P_m = ψ_m/(2y) for even m.
The coefficient ring ℤ[h₂, h₃]; h₂ = X 0, h₃ = X 1.
Equations
- Milla.Coeff = MvPolynomial (Fin 2) ℤ
Instances For
E = 16(x³ − h₂x − h₃)², the polynomial with E(℘) = (℘′)⁴ (paper dglP).
Equations
- Milla.E = 16 * (Polynomial.X ^ 3 - Polynomial.C Milla.h2 * Polynomial.X - Polynomial.C Milla.h3) ^ 2
Instances For
Milla's division polynomials P_m (paper Def. defipm); P 0 = 0 by convention.
P₁ = P₂ = 1, explicit quartic/sextic P₃, P₄, and for m = 4k + r ≥ 5:
P_{4k+1} = E·P_{2k+2}·P_{2k}³ − P_{2k−1}·P_{2k+1}³P_{4k+2} = P_{2k+1}·(P_{2k+3}·P_{2k}² − P_{2k−1}·P_{2k+2}²)P_{4k+3} = P_{2k+3}·P_{2k+1}³ − E·P_{2k}·P_{2k+2}³P_{4k+4} = P_{2k+2}·(P_{2k+4}·P_{2k+1}² − P_{2k}·P_{2k+3}²)
Equations
- One or more equations did not get rendered due to their size.
- Milla.P 0 = 0
- Milla.P 1 = 1
- Milla.P 2 = 1
- Milla.P 3 = Polynomial.C 3 * Polynomial.X ^ 4 - Polynomial.C (6 * Milla.h2) * Polynomial.X ^ 2 - Polynomial.C (12 * Milla.h3) * Polynomial.X - Polynomial.C (Milla.h2 ^ 2)
Instances For
Degree and leading coefficient of P_m (paper Thm. propindu (2), (3)) #
natDegree (P m) = (m²−1)/2 and leadingCoeff = m for odd m;
natDegree (P m) = (m²−4)/2 and leadingCoeff = m/2 for even m ≥ 2
(with the exact sign +l_m, refining the paper's ±l_m).
propindu (3), odd case (with the exact sign): leadingCoeff (P (2j+1)) = 2j+1.
propindu (3), even case (with the exact sign): leadingCoeff (P (2j+2)) = j+1.
lemwp2str: ℘'' = 6℘² − g₂/2 (paper Lemma lemwp2str) #
Obtained by differentiating the algebraic differential equation ℘′² = 4℘³ − g₂℘ − g₃
(Mathlib's derivWeierstrassP_sq), cancelling ℘′ where it is nonzero, and removing
the 2-torsion zeros of ℘′ by the identity theorem on the connected set Lᶜ.
F₂ = −℘′ (paper propfmpm, case m = 2) #
Writing σ(z−v) = (z−v)·Q(z−v) with the entire σ-product Q (Q(0) = 1), the formula
lemwpsigma becomes ℘(v) − ℘(z) = (z−v)·H(v) for v near z; differentiating at
v = z gives ℘′(z) = −H(z) = −σ(2z)/σ(z)⁴ = −F₂(z) — no Laurent series needed.
Duplication (paper lemwp2str, second half) #
The derivative of F₂ = σ(2z)/σ(z)⁴ = −℘′ gives ℘'' = 2(ζ(2z) − 2ζ(z))·℘′;
differentiating once more (with ζ′ = −℘ and ℘''' = 12℘℘′) eliminates ζ and
yields the duplication formula, and one further derivative yields ℘′(2z) and F₄.
The recursions lemfrekur (paper Lemma lemfrekur) #
Both recursions follow from the master identity
F_{2a+d}·F_d = F_{a+d}²·F_a²·(℘(az) − ℘((a+d)z)) — which is lemwpsigma at
u = (a+d)z, v = az plus σ-exponent bookkeeping — combined with lemwpnz.
This replaces the paper's three-term σ-identity lemsigmasigma.
Paper lemfrekur, second recursion:
F_{2j+4}·F₂ = F_{j+2}·(F_{j+4}·F_{j+1}² − F_j·F_{j+3}²) at generic z.
propfmpm: F_m = P̂_m(℘) (odd m) and F_m = −℘′·P̂_m(℘) (even m) #
P̂_m is Milla's division polynomial P_m with coefficients evaluated at
h₂ = ¼g₂, h₃ = ¼g₃ (paper Thm. propfmpm).
The evaluation ℤ[h₂, h₃] → ℂ, h₂ ↦ ¼g₂, h₃ ↦ ¼g₃.
Instances For
P̂_m ∈ ℂ[X]: Milla's division polynomial with h₂ = ¼g₂, h₃ = ¼g₃.
Equations
- L.Pc m = Polynomial.map L.coeffToC (Milla.P m)
Instances For
Milla's propfmpm: at a generic point z (all nonzero integer multiples of z
avoid L), F_m(z) = P̂_m(℘(z)) for odd m and F_m(z) = −℘′(z)·P̂_m(℘(z)) for
even m.
thmbaker (paper Thm. thmbaker) #
Both sides are polynomials in ℘(z); by propfmprod and propfmpm they agree at
℘(z) for every generic z, and ℘ takes infinitely many values at generic points
(irrational real multiples of ω₁), so they agree in ℂ[X].
Milla's thmbaker, odd case: m²·∏_{v ≠ 0}(X − ℘(u_v)) = P̂_m(X)² in ℂ[X].
Milla's thmbaker, even case:
m²·∏_{v ≠ 0}(X − ℘(u_v)) = P̂_m(X)²·4(X³ − ¼g₂X − ¼g₃) in ℂ[X].
The endgame: integrality of l_m·℘(u) (paper Thm. theomwpu) #
By thmbaker, each division value ℘(u) is a root of P̂_m(X)²·(4(X³ − h₂X − h₃))^{[m even]}.
Roots of the monic cubic are integral over R = ℤ[¼g₂, ¼g₃]; for roots of P̂_m we use
Polynomial.integralNormalization together with the leading coefficient l_m computed in
P_odd_leadingCoeff/P_even_leadingCoeff.
Milla's theomwpu: for every m-division point u, m·℘(u) is integral over
ℤ[¼g₂, ¼g₃].