upsilon_star_bounds
plain-language theorem explainer
The theorem establishes that the stellar mass-to-light ratio parameter Υ★ lies strictly between 1.5 and 1.62. Galaxy modelers working with Recognition Science gravity parameters would cite this interval when anchoring mass-to-light ratios to the golden ratio. The proof is a one-line term wrapper that unfolds the definition of Υ★ to φ and applies the pre-proven numerical bounds on φ.
Claim. $1.5 < Υ_★ ∧ Υ_★ < 1.62$, where $Υ_★ := φ = (1 + √5)/2$.
background
The module GravityParameters derives seven galactic gravity parameters from φ, classifying each as DERIVED, HAS RS BASIS, or PHENOMENOLOGICAL. Υ★ appears in the derived column with the explicit assignment Υ★ = φ. The local setting is the derivation of phenomenological parameters such as α, C_ξ, and p from the same φ foundation, with a0 and r0 linked through the τ★ relation. Upstream lemmas phi_gt_onePointFive and phi_lt_onePointSixTwo supply the concrete numerical bounds 1.5 < φ and φ < 1.62, each proved by direct comparison of √5 to the target constants.
proof idea
The proof is a term-mode one-liner. It unfolds the definition of upsilon_star to obtain phi, then applies the pair of lemmas phi_gt_onePointFive and phi_lt_onePointSixTwo via the exact tactic to discharge the conjunction of strict inequalities.
why it matters
This result places the derived stellar parameter Υ★ = φ inside the interval required for consistency with galactic dynamics in the Recognition framework. It directly supports the module table that lists Υ★ as DERIVED with no observational mismatch. The bound is inherited from the self-similar fixed point φ forced at step T6 of the unified forcing chain. No downstream theorems currently depend on it, leaving open its insertion into full galactic rotation-curve or mass-to-light models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.