RungGapEquivalent
plain-language theorem explainer
Two integer pairs (rung, nuclear charge Z) are equivalent when they induce the same canonical mass-ladder exponent. Mass-law uniqueness arguments cite this relation to treat gap-corrected reparametrizations as identical. The body is pure definitional equality of the exponents rung − 8 + gap(Z).
Claim. Integer pairs $(r_1,Z_1)$ and $(r_2,Z_2)$ are rung-gap equivalent when their canonical mass exponents agree: $r_1 - 8 + \mathrm{gap}(Z_1) = r_2 - 8 + \mathrm{gap}(Z_2)$, as real numbers.
background
In the Unified Forcing Chain, T0–T8 are forced from the Recognition Composition Law plus normalization and calibration. After T6 pins $\varphi$ as the self-similar fixed point, particle masses sit on a $\varphi$-ladder whose master exponent is the canonical form $\mathrm{rung}-8+\mathrm{gap}(Z)$.
The helper canonicalMassExponent packages that real-valued exponent: cast the rung, subtract the eight-tick offset (the T7 octave period $2^3$), and add the gap correction for nuclear charge $Z$. Two assignments that yield the same number are interchangeable for mass prediction inside a fixed sector.
The surrounding module records the complete inevitability chain from the absolute floor through $\varphi$, eight-tick structure, and $D=3$. This predicate is the equivalence relation used when the mass ladder is stated uniquely up to gap correction.
proof idea
Definitional, not a proof. The predicate is the propositional equality of the two real values produced by the canonical mass exponent on $(r_1,Z_1)$ and $(r_2,Z_2)$. Unfolding replaces it by equality of $\mathrm{rung}-8+\mathrm{gap_correction}(Z)$ on each side; no lemmas are applied.
why it matters
This is the precise equivalence surface for the mass ladder after T6. Downstream, canonical_mass_equal_of_rung_gap_equiv lifts the relation to equality of predicted masses inside a fixed sector: equivalent rung/gap assignments produce the same mass (the "unique up to gap-correction equivalence" claim).
It also appears in the T6_To_CanonicalMassLadder_Bridge certificate, which packages $\varphi$ uniqueness, the canonical formula $\mathrm{rung}-8+\mathrm{gap}(Z)$, $\varphi$-scaling under rung shift, uniqueness under gap-equivalent assignments, and SM fermion masses through the same master law. Framework landmarks: T6 ($\varphi$ forced), T7 (eight-tick offset in the exponent), and the RS mass formula yardstick $\cdot,\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.