alpha_gravity_eq_two_alphaLock
plain-language theorem explainer
Recognition Science sets the dynamical-time exponent α_gravity equal to twice the locked fine-structure constant α_lock. Galaxy dynamics researchers cite the equality when substituting the φ-derived value into acceleration-parameterized expressions for rotation curves. The proof is a one-line algebraic reduction that unfolds the two definitions and applies the ring tactic.
Claim. $α_{gravity} = 2 α_{lock}$ where $α_{lock} = (1 - 1/φ)/2$ and $α_{gravity} = 1 - 1/φ$.
background
The GravityParameters module derives galactic gravity parameters from Recognition Science first principles. Each parameter is classified as DERIVED, HAS RS BASIS, or PHENOMENOLOGICAL, with α_gravity listed under DERIVED using the RS formula 1 - 1/φ and a 1.8% match to the fitted value 0.389 ± 0.015. The module also records the axiom a0_phi_ladder_formula as a proven theorem.
proof idea
The proof unfolds the definitions of alpha_gravity (1 - 1/φ) and alphaLock ((1 - 1/φ)/2). The ring tactic then verifies the identity directly with no further lemmas.
why it matters
This algebraic fact supplies the bridge identity for the acceleration-parameterized exponent 2·alphaLock noted in the alphaLock definition. It supports the DERIVED status of α in the module's seven-parameter table and connects the phi-ladder constants to galactic dynamics. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.