Northcott's property for the rational logarithmic height

The logarithmic height of a rational number is the logarithm of the maximum of the absolute value of its normalized numerator and its positive denominator. Consequently, a height bound places the numerator and denominator in finite integer intervals. This file records that elementary rational specialization of Northcott's theorem.

theorem MazurTorsion.finite_rat_logHeight₁_le (B : ℝ) : {q : ℚ | Height.logHeight₁ q ≤ B}.Finite

The rational numbers of logarithmic height at most B form a finite set.

instance MazurTorsion.rationalLogHeightNorthcott : Northcott Height.logHeight₁

The usual logarithmic height on ℚ has Northcott's property.