alpha_gravity_eq_two_alphaLock
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 in Recognition Science
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.
scope and limits
- Does not derive α_gravity from the forcing chain T0-T8.
- Does not address numerical agreement with observations beyond the module comment.
- Does not extend to sibling parameters such as upsilon_star or p_steepness.
- Does not invoke the spin value definition despite the QFT import.
formal statement (Lean)
51theorem alpha_gravity_eq_two_alphaLock : alpha_gravity = 2 * alphaLock := by
proof body
Term-mode proof.
52 unfold alpha_gravity alphaLock
53 ring
54
55/-- Paper fitted value: 0.389 ± 0.015
56 RS prediction: 1 - 1/φ ≈ 0.382
57 Match: 1.8% -/