canonical_mass_equal_of_rung_gap_equiv
plain-language theorem explainer
Inside a fixed mass sector, two integer rung/gap pairs that induce the same canonical ladder exponent yield identical predicted masses. Mass-ladder and T6-bridge arguments cite this uniqueness-up-to-gap-equivalence fact. The proof is a short term rewrite: unfold the predictor and the equivalence, then substitute the shared exponent.
Claim. Fix a mass sector. If integer pairs $(r_1,Z_1)$ and $(r_2,Z_2)$ satisfy $r_1-8+\mathrm{gap}(Z_1)=r_2-8+\mathrm{gap}(Z_2)$, then the sector mass predictor returns the same value on both pairs.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law with normalization and calibration. After T6 forces $\varphi$ as the self-similar fixed point, particle masses sit on a $\varphi$-ladder whose exponent is the integer combination of rung and nuclear gap correction.
The canonical exponent is $\mathrm{canonicalMassExponent}(r,Z)=r-8+\mathrm{gap_correction}(Z)$. Two assignments are RungGapEquivalent precisely when those real exponents agree. The mass law predictor for a fixed sector is a function of that exponent (times a sector yardstick), so equal exponents must give equal masses.
This lemma isolates that functional dependence: gap corrections may re-label the integers without changing the physical mass, which is the precise “unique up to gap-correction equivalence” surface stated in the doc-comment.
proof idea
Term-mode, three unfolds then one rewrite. Unfold the mass predictor, the equivalence predicate, and the canonical exponent definition so both sides become the same function of the shared real exponent. The hypothesis heq is definitionally equality of those exponents; rw [heq] substitutes and closes the goal. No external lemmas are required beyond the definitions themselves.
why it matters
Feeds the T6-to-canonical-mass-ladder bridge (t6_to_canonical_mass_ladder_bridge_holds), whose doc-comment states that T6 supplies the canonical mass ladder. Without exponent-level uniqueness, the bridge could not treat the ladder formula as well-defined under gap reparametrization.
In the forcing chain this sits after T6 ($\varphi$ forced) and supports the RS mass formula $\mathrm{yardstick}\cdot\varphi^{r-8+\mathrm{gap}(Z)}$. It separates theorem-grade ladder structure from PDG empirical inputs (the next comment block in the file). It does not itself force $\varphi$ or the eight-tick structure; it only guarantees that once the ladder is in place, mass depends only on the exponent class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.