massAtAnchor
plain-language theorem explainer
The massAtAnchor definition supplies the explicit formula for the mass of any Standard Model fermion at the recognition anchor scale using rung offset, gap on ZOf, and phi scaling. Researchers deriving quark and lepton hierarchies from the phi-ladder cite it when testing ratio predictions against data. It is a direct definition that composes the supplied rung, gap, and exponential without further lemmas.
Claim. The anchor mass of fermion $f$ is $M_0$ times the exponential of $(r(f)-8+g(Z(f)))$ times the natural logarithm of the golden-ratio fixed point, where $r(f)$ is the rung of $f$, $Z(f)$ its charge index, and $g$ the gap function $g(Z)=ln(1+Z/phi)/ln phi$.
background
The RSBridge.Anchor module enumerates the twelve Standard Model fermions via the Fermion inductive type. Rung assigns an integer level to each species by sector (lepton, up-quark, down-quark). Gap is the closed-form residue $g(Z)=ln(1+Z/phi)/ln phi$ supplied by AnchorPolicy. M0 and Constants.phi are imported from the mass framework and CPM constants bundle. This implements the Recognition Science mass formula on the phi-ladder: yardstick times phi to the power (rung minus 8 plus gap(Z)). Upstream results from Gap45.Derivation and AnchorPolicy supply the concrete gap and rung definitions.
proof idea
One-line definition that multiplies the base mass M0 by the exponential of the offset (rung f minus 8 plus gap of ZOf f) times the natural log of phi.
why it matters
This definition supplies the concrete mass values used by QuarkAbsoluteBridgeScoreCardCert and the ratio theorems (bottom/strange, charm/up, strange/down) to certify phi-power predictions. It realizes the Recognition Science mass formula on the phi-ladder and connects to the forcing chain through T5 J-uniqueness, T6 phi fixed point, and the eight-tick octave. It closes the bridge from abstract recognition composition to observable particle masses at the anchor scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.