top_mass_match
plain-language theorem explainer
The top quark mass lies within 0.05 percent relative error of the value obtained by scaling the electron structural mass by phi to the power 23/4. Researchers comparing geometric mass predictions to collider data would cite this bound when checking the quarter-ladder hypothesis. The argument invokes an interval lemma for the predicted mass, applies abs_lt and linarith to bound the absolute deviation by 66, then uses div_lt_div_of_pos_right followed by norm_num to confirm the relative error stays below the threshold.
Claim. $|m(r) - 172690| / 172690 < 0.0005$ where $r = 23/4$ and $m(r) = m_0 · ϕ^r$ with $m_0$ the electron structural mass in MeV.
background
The module formalizes the quarter-ladder hypothesis: quarks occupy the same structural base mass as leptons but sit at quarter-integer rungs on the phi-ladder. The top quark is assigned residue 23/4. The definition predicted_mass(res) scales the electron structural mass by phi raised to the real value of the residue. The constant mass_top_exp is fixed at the experimental value 172690 MeV. Upstream results supply the residue definition, the scaling formula, and the experimental constant; an interval lemma (top_mass_pred_bounds) supplies the concrete bounds (172722, 172755) on the predicted value.
proof idea
The tactic proof first obtains the interval bounds via top_mass_pred_bounds. It simplifies the experimental constant, constructs an auxiliary statement that the absolute deviation is less than 66 using abs_lt and linarith on the interval endpoints, establishes positivity of the denominator, applies div_lt_div_of_pos_right to pass to the relative error, and finishes with a calc block that chains the inequality to 66/172690 followed by norm_num to reach the target 0.0005.
why it matters
This theorem supplies the top-quark case inside the T12 derivation of quark masses from the quarter-ladder hypothesis. It confirms that the phi-ladder prediction at residue 23/4 reproduces the observed mass to the stated precision, consistent with the Recognition Science mass formula that places particles on the phi-ladder via structural mass times phi to a rung offset. Because the module treats light-quark discrepancies as arising from omitted QCD effects, the result isolates the geometric contribution for the heaviest generation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.