rar_slope_rs_value
plain-language theorem explainer
The declaration proves that the RS-derived RAR slope equals 1 minus (1 minus 1 over phi) over 4. Galaxy dynamics modelers would cite it to fix the power-law exponent in the ILG-derived RAR to the Recognition Science value. The proof is a direct algebraic reduction that unfolds the definitions of rar_slope_rs and alphaLock then normalizes via ring.
Claim. The RS-derived RAR slope satisfies $1 - (1 - 1/phi)/4$, where the slope is obtained from the locked exponent via $1 - alphaLock/2$ and $alphaLock = (1 - 1/phi)/2$.
background
The RAREmergence module shows that the empirical RAR $a_obs = f(a_baryon)$ emerges from the ILG weight $w(r) proportional to (a0 / a_baryon)^{alpha/2}$, producing the power-law form with exponent 1 - alpha/2. The upstream definition rar_slope_rs sets this exponent to 1 - alphaLock/2. The constant alphaLock is the canonical locked value (1 - 1/phi)/2, which encodes the RS parameter lock on the dynamical-time exponent.
proof idea
The proof is a one-line term-mode reduction. It unfolds rar_slope_rs to expose alphaLock/2, unfolds alphaLock to insert the explicit form (1 - 1/phi)/2, and applies the ring tactic to simplify the resulting rational expression to the target 1 - (1 - 1/phi)/4.
why it matters
This supplies the concrete phi-derived numerical value for the RAR slope in the module's main power-law result, where the exponent is stated as approximately 0.8. It closes the algebraic step between the general ILG form and the specific RS parameter lock, connecting the gravity module to the phi fixed point from the forcing chain. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.