Encyclopedia Gravity Gravity Gravity Parameters Alpha Gravity Eq Two Alpha Lock
Gravity Gravity Parameters Alpha Gravity Eq Two Alpha Lock
In the Recognition Science framework, a theorem ties two galactic gravity parameters together: the dynamical-time exponent is exactly twice the locking exponent.
A doubling relation
In the Recognition Science framework, the parameter alpha_gravity (the dynamical-time exponent) is defined as 1 - 1/φ, where φ is the golden ratio. The parameter alphaLock is defined as half of that value. The theorem alpha_gravity_eq_two_alphaLock states that alpha_gravity equals 2 times alphaLock, a relation that follows directly from these definitions by algebraic simplification.
This is a statement about the framework's internal model of galactic dynamics. It does not claim that alpha_gravity is a measured quantity; it is a defined parameter. It does not claim that the relation holds for any other set of parameters. It does not claim that alphaLock has any independent physical meaning outside of this definitional context.
The theorem is a formal consequence of the framework's chosen definitions, not an empirical discovery. It establishes a consistency within the model: the two parameters are not independent but are locked together by the framework's construction. The practical effect is that any calculation using one parameter can be expressed in terms of the other, simplifying the model's internal bookkeeping.
THEOREM alpha_gravity_eq_two_alphaLock · IndisputableMonolith/Gravity/GravityParameters.lean
theorem alpha_gravity_eq_two_alphaLock : alpha_gravity = 2 * alphaLock := by
unfold alpha_gravity alphaLock
ring
What this page does not claim
This theorem does not claim that alpha_gravity is a measured quantity. This theorem does not claim that the relation holds for any other set of parameters. This theorem does not claim that alphaLock has any independent physical meaning outside of this definitional context.
Verify this page
Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:
$ lake env lean IndisputableMonolith/Gravity/GravityParameters.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)
A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.
Derived articles
This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:
- What empirical evidence, if any, supports the framework's choice of these specific parameter definitions?
- How does the relation between alpha_gravity and alphaLock constrain the framework's predictions for galactic rotation curves?
- What is the physical interpretation, if any, of the locking exponent alphaLock?
- Does the framework derive the value of the golden ratio from first principles, or is it an input?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM alpha_gravity_eq_two_alphaLock · IndisputableMonolith/Gravity/GravityParameters.lean
theorem alpha_gravity_eq_two_alphaLock : alpha_gravity = 2 * alphaLock := by unfold alpha_gravity alphaLock ringThe theorem alpha_gravity_eq_two_alphaLock states that alpha_gravity equals 2 times alphaLock, a relation that follows directly from these definitions by algebraic simplification. alpha_gravity_eq_two_alphaLock · IndisputableMonolith/Gravity/GravityParameters.lean