predict_mass
plain-language theorem explainer
The predict_mass definition supplies the explicit formula for particle masses in Recognition Science by scaling the sector yardstick with a power of phi determined by rung and gap values. Researchers deriving Standard Model fermion masses or checking Yukawa couplings would invoke it to obtain numerical predictions from the phi-ladder. The implementation reduces directly to multiplication and exponentiation using the imported yardstick and phi constant.
Claim. For sector $s$ and particle identifier $n$, the predicted mass is $m(s,n) = Y(s) · ϕ^{r(s,n) + g(s,n) - 8}$, where $Y(s)$ is the yardstick for sector $s$, $r(s,n)$ the rung number, and $g(s,n)$ the gap correction.
background
In the AnchorPolicy module, masses are computed on the phi-ladder using the formula yardstick times phi to a power adjusted by rung and gap. The yardstick is defined in Anchor as the base mass scale for each sector. Rung and gap functions map sector and name to integers representing the phi-tier and correction, respectively. Upstream, the phi constant comes from Constants.RSNativeUnits, and rung concepts trace to Compat.Constants and Cosmology scale definitions. The local setting ties into the mass formula from the Recognition Science primer: yardstick * phi^(rung - 8 + gap(Z)).
proof idea
This is a direct definition that unfolds to the product of Anchor.yardstick sector and Constants.phi raised to the exponent (rung sector name + gap sector name - 8). No tactics are involved; it is a one-line arithmetic expression relying on the rung and gap sibling definitions.
why it matters
This definition anchors the mass predictions that feed into the master mass law in MassLaw and the fermion mass computations in SMVerification. It realizes the mass formula on the phi-ladder, connecting to the T6 phi fixed point and the eight-tick octave structure. Downstream certificates such as SMVerificationCert rely on it for positivity and scaling properties. It touches the open question of first-principles derivation of quark rungs, which remain hypothesis-driven per the module comments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.