tier_difference
plain-language theorem explainer
The definition sets the integer tier difference Δn as nuclear tier minus luminosity tier on the φ-ladder. Stellar modelers deriving mass-to-light ratios from quantized nucleosynthesis would cite it to obtain M/L = φ^Δn. It is realized by direct subtraction of two fixed integer constants.
Claim. Define the tier difference as the integer $n = n_0 - n_1$ on the φ-ladder, where $n_0$ is the canonical nuclear tier and $n_1$ is the canonical photon luminosity tier.
background
This module places nuclear densities and photon luminosities on discrete integer indices called φ-tiers. A φ-tier is an integer index on the φ-ladder. The nuclear tier is fixed at the local value 12 obtained from eight-tick analysis of nuclear densities relative to the Planck scale. The luminosity tier is fixed at the local value 11 corresponding to solar emission. The module then forms the mass-to-light ratio directly from the exponent Δn via M/L = φ^Δn.
proof idea
The definition is a one-line subtraction of the two pre-defined constants nuclear_tier_local and luminosity_tier_local.
why it matters
This definition supplies the exponent that feeds ml_nucleosynthesis and the equality ml_nucleosynthesis = φ. It also supports the verification tier_difference = 1. The construction realizes the eight-tick quantization of nucleosynthesis that forces discrete φ-steps in energy release, consistent with the T7 eight-tick octave of the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.