alpha_gravity_pos
plain-language theorem explainer
alpha_gravity_pos establishes that the RS-derived dynamical-time exponent, defined as 1 minus one over phi, is strictly positive. Galactic dynamics modelers cite it to place the parameter in the allowed range for rotation-curve fits. The proof is a short tactic sequence that unfolds the definition, invokes one_lt_phi, shows one over phi is less than one, and finishes with linear arithmetic.
Claim. $0 < 1 - 1/φ$ where $φ$ denotes the golden ratio satisfying $φ = (1 + √5)/2$.
background
The module GravityParameters derives seven galactic gravity parameters from Recognition Science. alpha_gravity is classified as DERIVED with the explicit formula 1 - 1/φ and an observed match of 1.8 percent to the fitted value 0.389 ± 0.015. The local setting treats each parameter as either mathematically proven from φ, equipped with an RS basis, or purely phenomenological. The proof depends on the upstream lemma one_lt_phi, which states 1 < φ by comparing square roots and applying the ordering of the reals.
proof idea
The tactic proof first unfolds the definition alpha_gravity := 1 - 1/φ. It obtains 1 < φ from one_lt_phi and phi_pos from the constants module. A subsidiary goal shows 1/φ < 1 by rewriting the division inequality and using the positivity of φ. The final linarith step closes the positivity claim.
why it matters
The result sits inside the seven-parameter table of the module and confirms that the derived exponent alpha_gravity lies in the positive reals required for dynamical-time scaling. It supports the RS prediction 1 - 1/φ that matches the paper-fitted value to 1.8 percent. The declaration closes a positivity check that downstream derivations of galactic parameters rely upon; it touches the T6 step in which φ is forced as the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.