alpha_gravity
plain-language theorem explainer
The declaration defines the RS-derived dynamical-time exponent as one minus the reciprocal of the golden ratio. Galactic dynamics researchers cite it when matching rotation-curve data or deriving the steepness parameter p from first principles. The definition is introduced directly as an abbreviation that satisfies the algebraic relation to twice the lock parameter.
Claim. $α_{gravity} := 1 - φ^{-1}$, where $φ$ denotes the golden ratio arising as the self-similar fixed point.
background
The GravityParameters module derives seven galactic gravity parameters from the golden ratio $φ$. It classifies each parameter by status: derived (mathematically proven from $φ$), has RS basis, or phenomenological. The table lists $α$ as DERIVED with formula $1 - 1/φ$ and 1.8 percent match to the fitted value 0.389 ± 0.015. Upstream, $φ$ is supplied by the Constants module together with the lemmas one_lt_phi and phi_pos that establish its ordering and positivity.
proof idea
Direct definition as the arithmetic expression 1 - 1/φ. Downstream theorems unfold the definition, then apply the ring tactic to obtain equality with 2 · alphaLock and invoke the ordering lemmas on $φ$ to obtain strict positivity.
why it matters
The definition supplies the concrete value for the dynamical-time exponent that is invoked by the equality theorem alpha_gravity_eq_two_alphaLock and the positivity theorem alpha_gravity_pos. It realizes the RS prediction for the first entry in the seven-parameter table, linking directly to the phi-ladder and the eight-tick octave. It closes the derivation step for galactic parameters from the forcing chain, leaving open the question of whether tighter observational bounds can reduce the current 1.8 percent discrepancy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.