`alphaInv_def`

proved

show as: view math explainer →

module: IndisputableMonolith.Constants.AlphaExponentialForm
domain: Constants
line: 57 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Constants.AlphaExponentialForm on GitHub at line 57.

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

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

exponential_form_uniqueness_ode_principle IndisputableMonolith.Constants.AlphaExponentialForm

formal source

  54/-! ## Part 1: Basic Properties of the Exponential Form -/
  55
  56/-- The alphaInv formula unfolds to the exponential expression. -/
  57theorem alphaInv_def : alphaInv = alpha_seed * Real.exp (-(f_gap / alpha_seed)) := rfl
  58
  59/-- The seed is positive: α_seed = 4π·11 > 0. -/
  60theorem alpha_seed_positive : 0 < alpha_seed := by
  61  unfold alpha_seed
  62  have hpi : 0 < Real.pi := Real.pi_pos
  63  linarith
  64
  65/-- The exponential formula produces a positive value. -/
  66theorem alphaInv_positive : 0 < alphaInv := by
  67  unfold alphaInv
  68  exact mul_pos alpha_seed_positive (Real.exp_pos _)
  69
  70/-- The exponential factor is in (0, 1] since f_gap ≥ 0 (assuming w₈ > 0). -/
  71theorem exp_factor_bounded (hfg : 0 ≤ f_gap) :
  72    0 < Real.exp (-(f_gap / alpha_seed)) ∧ Real.exp (-(f_gap / alpha_seed)) ≤ 1 := by
  73  constructor
  74  · exact Real.exp_pos _
  75  · apply Real.exp_le_one_iff.mpr
  76    apply neg_nonpos_of_nonneg
  77    exact div_nonneg hfg (le_of_lt alpha_seed_positive)
  78
  79/-- The ratio alphaInv/alpha_seed equals the exponential factor. -/
  80theorem alphaInv_seed_ratio :
  81    alphaInv / alpha_seed = Real.exp (-(f_gap / alpha_seed)) := by
  82  unfold alphaInv
  83  field_simp
  84
  85/-! ## Part 2: The Logarithmic Structure
  86
  87Taking the natural log of α⁻¹/α_seed gives:

papers checked against this theorem

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