pith. machine review for the scientific record. sign in
theorem proved term proof

p_steepness_pos

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 127theorem p_steepness_pos : 0 < p_steepness ∧ p_steepness < 1 := by

proof body

Term-mode proof.

 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 -/

depends on (19)

Lean names referenced from this declaration's body.