charm_mass_match
plain-language theorem explainer
The theorem shows that the charm quark mass predicted by the quarter-ladder hypothesis on the phi-ladder satisfies a relative error below 2 percent against the experimental value of 1270 MeV. Researchers validating geometric derivations of fermion masses against the observed spectrum would cite this bound when checking the R = -4.5 rung assignment. The proof invokes the established interval (1245, 1247) MeV for the prediction, applies the absolute-value inequality, and reduces the relative deviation by direct comparison to 25/1270.
Claim. Let $m_0$ be the structural base mass shared with the electron and let $R = -4.5$ be the quarter-integer rung assigned to the charm quark. Define the predicted mass by $m_0 phi^R$. With the observed charm mass fixed at 1270 MeV, the relative deviation satisfies $|m_0 phi^R - 1270|/1270 < 0.02$.
background
The module formalizes T12, the quark-mass sector of the Recognition framework, under the Quarter-Ladder Hypothesis. Quarks occupy the same structural base mass as leptons but sit at quarter-integer positions on the phi-ladder; the charm assignment is R = -4.5. The predicted mass is obtained by scaling the structural base by phi raised to the rung value. Upstream, charm_mass_pred_bounds supplies the concrete interval 1245 < predicted mass < 1247, which rests on the structural-mass bounds for the electron and the monotonicity of phi to the power -4.5.
proof idea
The tactic proof first imports the interval theorem charm_mass_pred_bounds. It then rewrites the target expression with the concrete experimental value 1270, constructs an auxiliary bound on the absolute difference via abs_lt and linarith, and applies div_lt_div_of_pos_right to obtain the relative error strictly less than 25/1270. A final norm_num step confirms 25/1270 < 0.02.
why it matters
This result supplies the explicit numerical check for the charm rung inside the Quarter-Ladder Hypothesis of T12. It closes one link in the chain that derives all fermion masses from the single structural base and the phi-ladder geometry. The 2 percent tolerance is consistent with the framework's allowance for non-perturbative QCD corrections on light quarks; the same pattern is used for the top and bottom checks in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.