Problem10_53.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

4 declarations, 4 contain sorry, 0 declared as axioms

Bugeaud Collection of Conjectures and Open Questions: Simultaneously Small Entropies

A real number can be described by its continued fraction expansion and by its expansion in an integer base. Problem 10.53 asks for an irrational number for which both descriptions have small block complexity. Temur [Tem26] answered it, in the stronger form that asks for every base at once, by an explicit construction.

References:

[Bug12] Bugeaud, Yann. "Distribution modulo one and Diophantine approximation." Vol. 193. Cambridge University Press, 2012. Chapter 10.
Tem26 Temur, Faruk. "Simultaneously small continued fraction entropy and base $b$ entropy." arXiv preprint arXiv:2609.16362 (2026).
[BBFKW10] Broderick, Ryan, Yann Bugeaud, Lior Fishman, Dmitry Kleinbock, and Barak Weiss. "Schmidt's game, fractals, and numbers normal to no base." Mathematical Research Letters 17.2 (2010): 307-321.

Imports (1)

FormalConjecturesUtil

theorem Bugeaud53.problem_10_53 Problem 10.53 sorry line 50 source
Source documentation
Problem 10.53. There is an irrational real number $\xi$ such that $E(\xi) < \log 2$ and $E(\xi, b) < \log b$ for some integer $b \ge 2$. Answered by Temur [Tem26].

depends on sorry what this means
Statement uses: Exists, Real, And, Irrational, LT.lt, EReal, Real.cfEntropy, Real.log, OfNat.ofNat, Nat, LE.le, Real.baseEntropy
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem problem_10_53 :
    ∃ ξ : ℝ, Irrational ξ ∧ cfEntropy ξ < (Real.log 2 : EReal) ∧
      ∃ b : ℕ, 2 ≤ b ∧ baseEntropy b ξ < (Real.log b : EReal) := by
…
```
theorem Bugeaud53.problem_10_53.variants.all_bases Problem 10.53, in the stronger form that asks for every base at once: there is an irrational real number sorry line 61 source
Source documentation
Problem 10.53, in the stronger form that asks for every base at once: there is an irrational real number $\xi$ such that $E(\xi) < \log 2$ and $E(\xi, b) < \log b$ for every integer $b \ge 2$. Answered by Temur [Tem26].

depends on sorry what this means
Statement uses: Exists, Real, And, Irrational, LT.lt, EReal, Real.cfEntropy, Real.log, OfNat.ofNat, Nat, LE.le, Real.baseEntropy
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem problem_10_53.variants.all_bases :
    ∃ ξ : ℝ, Irrational ξ ∧ cfEntropy ξ < (Real.log 2 : EReal) ∧
      ∀ b : ℕ, 2 ≤ b → baseEntropy b ξ < (Real.log b : EReal) := by
…
```
theorem Bugeaud53.problem_10_53.variants.uncountable There are uncountably many numbers as in Problem 10.53 sorry line 72 source
Source documentation
There are uncountably many numbers as in Problem 10.53. This follows from a result of Broderick, Bugeaud, Fishman, Kleinbock and Weiss [BBFKW10] applied to the Gauss-Cantor set $\{[0; 1, a_1, 1, a_2, \ldots] : a_j \in \{1, 2\}\}$, as observed in [Tem26].

depends on sorry what this means
Statement uses: Not, Set.Countable, Real, Set.ofPred, And, Irrational, LT.lt, EReal, Real.cfEntropy, Real.log, OfNat.ofNat, Nat, LE.le, Real.baseEntropy
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem problem_10_53.variants.uncountable :
    ¬ {ξ : ℝ | Irrational ξ ∧ cfEntropy ξ < (Real.log 2 : EReal) ∧
      ∀ b : ℕ, 2 ≤ b → baseEntropy b ξ < (Real.log b : EReal)}.Countable := by
…
```
theorem Bugeaud53.problem_10_53.variants.temur Temur [Tem26], Theorem 1 sorry line 87 source
Source documentation
Temur [Tem26], Theorem 1. There is an irrational $\xi \in (0, 1)$ all of whose partial quotients are $1$ or $2$, such that $$\lVert b^k \xi \rVert > 154^{-2^b} \quad (b \ge 2,\ k \ge 0),$$ where $\lVert \cdot \rVert$ denotes the distance to the nearest integer. The bound on the partial quotients gives $E(\xi) \le (\log 2) / 4$, and the displayed inequality forces the base $b$ expansion of $\xi$ to omit a block of zeros, which gives $E(\xi, b) < \log b$ for every $b \ge 2$. Temur's $\xi$ is moreover computable.

depends on sorry what this means
Statement uses: Exists, Real, And, Irrational, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Nat, Or, Eq, Real.partQuot, LE.le, LT.lt, HPow.hPow, Int, Neg.neg, distToNearestInt, HMul.hMul, EReal and 4 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
66 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem problem_10_53.variants.temur :
    ∃ ξ : ℝ, Irrational ξ ∧ ξ ∈ Set.Ioo (0 : ℝ) 1 ∧
      (∀ n : ℕ, partQuot ξ n = 1 ∨ partQuot ξ n = 2) ∧
      (∀ b : ℕ, 2 ≤ b → ∀ k : ℕ,
        (154 : ℝ) ^ (-(2 ^ b) : ℤ) < distToNearestInt ((b : ℝ) ^ k * ξ)) ∧
      cfEntropy ξ ≤ ((Real.log 2 / 4 : ℝ) : EReal) ∧
      ∀ b : ℕ, 2 ≤ b → baseEntropy b ξ < (Real.log b : EReal) := by
…
```
Mentions: distToNearestInt