mass_bottom_exp
plain-language theorem explainer
mass_bottom_exp supplies the experimental bottom quark mass of 4180 MeV as the benchmark for the quarter-ladder prediction. Researchers checking geometric mass hierarchies in Recognition Science cite this constant when validating the bottom quark at topological position R = -2. The declaration is a direct numeric assignment with no computation or lemmas.
Claim. $m_b^{exp} = 4180$ MeV, the observed bottom quark mass used to validate the quarter-ladder hypothesis prediction at rung $R = -2$.
background
The module formalizes T12 quark masses under the Quarter-Ladder Hypothesis: quarks share the lepton structural base but sit at quarter-integer rungs on the phi-ladder. Bottom occupies the ideal position $R = -2.00 = -8/4$, with generation spacing given by quarter-integer steps such as 7.75 rungs from top to bottom. Discrepancies for light quarks are attributed to non-perturbative QCD effects outside the bare geometric model.
proof idea
The declaration is a direct numeric definition that assigns the constant 4180 with no lemmas or tactics applied.
why it matters
This constant is the input datum for H_bottom_mass_match and the theorem bottom_mass_match, which proves the predicted mass from res_bottom lies within 1% of the observed value. It completes the observed side of the T12 derivation, aligning with the phi-ladder and quarter-integer rung structure of Recognition Science. The sub-1% match for bottom confirms the geometric assignment while leaving chiral symmetry breaking for lighter quarks as an open extension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.