`alphaInv_lt`

proved

show as: view math explainer →

module: IndisputableMonolith.Numerics.Interval.AlphaBounds
domain: Numerics
line: 335 · 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 335.

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

 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
 338  have hy_lo : (0.00866 : ℝ) < f_gap / alpha_seed := by
 339    have hmul : (0.00866 : ℝ) * alpha_seed < f_gap := by
 340      have h1 : (0.00866 : ℝ) * alpha_seed < (0.00866 : ℝ) * (138.230092 : ℝ) := by
 341        exact mul_lt_mul_of_pos_left alpha_seed_lt (by norm_num)
 342      have h2 : (0.00866 : ℝ) * (138.230092 : ℝ) < (1.1979 : ℝ) := by norm_num
 343      exact lt_trans h1 (lt_trans h2 f_gap_gt_strong)
 344    exact (lt_div_iff₀ hseed_pos).2 (by simpa [mul_comm, mul_left_comm, mul_assoc] using hmul)
 345  have hexp_hi : Real.exp (-(f_gap / alpha_seed)) < ((495689 / 500000 : ℚ) : ℝ) := by
 346    have hmono : Real.exp (-(f_gap / alpha_seed)) < Real.exp (-(0.00866 : ℝ)) := by
 347      exact Real.exp_lt_exp.mpr (by linarith [hy_lo])
 348    exact lt_trans hmono exp_neg_00866_lt
 349  have hmul :
 350      alpha_seed * Real.exp (-(f_gap / alpha_seed)) <
 351        alpha_seed * (((495689 / 500000 : ℚ) : ℝ)) := by
 352    exact mul_lt_mul_of_pos_left hexp_hi hseed_pos
 353  have hseed_hi :
 354      alpha_seed * (((495689 / 500000 : ℚ) : ℝ)) <
 355        (138.230092 : ℝ) * (((495689 / 500000 : ℚ) : ℝ)) := by
 356    exact mul_lt_mul_of_pos_right alpha_seed_lt (by norm_num)
 357  calc
 358    alpha_seed * Real.exp (-(f_gap / alpha_seed))
 359        < alpha_seed * (((495689 / 500000 : ℚ) : ℝ) : ℝ) := hmul
 360    _ < (138.230092 : ℝ) * (((495689 / 500000 : ℚ) : ℝ) : ℝ) := hseed_hi
 361    _ < (137.039 : ℝ) := by norm_num
 362
 363/-- Upper bound alias retained for backwards compatibility after the canonical
 364exponential α update. -/
 365theorem alphaInv_lt_strong : alphaInv < (137.039 : ℝ) := by

papers checked against this theorem

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