H_charm_mass_match
plain-language theorem explainer
The declaration defines a proposition asserting that the charm quark mass predicted from the quarter-ladder rung matches the experimental value of 1270 MeV within 2 percent. Physicists working on geometric mass derivations would reference it when assembling the QuarkMassCert certificate for the hypothesis lane. The definition is a direct numeric comparison using the predicted_mass function applied to res_charm.
Claim. $ |m_{struct} phi^{r_{charm}} - 1270| / 1270 < 0.02 $, where $r_{charm}$ is the quarter-ladder residue for charm and $m_{struct}$ is the shared lepton structural mass.
background
This module formalizes quark masses via the Quarter-Ladder Hypothesis: quarks occupy quarter-integer rungs on the phi-ladder while sharing the structural base mass with leptons. Charm sits at R = -4.50 = -18/4. The upstream predicted_mass applies electron_structural_mass scaled by phi to the residue; mass_charm_exp supplies the PDG target 1270; res_charm is computed from res_bottom minus the bottom-to-charm step.
proof idea
One-line definition that applies the predicted_mass formula to res_charm, subtracts mass_charm_exp, normalizes by the experimental value, and checks the absolute value against the 0.02 bound.
why it matters
It supplies the charm_match field to the QuarkMassCert structure and is listed among hypothesis_dependent_claims. The declaration fills the T12 quarter-ladder step for charm in the hypothesis lane, pending explicit reconciliation with the core parameter-free mass model. It relies on the phi-ladder and eight-tick octave landmarks but remains outside the verified core until the coordinate reconciliation theorem is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.