population_tiers
plain-language theorem explainer
The definition enumerates the integer tiers {0, 1, 2, 3} that label distinct stellar populations by their effective rung difference on the φ-ladder. Astrophysicists fitting galactic mass-to-light ratios cite this set when mapping observed M/L scatter to quantized nucleosynthesis steps. The definition is a direct set literal with no computation or proof obligations.
Claim. The set of stellar population tiers is defined as the finite subset $S = {0, 1, 2, 3}subseteqmathbb{Z}$ of the integer φ-ladder indices.
background
A φ-tier is an integer index on the φ-ladder. In the module setting, nuclear density scales as φ to the nuclear tier while photon luminosity scales as φ to the photon tier, so the mass-to-light ratio equals φ raised to the tier difference Δn. The eight-tick cycle forces Δn to be an integer, restricting the possible values to a small discrete set. Upstream Recognition structures supply the underlying ledger and cycle definitions that enforce the discrete steps.
proof idea
The definition is a direct set literal that enumerates the four tiers. No lemmas are applied; the body simply writes the set {0, 1, 2, 3} of type Set PhiTier.
why it matters
This set supplies the admissible Δn values for the downstream theorem ml_from_phi_tier_structure, which states that the stellar M/L ratio is derived from φ-tier structure of nucleosynthesis and quantized by the eight-tick cycle. It implements the module claim that M/L lies in {φ^n : n in [0, 3]} and matches the tabulated population types in the declaration comment. The definition closes the discrete ladder to observed stellar populations without introducing continuous age distributions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.