m_H_exp

The MassComparison module is quarantined from the certified RS surface: it imports PDG experimental numbers and compares them to RS mass predictions built on the $\phi$-ladder. Predictions take the form $m(\mathrm{species}) = \mathrm{yardstick}(\mathrm{sector})\times\phi^{r_0+r_{\mathrm{species}}}$, with coherence energy $E_{\mathrm{coh}}=\phi^{-5}$ and sector yardsticks fixed by cube geometry.

Sibling constants in the same file pin lepton and light-quark experimental masses and their one-sigma widths (electron, muon, tau, $u$, $d$, $s$). The Higgs entry follows the same convention: a bare real in MeV equal to the PDG central value, with the uncertainty $110,\mathrm{MeV}$ recorded only in the doc-comment.

The same numeric binding appears in ElectroweakMasses, next to the RS Weinberg-angle formula $\sin^2\theta_W=(3-\phi)/6$.

No proof. The declaration is a one-line def that binds the real constant $125200$. There are no tactics, lemmas, or algebraic reductions.

Supplies the laboratory anchor against which any RS Higgs-mass prediction on the $\phi$-ladder is scored. Lives in the verification layer that the module doc marks as non-certified, because experimental inputs are external to the forcing chain (T0–T8) and the Recognition Composition Law. Downstream electroweak mass code reuses the same constant when comparing ladder output to PDG 2024. Does not itself derive the Higgs mass from RS; it only freezes the comparison target.