  93
  94/-- The RS-based morphology coupling coefficient.
  95    C_ξ = 2 · φ⁻⁴ ≈ 0.292 -/
  96def C_xi : ℝ := 2 * phi ^ (-(4 : ℝ))
  97
  98/-- C_ξ is positive.
  99    Paper fitted value: 0.298 ± 0.015
 100    RS prediction: 2/φ⁴ ≈ 0.292
 101    Match: 2% -/
 102theorem C_xi_pos : 0 < C_xi := by
 103  unfold C_xi
 104  have hphi_pos := phi_pos
 105  apply mul_pos (by norm_num : (0:ℝ) < 2)
 106  exact Real.rpow_pos_of_pos hphi_pos _
 107
 108/-! ## 4. p (Spatial Profile Steepness) — HAS RS BASIS
 109
 110The steepness exponent is 1 - αLock/4.
 111
 112**Physical motivation:** The transition steepness differs from 1 by a quarter
 113of the fine-structure exponent, linking spatial structure to α. -/
 114
 115/-- The RS-based spatial profile steepness.
 116    p = 1 - αLock/4 = 1 - (1 - 1/φ)/8 ≈ 0.952 -/
 117def p_steepness : ℝ := 1 - alphaLock / 4
 118
 119theorem p_steepness_eq : p_steepness = 1 - (1 - 1/phi) / 8 := by
 120  unfold p_steepness alphaLock
 121  ring
 122
 123/-- p is between 0 and 1.
 124    Paper fitted value: 0.95 ± 0.02
 125    RS prediction: 1 - αLock/4 ≈ 0.952
 126    Match: 0.2% -/

papers checked against this theorem

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