`alpha_seed`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.Alpha on GitHub at line 25.

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

  22
  23/-- Geometric seed from ledger structure: `4π·11`.
  24    Represents the baseline spherical closure cost over 11-edge interaction paths. -/
  25@[simp] def alpha_seed : ℝ := 4 * Real.pi * 11
  26
  27/-- Legacy curvature correction (voxel seam count).
  28    Retained for compatibility with older reports, but no longer used in
  29    the canonical certified `alphaInv` pipeline. -/
  30@[simp] def delta_kappa : ℝ := -(103 : ℝ) / (102 * Real.pi ^ 5)
  31
  32/-- Dimensionless inverse fine-structure constant (canonical exponential resummation).
  33    This value (~137.036) is derived from the structural seed and gap with zero
  34    adjustable parameters. -/
  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, ?_⟩

papers checked against this theorem

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