`alpha_components_derived`

proved

show as: view math explainer →

module: IndisputableMonolith.Constants.Alpha
domain: Constants
line: 50 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.Alpha on GitHub at line 50.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

Derivations using this theorem

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

formal source

  47
  48/-! ### Provenance Witnesses -/
  49
  50lemma alpha_components_derived :
  51    (∃ (seed gap : ℝ),
  52      alphaInv = seed * Real.exp (-(gap / seed)) ∧
  53      seed = alpha_seed ∧
  54      gap = f_gap) := by
  55  refine ⟨alpha_seed, f_gap, ?_⟩
  56  simp
  57
  58end
  59
  60end Constants
  61end IndisputableMonolith

papers checked against this theorem

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