A common denominator with a house bound for all monomials of bounded degree

Proved

Transcendence.exists_denom_house_monomial_le

by carlok · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

diaz-modulus-leannumber-theorytranscendence

Let $K$ be a number field and let $\theta_i \in K$ ( $i$ in a finite type). There are a non-zero algebraic integer $b \in K$ and a real $H \ge 1$ such that for every exponent vector $e$ and every $E$ with $\sum_i e_i \le E$ , the number

b^{E} \prod_i \theta_i^{e_i}

is an algebraic integer whose house (the largest absolute value of its conjugates, Mathlib's NumberField.house) is at most $H^{E}$ .

One non-zero integer $b$ clears the denominators of all the $\theta_i$ , and $H = 1 + \overline{|b|} + \sum_i \overline{|b\theta_i|}$ works, since the house is submultiplicative.

Preamble

import Mathlib

Formal statement

open NumberField

namespace Transcendence

theorem exists_denom_house_monomial_le {K ι : Type*} [Field K] [NumberField K] [Fintype ι]
    (θ : ι → K) : ∃ b : K, b ≠ 0 ∧ IsIntegral ℤ b ∧ ∃ H : ℝ, 1 ≤ H ∧ ∀ (e : ι → ℕ) (E : ℕ),
      ∑ i, e i ≤ E → IsIntegral ℤ (b ^ E * ∏ i, θ i ^ e i) ∧ house (b ^ E * ∏ i, θ i ^ e i) ≤ H ^ E := by
  sorry

end Transcendence

Source

Standard. Formal proof: Diaz modulus mission, 27 September 2026 (C. Perassi).

View graph