all_ml_on_phi_ladder
plain-language theorem explainer
All stellar population mass-to-light ratios lie on the φ-ladder, so each equals φ raised to an integer power. Astrophysicists working with Recognition Science nucleosynthesis models cite this to confirm that observed M/L values for young stars, main-sequence stars, red giants, and old populations are exactly the discrete steps φ^0 through φ^3. The proof is a one-line term reduction that substitutes the definition of the φ-ladder directly at each tier in the finite set.
Claim. $For every stellar population tier $n$ in the set {0, 1, 2, 3}, there exists an integer $k$ such that the φ-ladder value at tier $n$ equals $φ^k$.
background
The module develops Strategy 2 for deriving stellar mass-to-light ratios from discrete φ-tier structure of nuclear densities and photon fluxes. Nuclear density scales as φ to a nuclear tier times Planck density; luminosity scales as φ to a photon tier times the unit luminosity. Their ratio is therefore φ raised to the integer tier difference Δn. The φ-ladder at tier n is defined as φ^n. The set of population tiers is the finite set {0, 1, 2, 3}, corresponding to young blue stars (Δn=0), main-sequence stars (Δn=1), red giants (Δn=2), and old populations (Δn=3). Upstream, the eight-tick cycle forces all nucleosynthesis steps to land on integer exponents of φ.
proof idea
The term proof proceeds by introducing the tier n, discarding the membership hypothesis, and supplying n itself as the witness k. Reflexivity then closes the equality because the φ-ladder is defined by direct exponentiation with base φ.
why it matters
This result closes the claim that every population M/L value is quantized on the φ-ladder, directly supporting the main theorem that nucleosynthesis-derived M/L ratios match Strategy 1 and lie in the set {φ^n : n ∈ [0, 3]}. It instantiates the eight-tick octave constraint (T7) and the self-similar fixed point φ (T6) inside astrophysical observables. No open scaffolding remains; the finite enumeration of tiers makes the statement exhaustive for the populations considered.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.