tiers_are_quantized
plain-language theorem explainer
The theorem asserts that nuclear density and luminosity tiers always differ by an integer under eight-tick quantization. Stellar astrophysicists modeling mass-to-light ratios in Recognition Science would cite it to place M/L on the phi-ladder. The proof is a direct term-mode construction that exhibits the difference as the required integer.
Claim. For all nuclear density tier $ρ$ and photon luminosity tier $L$ in the $φ$-tier structure, there exists an integer $n$ such that $ρ - L = n$.
background
In the Recognition Science treatment of nucleosynthesis, physical quantities occupy discrete $φ$-tiers: nuclear density scales as $φ^{n_{nuclear}} × ρ_{Planck}$ and luminosity as $φ^{n_{photon}} × L_{unit}$. The mass-to-light ratio is then the tier difference $M/L = φ^{Δn}$. The upstream definition eight_tick_quantizes_tiers states that nuclear reactions are quantized by the eight-tick cycle, with each step requiring 8 ticks for one complete recognition cycle and releasing energy in units of $E_{coh} × φ^{-r}$ for some rung $r$; this forces tier indices to be integers.
proof idea
The proof is a one-line term wrapper. It introduces the tiers $ρ$ and $L$, then directly exhibits the integer $n = ρ - L$ to discharge the existential quantifier in eight_tick_quantizes_tiers.
why it matters
This result shows that nucleosynthesis-derived M/L lies in the set {$φ^n : n ∈ [0,3]$}, matching the independent Strategy 1 computation in the module. It fills the eight-tick quantization step (T7) in the forcing chain, ensuring discrete tiers for stellar assembly. The parent structure is the overall nucleosynthesis M/L equivalence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.