p_steepness_pos
plain-language theorem explainer
The theorem proves that the galactic rotation curve steepness parameter p satisfies 0 < p < 1. Galaxy dynamics modelers would cite this bound when adopting the Recognition Science form p = 1 - αLock/4 for rotation curve fits. The short proof unfolds the definition of p_steepness and applies linear arithmetic to the established positivity and upper bound of αLock.
Claim. $0 < p < 1$ where $p = 1 - α_{lock}/4$ and $α_{lock}$ satisfies $0 < α_{lock} < 1$.
background
GravityParameters derives seven galactic gravity parameters from the φ framework. The steepness p is listed under HAS RS BASIS with explicit formula 1 - αLock/4, where αLock is the fine-structure constant locked to φ via αLock = 1 - 1/φ. The module states that p matches the paper-fitted value 0.95 ± 0.02 to 0.2% accuracy. Upstream lemmas alphaLock_pos and alphaLock_lt_one establish the open interval for αLock from the positivity of φ and the inequality 1/φ < 1.
proof idea
The term-mode proof unfolds p_steepness, obtains the two lemmas alphaLock_pos and alphaLock_lt_one, then uses constructor followed by linarith on both sides of the conjunction.
why it matters
This theorem closes the interval bounds for p inside the GravityParameters module, which supplies the RS-derived steepness for galactic modeling. It directly supports the 0.2% match between the RS prediction 1 - αLock/4 ≈ 0.952 and the empirical fit. The result sits downstream of the alphaLock bounds in Constants and aligns with the module's classification of p as having an RS basis linked to the fine-structure constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.