QuarkMassCert
plain-language theorem explainer
QuarkMassCert packages three numerical match conditions for the top, bottom, and charm quark masses derived from the quarter-ladder positions on the phi-ladder. Researchers deriving particle masses geometrically would cite this certificate to record that the predictions agree with experiment to the stated tolerances. The structure is introduced as a direct record of the three independent Prop statements without further proof obligations.
Claim. Let $m_t^pred$ be the mass obtained from the quarter-ladder formula at rung $R=5.75$. QuarkMassCert asserts that $|m_t^pred - m_t^exp|/m_t^exp < 0.0005$, together with the analogous bounds $0.01$ for the bottom quark at $R=-2$ and $0.02$ for the charm quark at $R=-4.5$.
background
Module T12 formalizes the quark masses under the Quarter-Ladder Hypothesis: quarks share the structural base mass of leptons but occupy quarter-integer rungs on the phi-ladder. The three fields reference the sibling propositions H_top_mass_match, H_bottom_mass_match and H_charm_mass_match, each a Prop that bounds the relative deviation between the predicted mass (via res_top etc.) and the experimental PDG value. This certificate is distinct from the structural QuarkMassCert in QuarkMassHierarchyFromPhiLadder, which instead requires six flavours, the partition 6=3*2, and the constant ratio phi between consecutive masses.
proof idea
The declaration is a structure definition that simply records the three hypothesis propositions as fields. No tactics or lemmas are applied; it serves as a container for the match certificates.
why it matters
This certificate supplies the concrete numerical checks required by the theorem quark_mass_verified, which in turn populates the general QuarkMassCert structure used in the phi-ladder hierarchy. It advances the T12 derivation of quark masses by isolating the top, bottom, and charm sectors where the geometric predictions are tightest. The module notes that light-quark discrepancies remain to be reconciled with non-perturbative QCD effects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.