upsilon_star_bounds_implies_pos
plain-language theorem explainer
The declaration shows that any stellar mass-to-light ratio satisfying 1.5 < Υ★ < 1.62 must be positive. Galaxy modelers adopting Recognition Science gravity parameters would cite it to exclude unphysical negative ratios inside the stated interval. The proof is a one-line linear arithmetic reduction on the lower bound of the hypothesis.
Claim. If $1.5 < Υ_★ ∧ Υ_★ < 1.62$, then $0 < Υ_★$.
background
The GravityParameters module derives galactic gravity parameters from the golden ratio φ, classifying each as derived, RS-basis, or phenomenological. Υ★ is the stellar mass-to-light ratio, listed as derived with value φ by convention. The module table records seven parameters with their RS formulas and observational matches; Υ★ appears alongside α = 1 - 1/φ and C_ξ = 2φ^{-4}. Upstream results include the Physical structure supplying positivity of c, ħ, G and the tick definition τ₀ = 1 as the fundamental time quantum.
proof idea
The proof is a one-line term that applies linarith to the first conjunct of the hypothesis, which states the lower bound 1.5 > 0 and immediately yields strict positivity.
why it matters
The result secures positivity of Υ★ inside the interval used for galactic modeling and reinforces its derived status as φ in the module's seven-parameter table. It supports the overall derivation of gravity parameters from φ, consistent with the eight-tick octave and D = 3. No downstream theorems are recorded, leaving open its integration into larger rotation-curve or mass-ladder statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.