canonicalMassExponent
plain-language theorem explainer
The canonical mass exponent on the φ-ladder is the real number rung − 8 plus the gap correction at charge Z. Mass-law and rung/gap-equivalence results cite this as the shared exponent that enters φ^(·). The body is a one-line arithmetic definition, not a derived identity.
Claim. For integers $r$ (ladder rung) and $Z$, the canonical mass exponent is the real number $r - 8 + g(Z)$, where $g$ is the mass-law gap correction.
background
The module UnifiedForcingChain assembles the complete inevitability chain T−1 through T8 from the Recognition Composition Law, normalization, and calibration. Downstream of φ-forcing (T6) and the eight-tick/D=3 steps (T7–T8), particle masses sit on a discrete φ-ladder.
In RS-native units the mass formula is yardstick times $\varphi$ raised to an integer-shifted exponent. The shift subtracts the eight-tick reference level and adds a Z-dependent gap correction from the mass law (the same correction family used in α-precision and Gap-45 work). The two integer inputs are the rung index and the atomic-number (or sector charge) label Z.
This definition packages that exponent as a single real-valued function so later statements can compare assignments by equality of exponents rather than by ad hoc pairs $(r,Z)$.
proof idea
Pure definition: cast the integer rung to $\mathbb{R}$, subtract 8, and add Masses.MassLaw.gap_correction at Z. No lemmas, tactics, or proof obligations.
why it matters
Gives the precise exponent that the RS mass ladder uses: yardstick $\cdot,\varphi^{r-8+g(Z)}$. It is the carrier for rung/gap equivalence: two assignments are equivalent exactly when their canonical exponents agree, and that relation is what canonical_mass_equal_of_rung_gap_equiv unfolds to prove equal predicted masses inside a fixed sector.
In the forcing-chain narrative this sits after T6–T8 (φ, eight-tick octave, D=3) and the Gap-45 sync, packaging the mass-side arithmetic so uniqueness-up-to-gap-correction is a literal equality of reals rather than a hand-waved reparametrization. It does not itself force the numerical gap table; it standardizes the exponent those tables feed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.