chandrasekhar_mass_from_ledger
plain-language theorem explainer
Mass-to-light ratios in Recognition Science must satisfy 0.5 < M/L < 5 in solar units to anchor Chandrasekhar-mass structures. Researchers modeling white-dwarf stability or stellar assembly cite this bound to link the phi-ladder to observable M/L values. The definition packages the two-sided inequality directly on the constant phi-derived ratio.
Claim. The derived mass-to-light ratio $M/L$ in solar units satisfies $0.5 < M/L < 5$.
background
In the Astrophysics.ChandrasekharMassStructure module the mass-to-light ratio is obtained from the upstream MassToLight derivation. The quantity equals the golden ratio φ ≈ 1.618 solar units and arises from three independent routes: J-cost weighting of photon emission versus mass storage, phi-tier structure of nuclear and photon fluxes, and geometric constraints from wavelength, time scale, and coherence energy. The present definition supplies the structural requirement that mass-scale anchors remain positive and finite inside the RS ladder range.
proof idea
The definition is a direct abbreviation of the conjunction of the two inequalities on the upstream constant ml_derived.
why it matters
This definition is invoked by chandrasekhar_mass_structure (proved via ml_in_observed_range) and supplies the hypotheses for the two implication theorems that extract the separate lower and upper bounds. It therefore closes the structural anchor for Chandrasekhar-mass consistency inside the Recognition Science framework, tying the phi fixed point to the mass-ladder conventions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.