PhiTier
plain-language theorem explainer
PhiTier supplies the integer index set for the phi-ladder used to label nuclear densities and photon luminosities. Astrophysicists computing mass-to-light ratios from tier differences in Recognition Science nucleosynthesis models cite this definition. It is introduced as a direct abbreviation of the integers with no further structure or proof steps.
Claim. A phi-tier is an integer index $n$ belonging to the set of integers, serving as the discrete label for positions on the phi-ladder where nuclear density scales as phi to the power n and luminosity scales similarly.
background
The module develops Strategy 2 for nucleosynthesis by placing physical quantities on discrete phi-tiers. Nuclear density occupies one tier and photon luminosity another; their difference yields the mass-to-light ratio as phi to the power of that integer difference. The phi-ladder itself is the map sending each tier index to the real number phi raised to that index. This setting rests on the eight-tick cycle that forces all tier steps to be integers. The upstream dependency on the spin value definition supplies only the general recognition of discrete labels and is not invoked in the tier indexing itself.
proof idea
This is a one-line abbreviation that directly equates PhiTier to the integers.
why it matters
PhiTier supplies the common index type for NuclearTier and LuminosityTier, which in turn feed eight_tick_quantizes_tiers asserting that tier differences are integers. The module doc-comment states that this forces the nucleosynthesis-derived M/L to lie in the set of integer powers of phi, matching the eight-tick octave constraint from the Recognition framework. It closes the discrete tier step required for the main result that M/L belongs to the interval of phi powers from 0 to 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.