`alphaInv_gt`

proved

show as: view math explainer →

module: IndisputableMonolith.Numerics.Interval.AlphaBounds
domain: Numerics
line: 307 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Numerics.Interval.AlphaBounds on GitHub at line 307.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

Derivations using this theorem

Precision Band for the Fine-Structure Constant · derived / THEOREM
Lean-certified upper and lower bounds on alpha^{-1} place CODATA inside
The Fine-Structure Constant · foundational / THEOREM
α⁻¹ = 4π·11·exp(−w₈·ln(φ)/(4π·11)) is forced from J-cost uniqueness, φ self-similarity, and D=3; the certified band (137.030, 137.039) contains CODATA 137.036

depends on

used by

formal source

 304
 305/-! ## alphaInv bounds -/
 306
 307theorem alphaInv_gt : (137.030 : ℝ) < alphaInv := by
 308  simp only [alphaInv]
 309  have hseed_pos : (0 : ℝ) < alpha_seed := lt_trans (by norm_num) alpha_seed_gt
 310  have hy_hi : f_gap / alpha_seed < (0.00871 : ℝ) := by
 311    have hmul : f_gap < (0.00871 : ℝ) * alpha_seed := by
 312      have h1 : f_gap < (1.203 : ℝ) := f_gap_lt
 313      have h2 : (1.203 : ℝ) < (0.00871 : ℝ) * (138.230048 : ℝ) := by norm_num
 314      have h3 : (0.00871 : ℝ) * (138.230048 : ℝ) < (0.00871 : ℝ) * alpha_seed := by
 315        exact mul_lt_mul_of_pos_left alpha_seed_gt (by norm_num)
 316      exact lt_trans h1 (lt_trans h2 h3)
 317    exact (div_lt_iff₀ hseed_pos).2 (by simpa [mul_comm, mul_left_comm, mul_assoc] using hmul)
 318  have hexp_lo : ((991327 / 1000000 : ℚ) : ℝ) < Real.exp (-(f_gap / alpha_seed)) := by
 319    have hmono : Real.exp (-(0.00871 : ℝ)) < Real.exp (-(f_gap / alpha_seed)) := by
 320      exact Real.exp_lt_exp.mpr (by linarith [hy_hi])
 321    exact lt_trans exp_neg_00871_gt hmono
 322  have hseed_mul :
 323      (138.230048 : ℝ) * (((991327 / 1000000 : ℚ) : ℝ)) <
 324        alpha_seed * (((991327 / 1000000 : ℚ) : ℝ)) := by
 325    exact mul_lt_mul_of_pos_right alpha_seed_gt (by norm_num)
 326  have hmul :
 327      alpha_seed * (((991327 / 1000000 : ℚ) : ℝ)) <
 328        alpha_seed * Real.exp (-(f_gap / alpha_seed)) := by
 329    exact mul_lt_mul_of_pos_left hexp_lo hseed_pos
 330  calc
 331    (137.030 : ℝ) < (138.230048 : ℝ) * (((991327 / 1000000 : ℚ) : ℝ) : ℝ) := by norm_num
 332    _ < alpha_seed * (((991327 / 1000000 : ℚ) : ℝ) : ℝ) := hseed_mul
 333    _ < alpha_seed * Real.exp (-(f_gap / alpha_seed)) := hmul
 334
 335theorem alphaInv_lt : alphaInv < (137.039 : ℝ) := by
 336  simp only [alphaInv]
 337  have hseed_pos : (0 : ℝ) < alpha_seed := lt_trans (by norm_num) alpha_seed_gt

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.