canonical_mass_ladder_unique_of_gap_equiv
plain-language theorem explainer
Any mass assignment obeying the canonical ladder formula with the forced gap correction equals the master mass law at every sector, rung, and charge. Mass-spectrum workers cite it to collapse alternative gap choices to the unique RS predictor. The proof is a three-step calc: expand the formula, rewrite the gap, and match by definitional equality.
Claim. Let $m$ assign a real mass to each sector $s$, rung $r\in\mathbb{Z}$, and integer $Z$, and let $g:\mathbb{Z}\to\mathbb{R}$ be a gap function. Suppose $m(s,r,Z)=y_s\,\varphi^{r-8+g(Z)}$ for the sector yardstick $y_s$, and $g(Z)$ equals the canonical gap correction for every $Z$. Then $m(s,r,Z)$ equals the canonical predicted mass for every $(s,r,Z)$.
background
The ambient module is the Unified Forcing Chain: T-1 through T8 are derived as inevitabilities from the Recognition Composition Law plus normalization and calibration. T6 forces $\varphi$ as the self-similar fixed point of the discrete ledger; the mass spectrum is then read off a $\varphi$-ladder.
A mass assignment obeys the canonical ladder formula relative to a gap function $g$ when, for every sector, rung, and $Z$, $$m(s,r,Z)=y_s,\varphi^{(r:\mathbb{R})-8+g(Z)},$$ with $y_s$ the sector yardstick. The master mass law is exactly that formula with $g$ specialized to the canonical gap correction (the RS-native charge-dependent shift on the ladder).
The primer mass formula is the same object: yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$. This lemma isolates the uniqueness surface once the gap is fixed to that correction.
proof idea
Tactic proof by intro on sector, rung, and $Z$, then a calc chain. First step applies the ladder-formula hypothesis to expand $m$ as yardstick times $\varphi$ to the power $r-8+g(Z)$. Second step rewrites $g(Z)$ to the canonical gap correction via the pointwise gap hypothesis. Third step is rfl: the resulting expression is definitionally the canonical predicted mass. No external lemmas beyond the two hypotheses and the definition of the master mass law.
why it matters
Closes the uniqueness half of the mass-ladder bridge after T6. Downstream, t6_to_canonical_mass_ladder_bridge_holds packages T6 ($\varphi$ forced) into a bridge record whose fields include the canonical formula and rung scaling by $\varphi$; this lemma supplies the pointwise agreement that makes alternative gap-equivalent ladders collapse to that canonical formula.
In the forcing chain it sits under T6 ($\varphi$ as self-similar fixed point) and feeds the constants/mass layer where $c$, $\hbar$, $G$, and $\alpha$ are already $\varphi$-derived. It is the precise "unique up to gap-correction equivalence" surface: once the gap matches the forced correction, no other ladder formula can disagree with the master mass law inside a fixed sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.