Ranks of the elliptic curves y² = x³ − 2pqx
TheoremMultivariable Hensel lemma over the p-adic integers#●ready to prove
Let \(p\) be a prime, let \(f \in \mathbb{Z}_p[x_1, \dots, x_n]\) and \(a \in \mathbb{Z}_p^n\), and suppose that for some index \(i\) the \(p\)-adic absolute values satisfy \(|f(a)|_p < |(\partial f / \partial x_i)(a)|_p^2\), that is, \(\operatorname{ord}_p f(a) > 2 \operatorname{ord}_p (\partial f / \partial x_i)(a)\). Then there is a point \(x \in \mathbb{Z}_p^n\) with \(f(x) = 0\).
public theorem_wanted exists_mvPolynomial_eval_eq_zero_of_norm_lt_norm_pderiv_sq
{p : ℕ} [Fact p.Prime] {n : ℕ} (f : MvPolynomial (Fin n) ℤ_[p]) (a : Fin n → ℤ_[p])
(i : Fin n)
(h : ‖MvPolynomial.eval a f‖ < ‖MvPolynomial.eval a (MvPolynomial.pderiv i f)‖ ^ 2) :
∃ x : Fin n → ℤ_[p], MvPolynomial.eval x f = 0Sources
- Renz Jimwel Mina and Jerico Bacani, Rank of the Elliptic Curve y^2=x^3-2pqx, INTEGERS 26 (2026), Article A51, Lemma 1, quoted there as Hensel's lemma.
TheoremOdd-rank curves y² = x³ − 2pqx: rank one cases#●ready to prove
Let \(p \ne q\) be primes and let \(E\) be the elliptic curve \(y^2 = x^3 - 2pqx\) over \(\mathbb{Q}\). Suppose that \((p \bmod 8, q \bmod 8)\) is one of \((3, 3)\), \((3, 5)\), \((3, 7)\), \((5, 5)\), \((5, 7)\), or that \(p \equiv 1 \pmod 8\), \(q \equiv 3, 5\) or \(7 \pmod 8\) and the Legendre symbol \(\left(\frac{p}{q}\right)\) equals \(-1\). If the rank of the group \(E(\mathbb{Q})\) of rational points is odd, then it equals \(1\).
The odd-rank hypothesis stands for the parity conjecture for \(E\). The case with \(p\) and \(q\) interchanged is the same curve.
public theorem_wanted finrank_point_two_mul_mul_eq_one {p q : ℕ} (hp : p.Prime) (hq : q.Prime)
(hpq : p ≠ q) (E : WeierstrassCurve ℚ)
(hE : E = ⟨0, 0, 0, -(2 * p * q : ℚ), 0⟩)
(hcase : (p % 8, q % 8) ∈ [(3, 3), (3, 5), (3, 7), (5, 5), (5, 7)] ∨
(p % 8 = 1 ∧ q % 8 ∈ [3, 5, 7] ∧ jacobiSym p q = -1))
(hparity : Odd (Module.finrank ℤ E.toProjective.Point)) :
Module.finrank ℤ E.toProjective.Point = 1Sources
- Renz Jimwel Mina and Jerico Bacani, Rank of the Elliptic Curve y^2=x^3-2pqx, INTEGERS 26 (2026), Article A51, Theorem 1 (i).
TheoremOdd-rank curves y² = x³ − 2pqx: rank one or three cases#●ready to prove
Let \(p \ne q\) be primes and let \(E\) be the elliptic curve \(y^2 = x^3 - 2pqx\) over \(\mathbb{Q}\), and write \(\left(\frac{p}{q}\right)\) for the Legendre symbol. Suppose that \(p \equiv q \equiv 1 \pmod 8\) and \(\left(\frac{p}{q}\right) = -1\), or that \(p \equiv q \equiv 7 \pmod 8\), or that \(p \equiv 1 \pmod 8\), \(q \equiv 3, 5\) or \(7 \pmod 8\) and \(\left(\frac{p}{q}\right) = 1\). If the rank of the group \(E(\mathbb{Q})\) of rational points is odd, then it equals \(1\) or \(3\).
The odd-rank hypothesis stands for the parity conjecture for \(E\).
public theorem_wanted finrank_point_two_mul_mul_eq_one_or_three {p q : ℕ} (hp : p.Prime)
(hq : q.Prime) (hpq : p ≠ q) (E : WeierstrassCurve ℚ)
(hE : E = ⟨0, 0, 0, -(2 * p * q : ℚ), 0⟩)
(hcase : (p % 8 = 1 ∧ q % 8 = 1 ∧ jacobiSym p q = -1) ∨ (p % 8 = 7 ∧ q % 8 = 7) ∨
(p % 8 = 1 ∧ q % 8 ∈ [3, 5, 7] ∧ jacobiSym p q = 1))
(hparity : Odd (Module.finrank ℤ E.toProjective.Point)) :
Module.finrank ℤ E.toProjective.Point = 1 ∨ Module.finrank ℤ E.toProjective.Point = 3Sources
- Renz Jimwel Mina and Jerico Bacani, Rank of the Elliptic Curve y^2=x^3-2pqx, INTEGERS 26 (2026), Article A51, Theorem 1 (ii).
TheoremOdd-rank curves y² = x³ − 2pqx: rank one, three or five case#●ready to prove
Let \(p \ne q\) be primes with \(p \equiv q \equiv 1 \pmod 8\) and Legendre symbol \(\left(\frac{p}{q}\right) = 1\), and let \(E\) be the elliptic curve \(y^2 = x^3 - 2pqx\) over \(\mathbb{Q}\). If the rank of the group \(E(\mathbb{Q})\) of rational points is odd, then it equals \(1\), \(3\) or \(5\).
The odd-rank hypothesis stands for the parity conjecture for \(E\).
public theorem_wanted finrank_point_two_mul_mul_eq_one_or_three_or_five {p q : ℕ}
(hp : p.Prime) (hq : q.Prime) (hpq : p ≠ q) (E : WeierstrassCurve ℚ)
(hE : E = ⟨0, 0, 0, -(2 * p * q : ℚ), 0⟩)
(hcase : p % 8 = 1 ∧ q % 8 = 1 ∧ jacobiSym p q = 1)
(hparity : Odd (Module.finrank ℤ E.toProjective.Point)) :
Module.finrank ℤ E.toProjective.Point = 1 ∨ Module.finrank ℤ E.toProjective.Point = 3 ∨
Module.finrank ℤ E.toProjective.Point = 5Sources
- Renz Jimwel Mina and Jerico Bacani, Rank of the Elliptic Curve y^2=x^3-2pqx, INTEGERS 26 (2026), Article A51, Theorem 1 (iii).
TheoremOdd-rank curves y² = x³ − 2pqx: a rank three family#●ready to prove
Let \(r\) be a positive integer such that \(p = 272r^2 + 120r + 9\) and \(q = 2p + 9 = 544r^2 + 240r + 27\) are both prime, and let \(E\) be the elliptic curve \(y^2 = x^3 - 2pqx\) over \(\mathbb{Q}\). If the rank of the group \(E(\mathbb{Q})\) of rational points is odd, then it equals \(3\).
The odd-rank hypothesis stands for the parity conjecture for \(E\).
public theorem_wanted finrank_point_two_mul_mul_eq_three {r : ℕ} (hr : 0 < r)
(hp : (272 * r ^ 2 + 120 * r + 9).Prime) (hq : (544 * r ^ 2 + 240 * r + 27).Prime)
(E : WeierstrassCurve ℚ)
(hE : E = ⟨0, 0, 0,
-(2 * (272 * r ^ 2 + 120 * r + 9 : ℕ) * (544 * r ^ 2 + 240 * r + 27 : ℕ) : ℚ), 0⟩)
(hparity : Odd (Module.finrank ℤ E.toProjective.Point)) :
Module.finrank ℤ E.toProjective.Point = 3Sources
- Renz Jimwel Mina and Jerico Bacani, Rank of the Elliptic Curve y^2=x^3-2pqx, INTEGERS 26 (2026), Article A51, Theorem 2.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.