T6_To_CanonicalMassLadder_Bridge
plain-language theorem explainer
Bridge certificate: once T6 forces φ as the unique positive root of x²=x+1, the Recognition mass ladder is exactly the canonical formula with exponent rung−8+gap(Z). Cite it for φ-scaling of sector masses, uniqueness under gap-equivalent rung assignments, and routing of SM fermion masses through one master law. It is a Prop structure packaging nine fields; instances are built by the companion holds theorem, not proved inside the structure itself.
Claim. Assume $\varphi$ is forced: the unique $r>0$ with $r^2=r+1$. Then the master mass law equals the canonical ladder $m(s,r,Z)=y_s\,\varphi^{r-8+\mathrm{gap}(Z)}$; one rung step multiplies every sector mass by $\varphi$; $\mathrm{gap}(0)=0$; any mass map obeying the same formula and gap coincides with the master law; gap-equivalent rung pairs give equal masses; each Standard Model fermion mass equals the master prediction on its sector, rung, and $Z$ and is positive; PDG comparison values remain an empirical encoded surface.
background
In the Unified Forcing Chain, T6 asserts that a discrete ledger with self-similar cost admits only one scaling ratio: $\varphi=(1+\sqrt{5})/2$, the unique positive solution of $x^2=x+1$. That uniqueness is the input hypothesis of this bridge.
The canonical mass ladder assigns to each sector $s$, integer rung $r$, and charge-like index $Z$ the value $y_s,\varphi^{r-8+\mathrm{gap}(Z)}$, where $y_s$ is the sector yardstick. Two rung/gap pairs are equivalent when they induce the same exponent, so they must predict the same mass. The Recognition primer mass formula is exactly this yardstick times $\varphi$ to that exponent.
The module's stronger claim is a complete inevitability chain from the cost foundation (Recognition Composition Law plus normalization and calibration) through T0–T8. This structure is the interface that turns T6's $\varphi$ into the mass-ladder layer used later in the complete chain.
proof idea
No proof body: the declaration is a Prop structure (certificate interface). Each field is a named obligation—φ uniqueness re-exported from T6, the master law matching MassLadderFormula, rung scaling by φ, vanishing neutral gap, uniqueness for equal gaps, equality under RungGapEquivalent, SM fermion routing and positivity, and the PDG empirical surface.
Inhabitation is deferred to t6_to_canonical_mass_ladder_bridge_holds, which fills the fields from h6.phi_unique, canonical_mass_law_formula, canonical_mass_law_rung_scaling, and sibling lemmas. A Subsingleton instance records that any two certificates for fixed T6 are definitionally equal.
why it matters
Without this bridge, T6 only pins φ; the mass sector would not be forced to the single canonical ladder. Downstream, CompleteForcingChain consumes the bridge so the full T−1…T8 package includes mass-ladder structure, and t6_to_canonical_mass_ladder_bridge_holds is the theorem that supplies a concrete certificate from any T6_Phi_Forced.
Framework landmarks: T6 (φ forced as self-similar fixed point) and the primer mass formula yardstick·φ^(rung−8+gap(Z)). The structure also keeps PDG numbers on an empirical surface, separating theorem-grade ladder identities from encoded comparison data. That split matters for anyone auditing what is forced versus what is fitted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.