recognition / Numerics / Numerics.Interval.AlphaBounds / alphaInv_lt_strong

theorem

`alphaInv_lt_strong`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

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

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

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

depends on

formal source

 362
 363/-- Upper bound alias retained for backwards compatibility after the canonical
 364exponential α update. -/
 365theorem alphaInv_lt_strong : alphaInv < (137.039 : ℝ) := by
 366  exact alphaInv_lt
 367
 368end IndisputableMonolith.Numerics

papers checked against this theorem

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