phi_in_observed_range
plain-language theorem explainer
The golden ratio φ satisfies 0.5 < φ < 5. Recognition Science astrophysicists cite this bound to confirm that the derived stellar mass-to-light ratio falls inside the observed interval [0.5, 5] solar units. The proof is a direct algebraic verification that unfolds the quadratic definition of φ and applies elementary square-root inequalities.
Claim. $0.5 < φ ∧ φ < 5$ where $φ = (1 + √5)/2$.
background
The MassToLight module derives the stellar mass-to-light ratio M/L from Recognition Science by three routes: recognition-cost minimization in stellar assembly, φ-tier differences in nucleosynthesis, and geometric observability constraints. All routes produce M/L equal to a power of φ, the self-similar fixed point of the J-cost function. The Constants structure supplies the numerical value of φ; upstream lemmas on edge lengths and mechanism design ensure the ledger structure forces this fixed point without external calibration.
proof idea
The tactic proof opens the conjunction with constructor. The left conjunct unfolds φ, invokes positivity of √5, and closes with linarith. The right conjunct proves √5 < 3 by rewriting 3 as √9 and applying the monotonicity of sqrt, then closes with linarith.
why it matters
This theorem supplies the numerical range check required by ml_in_observed_range once ml_derived_value equates the derived M/L to φ. It thereby confirms that the discrete φ-ladder values lie inside the observed stellar band, completing one step toward the zero-parameter status asserted in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.