upsilon_star_bounds
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 in Recognition Science
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.
scope and limits
- Does not prove any specific numerical value of Υ★ inside the open interval.
- Does not derive Υ★ from first principles beyond the identification with φ.
- Does not address observational calibration or error bars on mass-to-light ratios.
- Does not connect Υ★ to the phi-ladder mass formula or the other six gravity parameters.
formal statement (Lean)
78theorem upsilon_star_bounds : 1.5 < upsilon_star ∧ upsilon_star < 1.62 := by
proof body
Term-mode proof.
79 unfold upsilon_star
80 exact ⟨phi_gt_onePointFive, phi_lt_onePointSixTwo⟩
81
82/-- Upsilon-star bounds imply positivity of the stellar mass-to-light ratio. -/