p_steepness_eq
plain-language theorem explainer
The equality fixes the galactic gravity steepness parameter at one minus one-eighth of one minus the reciprocal of phi. Researchers fitting rotation curves within Recognition Science cite the identity to anchor the phenomenological p directly to the golden ratio. The proof reduces to unfolding the definitions of p_steepness and alphaLock then invoking ring for algebraic cancellation.
Claim. $p = 1 - (1 - 1/φ)/8$, where $p$ is the RS-based spatial profile steepness and $φ$ denotes the golden ratio.
background
The GravityParameters module derives seven galactic gravity parameters from Recognition Science. Three are fully derived from φ, three carry an RS basis with observational match, and the rest remain phenomenological. The parameter p belongs to the middle class with the explicit RS formula 1 − αLock/4. alphaLock itself is defined in Constants as (1 − 1/φ)/2, the locked fine-structure constant. The local setting is therefore purely algebraic once the two definitions are fixed; no additional physical axioms enter the statement.
proof idea
The term proof first unfolds p_steepness to 1 − alphaLock/4 and alphaLock to (1 − 1/φ)/2. The ring tactic then performs the arithmetic reduction, replacing alphaLock/4 by (1 − 1/φ)/8 and yielding the target right-hand side.
why it matters
The identity supplies the explicit RS prediction for p listed in the module table (1 − αLock/4 ≈ 0.952) and records the 0.2 % match to the fitted value 0.95 ± 0.02. It therefore closes the algebraic step that lets the gravity-parameter table claim an RS basis for p. The result sits inside the broader program of extracting galactic phenomenology from the forcing chain (T5–T8) without introducing new constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.