Kronecker's theorem for projective tuples and the height gap

Kronecker's criterion NumberField.absMulHeight₁_eq_one_iff says that an algebraic number has absolute height one exactly when it is zero or a root of unity. This file proves its projective form and the quantitative consequence at bounded degree.

• Projective Kronecker. A tuple x with algebraic coordinates has absolute projective height one exactly when every ratio x i / x j with x j ≠ 0 is zero or a root of unity. For a tuple of zeros and roots of unity, a common exponent N makes x ^ N a tuple of zeros and ones; such a tuple is its own square, so its height is an idempotent real number at least one.
• The height gap. An algebraic number that is neither zero nor a root of unity has absolute height strictly above one (NumberField.one_lt_absMulHeight₁). Among such numbers of degree at most D the absolute logarithmic height is bounded below by a positive constant depending on D. The constant is ineffective: it is the minimum over the finitely many such numbers of absolute height at most 2, which bounded-degree Northcott (TauCeti.finite_setOf_absMulHeight₁_le) provides.
• The degree dependence is essential. The real numbers 2 ^ (1 / N) are algebraic, not roots of unity, and have absolute logarithmic height log 2 / N, so no positive lower bound holds uniformly in the degree.

Main results

• TauCeti.absoluteProjectiveTupleHeight_eq_one_iff: projective Kronecker.
• TauCeti.absoluteProjectiveTupleHeight_eq_one_of_forall_eq_zero_or_isOfFinOrder: a tuple of zeros and roots of unity has absolute height one.
• TauCeti.exists_pos_forall_le_absLogHeight₁: the height gap at bounded degree.
• TauCeti.exists_absLogHeight₁_lt: without a degree bound there is no gap.

References

• E. Bombieri and W. Gubler, Heights in Diophantine Geometry (2006), Theorem 1.5.9 and Corollary 1.6.15.
• M. Hindry and J. H. Silverman, Diophantine Geometry: An Introduction (2000), Theorem B.2.3 and Corollary B.2.3.1.
• A prior formalization of these results is Ralf Stephan's ArithmeticHeights/Kronecker.lean and ArithmeticHeights/LowerBound.lean in rwst/Subspace-Theorems, commit e443c2479e19f7665b31d8e94e2317c8ced1ca06 (Apache 2.0).

theorem TauCeti.absoluteProjectiveTupleHeight_eq_one_of_forall_eq_zero_or_isOfFinOrder {F : Type u_1} [Field F] [CharZero F] {ι : Type u_2} [Finite ι] {x : ι → F} (hx : ∀ (i : ι), x i = 0 ∨ IsOfFinOrder (x i)) : absoluteProjectiveTupleHeight x = 1

A tuple whose coordinates are each zero or of finite multiplicative order has absolute projective height one.

theorem TauCeti.absoluteProjectiveTupleHeight_eq_one_iff {F : Type u_1} [Field F] [CharZero F] {ι : Type u_2} [Finite ι] {x : ι → F} (hx : ∀ (i : ι), IsAlgebraic ℚ (x i)) : absoluteProjectiveTupleHeight x = 1 ↔ ∀ (i j : ι), x j ≠ 0 → x i = 0 ∨ IsOfFinOrder (x i / x j)

Kronecker's theorem for projective tuples. A tuple with algebraic coordinates has absolute projective height one if and only if, for every nonzero coordinate x j, each ratio x i / x j is zero or of finite multiplicative order. This includes the zero tuple.

theorem TauCeti.exists_pos_forall_le_absLogHeight₁ (F : Type u_1) [Field F] [CharZero F] (D : ℕ) : ∃ c > 0, ∀ (x : F), IsIntegral ℚ x → x ≠ 0 → ¬IsOfFinOrder x → Module.finrank ℚ ↥ℚ⟮x⟯ ≤ D → c ≤ NumberField.absLogHeight₁ x

The height gap at bounded degree. For every D there is c > 0 such that every algebraic number of degree at most D that is neither zero nor of finite multiplicative order has absolute logarithmic height at least c. The constant is ineffective.

theorem TauCeti.absLogHeight₁_two_rpow_inv (N : ℕ) : NumberField.absLogHeight₁ (2 ^ (↑N)⁻¹) = Real.log 2 / ↑N

The real number 2 ^ (1 / N) has absolute logarithmic height log 2 / N. For N = 0 both sides are 0.

theorem TauCeti.exists_absLogHeight₁_lt {c : ℝ} (hc : 0 < c) : ∃ (x : ℝ), IsIntegral ℚ x ∧ x ≠ 0 ∧ ¬IsOfFinOrder x ∧ NumberField.absLogHeight₁ x < c

No gap without a degree bound. For every c > 0 some algebraic number that is neither zero nor of finite multiplicative order has absolute logarithmic height below c: one may take 2 ^ (1 / N) for N large.