`alpha`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.Alpha on GitHub at line 38.

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

used by

formal source

  35@[simp] def alphaInv : ℝ := alpha_seed * Real.exp (-(f_gap / alpha_seed))
  36
  37/-- Fine-structure constant (α_EM). -/
  38@[simp] def alpha : ℝ := 1 / alphaInv
  39
  40/-! ### Numeric Verification
  41
  42The derived constants in this module are **symbolic formulas**. Any numeric
  43evaluation/match-to-CODATA checks are quarantined in
  44`IndisputableMonolith/Constants/AlphaNumericsScaffold.lean` so they cannot be
  45accidentally pulled into the certified surface.
  46-/
  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.