ml_in_observed_range
The derived stellar mass-to-light ratio satisfies 0.5 < M/L_derived < 5 solar units. Stellar population modelers cite the result to confirm that the zero-parameter derivation matches observed calibrations. The proof is a one-line wrapper that substitutes the defining equality M/L_derived = φ and applies the separate bound on φ.
claim$0.5 < M/L_derived < 5$ (solar units), where $M/L_derived$ is the mass-to-light ratio obtained from the three-strategy Recognition Science derivation and equals the golden ratio $φ$.
background
The module derives the stellar mass-to-light ratio from Recognition Science principles, removing the last external calibration. Three strategies converge on the same value: stellar assembly weights the recognition cost differential between photon emission and mass storage to obtain $φ^n$; φ-tier nucleosynthesis assigns nuclear densities and photon fluxes to discrete φ levels yielding $φ^{Δn}$; geometric observability limits from recognition wavelength, coherence time, and energy force the ratio onto the φ ladder. The definition ml_derived sets this ratio to φ, and ml_derived_value records the identification by reflexivity. Upstream, phi_in_observed_range proves the numerical bound $0.5 < φ < 5$ from the explicit formula for φ and positivity of the square root.
proof idea
The proof is a one-line wrapper. It rewrites ml_derived via ml_derived_value to reduce the goal to φ, then discharges the goal by applying phi_in_observed_range.
why it matters in Recognition Science
This theorem is invoked by ml_derivation_complete to assemble the full M/L certificate, by ml_derivation_falsifiable to state the concrete prediction, and by chandrasekhar_mass_structure. It realizes the module's main result that the φ-ladder value lies inside the observed stellar interval [0.5, 5], completing zero-parameter status for Recognition Science: all constants and astrophysical ratios now derive from the ledger structure. The step aligns with the self-similar fixed point φ forced in the unified chain.
scope and limits
- Does not compute M/L for specific stellar masses or metallicities.
- Does not incorporate dust extinction or observational selection biases.
- Does not predict the distribution of M/L across galaxies.
- Does not derive the numerical bounds from the forcing chain without the explicit φ inequality.
formal statement (Lean)
150theorem ml_in_observed_range : 0.5 < ml_derived ∧ ml_derived < 5 := by
proof body
Term-mode proof.
151 rw [ml_derived_value]
152 exact phi_in_observed_range
153
154/-! ## The Complete Derivation Certificate -/
155
156/-- **THEOREM (RIGOROUS given axioms)**: Complete M/L Derivation Certificate.
157
158 This theorem assembles all the components of the M/L derivation.
159 It depends on the physical axioms `ml_derived_value` and `three_strategies_agree`. -/