An explicit height gap for nontorsion units

There are at most unitPowerCountBound d algebraic integers of degree at most d whose conjugates have modulus at most two. If a unit has relative logarithmic height less than log 2 / (unitPowerCountBound d + 1), its first unitPowerCountBound d + 1 powers all belong to this set. Two powers coincide, so the unit is torsion.

This gives a deliberately coarse, explicit degree-only lower bound for the height of every nontorsion unit. Unlike a minimum obtained from qualitative Northcott finiteness, the bound is a finite sum of natural-number expressions and log 2. The same gap holds for every nonzero algebraic integer of infinite multiplicative order.

The counting input is TauCeti.finite_setOf_isIntegral_house_le; the proof does not require a lower bound for Mahler measure such as Dobrowolski's theorem.

def TauCeti.NumberField.Units.unitPowerCountBound (d : ℕ) : ℕ

An explicit upper bound on the number of algebraic integers of degree at most d with house at most two.

theorem TauCeti.NumberField.Units.unitPowerCountBound_def (d : ℕ) : unitPowerCountBound d = ∑ k ∈ Finset.range (d + 1), k * (2 * 4 ^ k + 1) ^ k

The finite-sum formula for the bounded-power count.

noncomputable def TauCeti.NumberField.Units.unitHeightLowerBound (d : ℕ) : ℝ

The explicit relative logarithmic height gap obtained by counting bounded powers.

theorem TauCeti.NumberField.Units.unitHeightLowerBound_def (d : ℕ) : unitHeightLowerBound d = Real.log 2 / (↑(unitPowerCountBound d) + 1)

The formula for the relative logarithmic unit-height gap.

theorem TauCeti.NumberField.Units.unitHeightLowerBound_pos (d : ℕ) : 0 < unitHeightLowerBound d

The explicit unit height bound is strictly positive in every degree.

theorem TauCeti.NumberField.Units.unitHeightLowerBound_le_logHeight₁_of_isIntegral {K : Type u_1} [Field K] [NumberField K] {x : K} (hx : IsIntegral ℤ x) (hx0 : x ≠ 0) (hxord : ¬IsOfFinOrder x) : unitHeightLowerBound (Module.finrank ℚ K) ≤ Height.logHeight₁ x

Explicit height gap for algebraic integers. A nonzero algebraic integer of infinite multiplicative order has relative logarithmic height at least the explicit bounded-power constant. The nonzero hypothesis is necessary because zero has height zero.

theorem TauCeti.NumberField.Units.unitHeightLowerBound_le_logHeight₁ {K : Type u_1} [Field K] [NumberField K] {u : (NumberField.RingOfIntegers K)ˣ} (hu : u ∉ NumberField.Units.torsion K) : unitHeightLowerBound (Module.finrank ℚ K) ≤ Height.logHeight₁ ((algebraMap (NumberField.RingOfIntegers K) K) ↑u)

Explicit unit height gap. Every nontorsion unit of a degree-d number field has relative logarithmic height at least log 2 / (unitPowerCountBound d + 1).