 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% -/
 127theorem p_steepness_pos : 0 < p_steepness ∧ p_steepness < 1 := by
 128  unfold p_steepness
 129  have ha := alphaLock_pos
 130  have hb := alphaLock_lt_one
 131  constructor <;> linarith
 132
 133/-! ## 5. A (Spatial Profile Amplitude) — HAS RS BASIS
 134
 135The amplitude is 1 + αLock/2.
 136
 137**Physical motivation:** The outer enhancement is 1 plus half the fine-structure
 138exponent, linking spatial structure amplitude to α. -/
 139
 140/-- The RS-based spatial profile amplitude.
 141    A = 1 + αLock/2 = 1 + (1 - 1/φ)/4 ≈ 1.096 -/
 142def A_amplitude : ℝ := 1 + alphaLock / 2
 143
 144theorem A_amplitude_eq : A_amplitude = 1 + (1 - 1/phi) / 4 := by
 145  unfold A_amplitude alphaLock
 146  ring
 147

papers checked against this theorem

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