m_b_exp
plain-language theorem explainer
Experimental bottom-quark mass fixed at 4180 MeV (MS-bar scheme at the pole), taken from PDG 2024 as 4.18(3) GeV. Mass-comparison and verification modules cite this constant when checking Recognition Science φ-ladder predictions against data. The declaration is a bare real literal with no proof obligation.
Claim. The experimental bottom-quark mass is the real constant $m_b^{\mathrm{exp}} = 4180$ (MeV), corresponding to $4.18(3)\,\mathrm{GeV}$ in the $\overline{\mathrm{MS}}$ scheme evaluated at $m_b$.
background
The MassComparison module holds PDG 2024 experimental masses side-by-side with Recognition Science predictions. It is quarantined from the certified surface precisely because it imports external data and because the RS side still depends on the anchor/φ-ladder rung system.
RS predicts a species mass by $m = \mathrm{yardstick}(\mathrm{sector})\times\varphi^{r_0+r_{\mathrm{species}}}$, with coherence energy $E_{\mathrm{coh}}=\varphi^{-5}$ and sector integers fixed by cube geometry. Experimental anchors such as this bottom-quark value supply the numerical targets against which those ladder predictions are scored.
Sibling constants in the same file fix the electron, muon, tau, and light-quark experimental masses (and their one-sigma uncertainties) in the same MeV convention.
proof idea
Pure definition: the real literal 4180 is assigned with no tactics, lemmas, or computation. The accompanying doc-comment records the PDG provenance (4.18(3) GeV = 4180(30) MeV, MS-bar at $m_b$).
why it matters
Supplies the PDG bottom-quark datum required by the machine-verified mass-comparison layer. Without a fixed experimental target, the RS mass formula $m=\mathrm{yardstick}\times\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$ cannot be scored numerically against reality. The module remains quarantined: experimental input is not derived from the forcing chain (T0–T8) or the Recognition Composition Law, so this constant never enters certified theorems. It exists solely so residual and ratio checks against the φ-ladder can be stated in Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.