tier_difference_value
plain-language theorem explainer
The theorem establishes that the difference between the nuclear tier (12) and luminosity tier (11) equals exactly one phi-ladder step. Astrophysicists deriving mass-to-light ratios from discrete tier structures in Recognition Science would cite this equality when matching nucleosynthesis predictions to observed stellar M/L values. The proof proceeds by unfolding the three local tier definitions followed by direct numerical reduction.
Claim. The difference between the canonical nuclear tier $n=12$ and luminosity tier $n=11$ satisfies $n=1$.
background
In the Recognition Science framework, stellar quantities occupy discrete phi-tiers. Nuclear density scales as phi to the nuclear tier times Planck density, while photon luminosity scales as phi to the luminosity tier times the unit luminosity. The module sets the nuclear tier to 12 within the stellar window from eight-tick analysis of nuclear-to-Planck density ratios, and the luminosity tier to 11 for solar-scale emission.
proof idea
The proof unfolds the definitions of tier_difference, nuclear_tier_local, and luminosity_tier_local, then applies norm_num to reduce the arithmetic difference 12-11 to 1.
why it matters
This equality confirms that the nucleosynthesis-derived M/L equals phi^1, matching the main module claim that M/L lies in the set of phi^n for n in [0,3]. It closes the local tier gap required by the eight-tick cycle and supports the phi-ladder mass formula in stellar contexts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.