m_b_exp
plain-language theorem explainer
The declaration supplies the PDG central value for the bottom quark mass as the real number 4180 in MeV units. Researchers verifying Recognition Science mass ladder predictions against experimental data would reference this constant. It is introduced as a bare numeric definition with no derivation or proof obligations.
Claim. $m_b^{exp} = 4180$ MeV, the central PDG 2024 value for the bottom quark in the MS-bar scheme at scale $m_b$.
background
Quark masses in Recognition Science follow the down-quark sector formula $m = 2^{23} φ^{-10+r}/10^6$ MeV with rung integer r drawn from Anchor.lean. For the b quark the rung is 21, yielding a predicted mass that is compared to the experimental anchor. The module explicitly quarantines all PDG inputs as imported constants rather than RS derivations.
proof idea
Direct constant assignment of the integer 4180 to the real number m_b_exp with no tactics, reductions, or referenced lemmas.
why it matters
This constant supplies the experimental reference for bottom-quark verification inside the same module, closing the numerical comparison against the phi-ladder mass formula. It supports checks that use the eight-tick octave and D=3 spatial dimensions already fixed in the upstream forcing chain. No open scaffolding questions attach to the definition itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.