The fundamental unit, the regulator and the height of 1 + √2

Let K be a number field generated over ℚ by an algebraic integer θ with minpoly ℤ θ = X² − 2, so that K = ℚ(√2). Then 1 + θ is a unit, since (1 + θ) (θ − 1) = θ² − 1 = 1, and at the real place where θ has the value √2 it has the value 1 + √2. The unit candidates below 1 + √2 are the quadratics X² + mX ± 1 with |m| ≤ 3. All but X² − X − 1 have no real root in (1, 1 + √2), and X² − X − 1 has discriminant 5, which is not 8 times a square, so it is not the minimal polynomial of an integral primitive element of a field of discriminant 8. This elimination certificate makes 1 + θ a fundamental unit, and the regulator of ℚ(√2) is Real.log (1 + √2).

In unit rank one the logarithmic height of a fundamental unit is the regulator, so absLogHeight₁ (1 + θ) = Real.log (1 + √2) / 2. This is the test case for the comparison between the regulator and the heights of a fundamental system at r = 1, d = 2: Hadamard's upper bound reads log (1 + √2) ≤ 4 · log (1 + √2) / 2, while Bugeaud–Győry's bound ∏ i, h(ε i) ≤ (r!)² / (2 ^ (r − 1) d ^ r) · regulator K for a reduced fundamental system holds with equality, log (1 + √2) / 2 = (1 / 2) · log (1 + √2), so its constant cannot be lowered.

Main results

• TauCeti.NumberField.Sqrt2.one_add_mul_sub_one_eq_one: (1 + θ) (θ − 1) = 1, so 1 + θ is a unit (TauCeti.NumberField.Sqrt2.isUnit_one_add).
• TauCeti.NumberField.Sqrt2.unitCandidateEliminationCertificate_one_add_sqrt_two: the elimination certificate at 1 + √2.
• TauCeti.NumberField.Sqrt2.closure_sup_torsion_eq_top: a unit with value 1 + θ generates the units of ℚ(√2) modulo torsion.
• TauCeti.NumberField.Sqrt2.regulator_eq_log_one_add_sqrt_two: regulator K = Real.log (1 + √2).
• TauCeti.NumberField.Sqrt2.absLogHeight₁_one_add_eq: absLogHeight₁ (1 + θ) = Real.log (1 + √2) / 2.
• TauCeti.NumberField.Sqrt2.absLogHeight₁_one_add_eq_regulator_div_two and TauCeti.NumberField.Sqrt2.regulator_le_four_mul_absLogHeight₁_one_add: the two comparisons between the regulator and the height of the fundamental unit.

References

• H. Cohen, A Course in Computational Algebraic Number Theory, §5.7.
• Y. Bugeaud and K. Győry, Bounds for the solutions of unit equations, Acta Arith. 74 (1996), 67–80, §3, Lemma 1.

@[simp]

theorem TauCeti.NumberField.Sqrt2.one_add_mul_sub_one_eq_one {K : Type u_1} [Field K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - 2) : (1 + θ) * (θ - 1) = 1

An algebraic integer θ with minpoly ℤ θ = X² − 2 makes 1 + θ a unit: (1 + θ) (θ − 1) = 1.

theorem TauCeti.NumberField.Sqrt2.isUnit_one_add {K : Type u_1} [Field K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - 2) : IsUnit (1 + θ)

1 + θ is a unit of 𝓞 K.

theorem TauCeti.NumberField.Sqrt2.unitCandidateEliminationCertificate_one_add_sqrt_two {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - 2) (hgen : ℚ[↑θ] = ⊤) : Units.UnitCandidateEliminationCertificate K (1 + √2)

The elimination certificate at 1 + √2. In ℚ(√2), every candidate polynomial X² + mX ± 1 with |m| ≤ 2 + √2 either has no real root in (1, 1 + √2) or, as for X² − X − 1, has a discriminant that is not 8 times a positive square.

theorem TauCeti.NumberField.Sqrt2.closure_sup_torsion_eq_top {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - 2) (hgen : ℚ[↑θ] = ⊤) {u : (NumberField.RingOfIntegers K)ˣ} (hu : ↑u = 1 + θ) : Subgroup.closure {u} ⊔ NumberField.Units.torsion K = ⊤

1 + √2 is a fundamental unit of ℚ(√2). A unit u with (u : 𝓞 K) = 1 + θ generates the unit group modulo torsion.

theorem TauCeti.NumberField.Sqrt2.regulator_eq_log_one_add_sqrt_two {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - 2) (hgen : ℚ[↑θ] = ⊤) : NumberField.Units.regulator K = Real.log (1 + √2)

The regulator of ℚ(√2) is Real.log (1 + √2).

theorem TauCeti.NumberField.Sqrt2.absLogHeight₁_one_add_eq_regulator_div_two {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - 2) (hgen : ℚ[↑θ] = ⊤) : NumberField.absLogHeight₁ ↑(1 + θ) = NumberField.Units.regulator K / 2

The reduced bound is sharp at ℚ(√2). The absolute logarithmic height of the fundamental unit 1 + √2 equals (r!)² / (2 ^ (r - 1) d ^ r) = 1 / 2 times the regulator.

theorem TauCeti.NumberField.Sqrt2.absLogHeight₁_one_add_eq {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - 2) (hgen : ℚ[↑θ] = ⊤) : NumberField.absLogHeight₁ ↑(1 + θ) = Real.log (1 + √2) / 2

The absolute logarithmic height of the fundamental unit 1 + √2 of ℚ(√2) is Real.log (1 + √2) / 2.

theorem TauCeti.NumberField.Sqrt2.regulator_le_four_mul_absLogHeight₁_one_add {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - 2) (hgen : ℚ[↑θ] = ⊤) : NumberField.Units.regulator K ≤ 4 * NumberField.absLogHeight₁ ↑(1 + θ)

Hadamard's bound at ℚ(√2). The regulator is at most (2d) ^ r = 4 times the absolute logarithmic height of the fundamental unit; here log (1 + √2) ≤ 4 · log (1 + √2) / 2.