Heights of rational points on elliptic curves

TheoremHeight lower bounds on \(y^2 = x^3 + ax + b\) when \(a = \pm 1\) or \(b = \pm 1\)#●ready to prove

Let \(a, b \in \mathbb{Z}\) with \(4a^3 + 27b^2 \ne 0\), and for \(u, v \in \mathbb{Q}\) let \(H(u, v) = \max(|U|, |V|, |W|)\), where \(U, V, W\) are coprime integers with \((U : V : W) = (u : v : 1)\). Consider the rational solutions \((u, v)\) of \(v^2 = u^3 + au + b\). (a) If \(a = \pm 1\) and \(b \notin \{0, 1, -1\}\), every solution has \(H(u, v) \ge (|b|/5)^{1/3}\). (b) If \(a \notin \{0, 1, -1\}\) and \(b = -1\), every solution has \(H(u, v) \ge (|a|/5)^{1/3}\). (c) If \(a \notin \{0, 1, -1\}\) and \(b = 1\), every solution with \(H(u, v) < (|a|/5)^{1/3}\) is \((0, 1)\) or \((0, -1)\).

public theorem_wanted naiveHeight_lower_bound_of_unit_coeff (a b : ℤ)
    (hE : 4 * a ^ 3 + 27 * b ^ 2 ≠ 0) :
    ((a = 1 ∨ a = -1) → b ≠ 0 → b ≠ 1 → b ≠ -1 → ∀ u v : ℚ, v ^ 2 = u ^ 3 + a * u + b →
        ¬ Height.mulHeight ![u, v, 1] < (|(b : ℝ)| / 5) ^ ((1 : ℝ) / 3)) ∧
      (a ≠ 0 → a ≠ 1 → a ≠ -1 → b = -1 → ∀ u v : ℚ, v ^ 2 = u ^ 3 + a * u + b →
        ¬ Height.mulHeight ![u, v, 1] < (|(a : ℝ)| / 5) ^ ((1 : ℝ) / 3)) ∧
      (a ≠ 0 → a ≠ 1 → a ≠ -1 → b = 1 → ∀ u v : ℚ, v ^ 2 = u ^ 3 + a * u + b →
        Height.mulHeight ![u, v, 1] < (|(a : ℝ)| / 5) ^ ((1 : ℝ) / 3) →
          u = 0 ∧ (v = 1 ∨ v = -1))

Sources

• Dimitrios Poulakis, Lower Bounds for the Height of Rational Points of Elliptic Curves, INTEGERS 25 (2025), Article A66, Theorem 2.

TheoremHeight lower bounds on \(y^2 = x^3 + ax + b\) when \(b = \pm a\), \(b = 0\) or \(a = 0\)#●ready to prove

Let \(a, b \in \mathbb{Z}\) with \(4a^3 + 27b^2 \ne 0\), and for \(u, v \in \mathbb{Q}\) let \(H(u, v) = \max(|U|, |V|, |W|)\), where \(U, V, W\) are coprime integers with \((U : V : W) = (u : v : 1)\). Consider the rational solutions \((u, v)\) of \(v^2 = u^3 + au + b\). (a) If \(b = a\), every solution has \(H(u, v) \ge (|a|/4)^{1/3}\). (b) If \(b = -a\), every solution with \(H(u, v) < (|a|/4)^{1/3}\) is \((1, 1)\) or \((1, -1)\). (c) If \(b = 0\), every solution with \(H(u, v) < (|a|/4)^{1/3}\) is \((0, 0)\). (d) If \(a = 0\), every solution has \(H(u, v) \ge (|b|/3)^{1/3}\).

In (b) the points \((1, \pm 1)\) and the point at infinity need not form a subgroup of order three: for \(a = 5\), doubling \((1, 1)\) gives \((14, -53)\).

public theorem_wanted naiveHeight_lower_bound_of_special_coeff (a b : ℤ)
    (hE : 4 * a ^ 3 + 27 * b ^ 2 ≠ 0) :
    (b = a → ∀ u v : ℚ, v ^ 2 = u ^ 3 + a * u + b →
        ¬ Height.mulHeight ![u, v, 1] < (|(a : ℝ)| / 4) ^ ((1 : ℝ) / 3)) ∧
      (b = -a → ∀ u v : ℚ, v ^ 2 = u ^ 3 + a * u + b →
        Height.mulHeight ![u, v, 1] < (|(a : ℝ)| / 4) ^ ((1 : ℝ) / 3) →
          u = 1 ∧ (v = 1 ∨ v = -1)) ∧
      (b = 0 → ∀ u v : ℚ, v ^ 2 = u ^ 3 + a * u + b →
        Height.mulHeight ![u, v, 1] < (|(a : ℝ)| / 4) ^ ((1 : ℝ) / 3) → u = 0 ∧ v = 0) ∧
      (a = 0 → ∀ u v : ℚ, v ^ 2 = u ^ 3 + a * u + b →
        ¬ Height.mulHeight ![u, v, 1] < (|(b : ℝ)| / 3) ^ ((1 : ℝ) / 3))

Sources

• Dimitrios Poulakis, Lower Bounds for the Height of Rational Points of Elliptic Curves, INTEGERS 25 (2025), Article A66, Theorem 3.

TheoremHeight of a point on \(y^2 = x^3 + ax - b\) versus the height of its \(x\)-coordinate#●ready to prove

Let \(a, b \in \mathbb{Z}\) with \(a \ne 0\), \(b > 0\) and \(4a^3 + 27b^2 \ne 0\). For \(u \in \mathbb{Q}\) let \(H(u) = \max(|u_0|, u_1)\), where \(u = u_0/u_1\) in lowest terms with \(u_1 > 0\), and for \(u, v \in \mathbb{Q}\) let \(H(u, v) = \max(|U|, |V|, |W|)\), where \(U, V, W\) are coprime integers with \((U : V : W) = (u : v : 1)\). Then every rational solution \((u, v)\) of \(v^2 = u^3 + au - b\) satisfies \(H(u, v) < \sqrt{1 + |a|}\, H(u)^{3/2}\).

public theorem_wanted naiveHeight_lt_sqrt_mul_naiveHeight_x_rpow (a b : ℤ) (ha : a ≠ 0)
    (hb : 0 < b) (hE : 4 * a ^ 3 + 27 * b ^ 2 ≠ 0) (u v : ℚ)
    (hP : v ^ 2 = u ^ 3 + a * u - b) :
    Height.mulHeight ![u, v, 1] <
      Real.sqrt (1 + |(a : ℝ)|) * Height.mulHeight ![u, 1] ^ ((3 : ℝ) / 2)

Sources

• Dimitrios Poulakis, Lower Bounds for the Height of Rational Points of Elliptic Curves, INTEGERS 25 (2025), Article A66, Lemma 4.

TheoremHeight lower bound on \(y^2 = x^3 + ax + b\) when \(|a|\) is small#●ready to prove

Let \(a, b \in \mathbb{Z}\) with \(ab \ne 0\) and \(4a^3 + 27b^2 \ne 0\), let \(\lVert p \rVert = \sqrt{2 + a^2 + b^2}\), and suppose \(1 + |a| < \lVert p \rVert^{1/2}/1.782\). For \(u, v \in \mathbb{Q}\) let \(H(u, v) = \max(|U|, |V|, |W|)\), where \(U, V, W\) are coprime integers with \((U : V : W) = (u : v : 1)\). Then every rational solution \((u, v)\) of \(v^2 = u^3 + au + b\) with \(uv \ne 0\) satisfies \(H(u, v) > \lVert p \rVert^{1/6}/1.634\).

public theorem_wanted naiveHeight_gt_of_small_linear_coeff (a b : ℤ) (hab : a * b ≠ 0)
    (hE : 4 * a ^ 3 + 27 * b ^ 2 ≠ 0)
    (hsmall : 1 + |(a : ℝ)| < Real.sqrt (2 + a ^ 2 + b ^ 2) ^ ((1 : ℝ) / 2) / 1.782) (u v : ℚ)
    (huv : u * v ≠ 0) (hP : v ^ 2 = u ^ 3 + a * u + b) :
    Real.sqrt (2 + a ^ 2 + b ^ 2) ^ ((1 : ℝ) / 6) / 1.634 < Height.mulHeight ![u, v, 1]

Sources

• Dimitrios Poulakis, Lower Bounds for the Height of Rational Points of Elliptic Curves, INTEGERS 25 (2025), Article A66, Corollary 1.

4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.