IndisputableMonolith.Constants.FineStructureConstant

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Foundation.PhiForcing
   4
   5/-!
   6# α_lock: the ILG kernel exponent (NOT the fine-structure constant)
   7
   8HONEST STATUS (2026-07-06): despite this module's historical name,
   9`alphaLock = (1 − 1/φ)/2 ≈ 0.19` is the information-limited-gravity
  10kernel exponent. It is NOT the electromagnetic fine-structure constant
  11α ≈ 1/137 ≈ 0.0073, and no "ledger-to-lab conversion" connecting the two
  12exists in this repository. The former claim that it resolves
  13"C-001: What determines α?" is RETRACTED.
  14
  15The honest position on the EM α is in `Constants.AlphaGenesis`: the exact
  16value of α⁻¹(0) is a free boundary datum within RS
  17(`KappaGammaIrreducibility`), and the first-order construction value is
  18excluded by measurement (`MeasurementVerdict`).
  19-/
  20
  21namespace IndisputableMonolith
  22namespace Constants
  23namespace FineStructureConstant
  24
  25open Real Constants
  26
  27/-! ## Definition and Basic Facts -/
  28
  29/-- α_lock > 0 (re-export from Constants). -/
  30theorem alphaLock_pos : 0 < alphaLock := Constants.alphaLock_pos
  31
  32/-- α_lock < 1 (re-export from Constants). -/
  33theorem alphaLock_lt_one : alphaLock < 1 := Constants.alphaLock_lt_one
  34
  35/-- α_lock lies in the open unit interval. -/
  36theorem alphaLock_in_unit_interval : 0 < alphaLock ∧ alphaLock < 1 :=
  37  ⟨alphaLock_pos, alphaLock_lt_one⟩
  38
  39/-! ## Numerical Bounds -/
  40
  41/-- α_lock is between 0.18 and 0.21 (coarse bound from φ ∈ (1.61, 1.62)). -/
  42theorem alphaLock_numerical_bounds :
  43    (0.18 : ℝ) < alphaLock ∧ alphaLock < (0.21 : ℝ) := by
  44  unfold alphaLock
  45  have h_phi := phi_gt_onePointSixOne
  46  have h_phi' := phi_lt_onePointSixTwo
  47  constructor
  48  · have h_inv : 1 / phi < 1 / 1.61 := by
  49      rw [div_lt_div_iff_of_pos_left (by norm_num) phi_pos (by norm_num)]
  50      exact h_phi
  51    linarith
  52  · have h_inv : 1 / 1.62 < 1 / phi := by
  53      rw [div_lt_div_iff_of_pos_left (by norm_num) (by norm_num) phi_pos]
  54      exact h_phi'
  55    linarith
  56
  57/-! ## Structure statement (formerly mislabeled "C-001 Resolution") -/
  58
  59/-- α_lock structure: `alphaLock = (1 − 1/φ)/2` with unit-interval bounds.
  60    This is a φ-structural fact about the ILG kernel exponent. It does NOT
  61    determine the EM fine-structure constant; see the module header. -/
  62theorem alphaLock_structure :
  63    0 < alphaLock ∧ alphaLock < 1 ∧
  64    alphaLock = (1 - 1 / phi) / 2 :=
  65  ⟨alphaLock_pos, alphaLock_lt_one, rfl⟩
  66
  67@[deprecated alphaLock_structure (since := "2026-07-06")]
  68alias fine_structure_derived := alphaLock_structure
  69
  70end FineStructureConstant
  71end Constants
  72end IndisputableMonolith
  73