MassLadderFormula
plain-language theorem explainer
A mass assignment on sectors obeys the canonical φ-ladder law when every mass equals the sector yardstick times φ to the power (rung − 8 + gap(Z)). Anyone citing the master fermion mass law or the T6→mass-ladder bridge uses this predicate as the interface. It is a pure Prop definition: equality to the geometric ladder formula, no proof content.
Claim. A pair $(m, g)$ consisting of a sector-indexed mass map $m$ and a gap function $g:\mathbb{Z}\to\mathbb{R}$ satisfies the canonical mass-ladder formula when, for every sector $s$, rung $r\in\mathbb{Z}$, and charge label $Z\in\mathbb{Z}$, $$m(s,r,Z)=y_s\,\varphi^{r-8+g(Z)},$$ where $y_s$ is the sector yardstick and $\varphi$ is the golden ratio fixed by T6.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. T5 pins the cost $J(x)=(x+x^{-1})/2-1$; T6 forces $\varphi$ as the unique positive self-similar fixed point of the discrete ledger.
Particle masses in RS sit on a $\varphi$-ladder. Each sector carries a fixed yardstick $y_s$; the exponent is an integer rung shifted by a universal offset of $8$ (the eight-tick octave from T7) plus a gap correction $g(Z)$ that depends on the charge/atomic label. The primer mass formula is exactly $y_s,\varphi^{r-8+\mathrm{gap}(Z)}$.
This definition packages that geometric law as a Prop on an arbitrary mass assignment and gap function, so later uniqueness and bridge certificates can quantify over “any ladder that looks like the canonical one.”
proof idea
Definitional, not a proof. The body is the universal quantification
$\forall,s,r,Z.; m(s,r,Z)=y_s,\varphi^{(r:\mathbb{R})-8+g(Z)}$.
No tactics, no lemmas: it is the interface Prop that canonical_mass_law_formula discharges by rfl against the existing master predictor, and that uniqueness and bridge structures take as a hypothesis.
why it matters
This is the typed interface between T6 ($\varphi$ forced) and the Standard Model mass spectrum inside the forcing chain. Downstream, canonical_mass_law_formula shows the existing master predictor is exactly this ladder; canonical_mass_ladder_unique_of_gap_equiv shows any other ladder with the same forced gap agrees pointwise; and T6_To_CanonicalMassLadder_Bridge packages $\varphi$-uniqueness, the canonical formula, rung-shift scaling, and SM fermion routing as a single certificate.
Framework landmarks: T6 supplies $\varphi$; T7’s eight-tick octave supplies the $-8$ offset; the gap correction is the Gap-45-derived term that synchronizes with T8. Without this Prop, the mass law would remain an ad-hoc formula rather than a forced geometric consequence of the chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.