alphaLock_in_unit_interval

formal source

  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/-! ## C-001 Resolution Statement -/
  58
  59/-- **C-001 Resolution**: The fine structure constant is determined by φ.
  60
  61    α_lock = (1 − 1/φ)/2 has no free parameters.
  62    It is the unique coupling compatible with the ledger's
  63    reciprocal symmetry and self-similar closure.
  64
  65    Relationship to measured α ≈ 1/137 requires the conversion
  66    from RS-native to SI units (λ_rec calibration). -/