charm_mass_pred_bounds
plain-language theorem explainer
The theorem proves that the predicted charm quark mass lies strictly between 1245 and 1247 in the Recognition units. Researchers deriving quark masses from the quarter-ladder hypothesis would cite these bounds when checking geometric predictions against experiment. The proof rewrites the predicted mass via the structural mass definition, inserts the known bounds on m_struct and on phi to the power -4.5, then applies linear arithmetic in two calc chains to sandwich the interval.
Claim. Let $m_0$ be the structural mass scale of the lepton sector and let $m_c = m_0 · φ^{-4.5}$ be the predicted charm mass on the quarter-ladder. Then $1245 < m_c < 1247$.
background
The structural mass is defined as $m_0 = Y · φ^{r-8}$ where $Y$ is the lepton yardstick and $r$ the rung; the upstream theorem structural_mass_bounds supplies the tight interval $10856 < m_0 < 10858$. The predicted mass function is the definition $m = m_0 · φ^{res}$ for any residue res. For charm the residue equals -4.5, so the expression reduces to $m_0 · φ^{-4.5}$ once res_charm_eq_neg45 is applied. The module T12 formalizes the Quarter-Ladder Hypothesis under which quarks share the lepton structural base but sit at quarter-integer rungs on the phi-ladder.
proof idea
The tactic proof begins with simp on the predicted_mass definition, then obtains the structural bounds via ElectronMass.Necessity.structural_mass_bounds and the two numerical axioms phi_pow_neg45_lower and phi_pow_neg45_upper. After rewriting res_charm to -4.5 it splits the conjunction and uses two calc blocks, each closed by nlinarith on the structural and phi-power inequalities, followed by norm_num to reach the target constants 1245 and 1247.
why it matters
The result is the direct input to the downstream theorem charm_mass_match, which concludes that the geometric prediction lies within 2% of the observed charm mass 1270 MeV. It supplies the charm entry in the T12 Quark Masses module and thereby completes one step of the quarter-ladder hypothesis. The argument rests on the forced structural mass scale and the phi-ladder structure already established for the electron sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.