IndisputableMonolith.Constants.Alpha

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Constants.GapWeight
   4
   5namespace IndisputableMonolith
   6namespace Constants
   7
   8noncomputable section
   9
  10/-! ### Electromagnetic Fine-Structure Constant (α_EM) Derivation
  11
  12Derivation of the fine-structure constant from geometric and recognition primitives.
  13
  14Canonical formula: α⁻¹ = (4π·11) · exp(−(w8·ln φ)/(4π·11))
  15
  16where:
  17* `4π·11` is the geometric seed (spherical closure over 11-edge paths).
  18* `w8·ln(φ)` is the information gap cost (8-tick weight × self-similar scaling).
  19This keeps the seed and gap terms as fully structural inputs while removing the
  20legacy additive correction from the certified pipeline.
  21-/
  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, ?_⟩
  56  simp
  57
  58end
  59
  60end Constants
  61end IndisputableMonolith
  62