H_bottom_mass_match
plain-language theorem explainer
The declaration encodes the one-percent relative-error agreement between the phi-ladder prediction at the bottom-quark rung and the PDG mass 4180 MeV. Researchers assembling the quarter-ladder hypothesis checks cite it when building the QuarkMassCert certificate. It is introduced as an explicit inequality on the output of predicted_mass applied to res_bottom.
Claim. Let $m_b^pred = m_struct · ϕ^R$ with $R = -2$ the assigned quarter-ladder rung. Then $H_b$ asserts $|m_b^pred - 4180|/4180 < 0.01$.
background
The QuarkMasses module implements the quarter-ladder hypothesis under which quarks occupy quarter-integer rungs on the phi-ladder while sharing the lepton structural mass. The bottom rung is fixed at -2.00. predicted_mass(res) returns electron_structural_mass multiplied by phi raised to the real value of the rational rung res. mass_bottom_exp is the constant 4180. res_bottom is obtained by subtracting the top-to-bottom generation step from res_top. The same numeric targets and formulas appear in the RRF mirror module.
proof idea
This is a direct definition of the proposition as the inequality abs(predicted_mass res_bottom - mass_bottom_exp) / mass_bottom_exp < 0.01. No lemmas or tactics are invoked; the body is the explicit bound itself.
why it matters
It supplies the bottom-match field required by the QuarkMassCert structure and by the theorem quark_mass_verified. The definition appears in the hypothesis_dependent_claims list used by hypothesis_claims_properly_located in QuarkCoordinateReconciliation to keep these checks inside the Physics layer. It instantiates the T12 quarter-ladder numerical verification for the bottom generation before any reconciliation with the core mass model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.