A candidate in $\overline{\mathbb{Q}} + \overline{\mathbb{Q}}\ell$ is a rational multiple of $\ell$ ; no candidate is $a + b\pi$ ; unconditionally

Proved

DiazModulus.candidate_one_log_saturation_unconditional

by carlok · Oct 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

diaz-modulus-leannumber-theorytranscendence

Let $u$ be a candidate: $u \neq 0$ with $|u|$ and $e^{u}$ algebraic. If $u = a + b\ell$ with $a, b$ algebraic and $\ell$ a logarithm of an algebraic number, then $u = r\ell$ for some $r \in \mathbb{Q}$ ; and $u \neq a + b\pi$ for all algebraic $a, b$ .

This is DiazModulus.candidate_one_log_saturation with both of its hypotheses discharged: Baker's theorem for two logarithms by DiazModulus.baker_two_logs, proved in this mission following Chapter 4 of Waldschmidt's book, and Hermite–Lindemann by DiazModulus.hermite_lindemann_holds.

Proof. DiazModulus.candidate_one_log_saturation DiazModulus.baker_two_logs DiazModulus.hermite_lindemann_holds.

Novelty. Nothing beyond the parent node; its page gives the argument and the attribution.

Preamble

import Definitions.Def_DiazModulus

Formal statement

namespace DiazModulus

theorem candidate_one_log_saturation_unconditional {u : ℂ} (h : IsCandidate u) :
    (∀ l : ℂ, l ∈ LogAlg → ∀ a b : ℂ, a ∈ Qbar → b ∈ Qbar →
        u = a + b * l → ∃ r : ℚ, u = (r : ℂ) * l)
      ∧ (∀ a b : ℂ, a ∈ Qbar → b ∈ Qbar → u ≠ a + b * ((Real.pi : ℝ) : ℂ)) := by
  sorry

end DiazModulus

Source

The statement and argument of `DiazModulus.candidate_one_log_saturation` (C. Perassi's working notes of 12 September 2026), with Baker's theorem (A. Baker, Linear forms in the logarithms of algebraic numbers I, Mathematika 13 (1966), 204–216) proved in this mission as `DiazModulus.baker_two_logs`. Formal proof: Diaz modulus mission, 2 October 2026 (C. Perassi).

View graph

A candidate in Q‾+Q‾ℓ\overline{\mathbb{Q}} + \overline{\mathbb{Q}}\ellQ​+Q​ℓ is a rational multiple of ℓ\ellℓ; no candidate is a+bπa + b\pia+bπ; unconditionally

A candidate in $\overline{\mathbb{Q}} + \overline{\mathbb{Q}}\ell$ is a rational multiple of $\ell$ ; no candidate is $a + b\pi$ ; unconditionally