ml_matches_stellar_observations
plain-language theorem explainer
The theorem shows that the nucleosynthesis-derived mass-to-light ratio lies strictly between 1 and 5 solar units. Modelers of stellar populations cite it to verify that the phi-ladder output falls inside the observed scatter for main-sequence and giant stars. The proof rewrites the quantity to phi and applies the standard bounds on phi together with a numeric check.
Claim. The nucleosynthesis-derived mass-to-light ratio satisfies $1 < (M/L)_{nuc} < 5$.
background
In the phi-tier nucleosynthesis module, nuclear densities and photon luminosities occupy discrete phi-ladders so that the mass-to-light ratio reduces to $M/L = phi^{Delta n}$ for integer tier difference Delta n. The definition ml_nucleosynthesis is the phi-ladder evaluated at that tier difference, and the upstream equality theorem states that this quantity equals phi exactly. The module works inside the eight-tick quantization of nuclear reactions, which forces Delta n to be an integer and therefore places M/L at successive powers of phi.
proof idea
The tactic proof first rewrites the target using the equality ml_nucleosynthesis_eq_phi to replace the quantity by phi. It then applies the constructor tactic to split the conjunction and discharges the left conjunct with the lemma one_lt_phi. The right conjunct is proved by a short calc that invokes phi_lt_two followed by a norm_num check that 2 is less than 5.
why it matters
This result confirms that the phi-ladder prediction for stellar M/L lies inside the empirical range quoted in the module documentation (main-sequence 0.5-3, giants 2-10, population averages 1-5). It therefore supplies a direct consistency check between the Recognition Science derivation of M/L = phi^{Delta n} and observed stellar data. The declaration sits downstream of the eight-tick nucleosynthesis constraint and the definition of the phi-ladder; it has no further dependents in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.