ml_from_phi_tier_structure
plain-language theorem explainer
The declaration shows that the nucleosynthesis mass-to-light ratio equals phi to the power of an integer drawn from the population tiers set, with the ratio bounded between 1 and 5. Researchers deriving stellar properties from Recognition Science phi-ladders would reference this result to confirm consistency with the eight-tick quantization. The proof selects the exponent 1 and verifies the conditions via direct set membership and rewriting with the equality lemma together with the phi bounds.
Claim. There exists an integer $n$ belonging to the set of population tiers such that the nucleosynthesis-derived mass-to-light ratio equals $phi^n$ and satisfies $1 leq phi^n < 5$.
background
The module develops Strategy 2 for deriving the stellar mass-to-light ratio from the discrete phi-tier structure of nucleosynthesis. Nuclear densities and photon luminosities occupy phi-ladders, so their ratio is phi to an integer power Delta n. The set population_tiers collects the admissible exponents {0,1,2,3} corresponding to different stellar populations. The definition ml_nucleosynthesis unfolds to phi_ladder of tier_difference, and the companion theorem ml_nucleosynthesis_eq_phi establishes that this equals phi exactly.
proof idea
The proof explicitly instantiates Delta n with the value 1. Membership in population_tiers follows by simplification on the set definition {0,1,2,3}. The equality ml_nucleosynthesis = phi^1 is obtained by rewriting with ml_nucleosynthesis_eq_phi and zpow_one. The lower bound 1 < phi is applied directly from one_lt_phi after rewriting. The upper bound proceeds by phi < 2 from phi_lt_two followed by a norm_num comparison against 5.
why it matters
This result supplies the main theorem of the NucleosynthesisTiers module, confirming that the M/L ratio obtained from phi-tier nucleosynthesis lies on the phi-ladder and matches the range expected from Strategy 1 in StellarAssembly. It closes the loop on the eight-tick quantization of nuclear reactions within the Recognition Science framework. The derivation remains independent of the mass-to-light work in Derivations.MassToLight yet produces the same phi^1 typical value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.