mass_bottom_exp
plain-language theorem explainer
The experimental bottom quark mass is supplied as the constant 4180 MeV. Researchers verifying Recognition Science quark mass predictions cite this value when testing the quarter-ladder hypothesis at rung R = -2.00. It enters as a direct numeric assignment to enable match checks against geometric predictions from the phi-ladder.
Claim. $m_b^{exp} = 4180$ MeV, the observed mass of the bottom quark used as target for the quarter-ladder prediction at rung $R = -2.00$.
background
Module Physics.QuarkMasses develops quark masses from the Quarter-Ladder Hypothesis. Quarks share the lepton structural base but occupy quarter-integer rungs on the phi-ladder. The bottom quark is assigned position $R = -2.00 = -8/4$, and the definition supplies the PDG target value of 4180 MeV for comparison with the predicted mass from res_bottom.
proof idea
One-line definition that directly assigns the constant 4180.
why it matters
The definition anchors H_bottom_mass_match and the theorem bottom_mass_match, which establishes 0.79% agreement with the predicted mass. It supports the T12 quark masses section, implementing the quarter-ladder positions. The module notes that full reconciliation with the parameter-free core mass model remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.