bottom_mass_match
plain-language theorem explainer
The declaration verifies that the bottom quark mass from the quarter-ladder rung on the phi-ladder differs from the experimental value 4180 MeV by less than one percent. Researchers deriving particle masses from the Recognition Science functional equation would reference this bound when checking consistency with observed spectra. The tactic proof obtains an interval bound on the prediction, applies abs_lt together with linarith to control the deviation, and reduces the relative error by direct division and norm_num comparison.
Claim. Let $m_b$ be the bottom quark mass obtained by scaling the structural base mass by the factor $phi^{r_b}$ where $r_b = -2$ is the assigned quarter-integer rung. Let $m_{exp} = 4180$ MeV. Then $|m_b - m_{exp}| / m_{exp} < 0.01$.
background
The Quarter-Ladder Hypothesis places quarks at quarter-integer positions on the phi-ladder while sharing the same structural base mass as leptons. The bottom quark is assigned rung $R = -2.00 = -8/4$. The definition predicted_mass(res) returns electron_structural_mass multiplied by phi raised to the real power of the rung. The constant mass_bottom_exp is fixed at 4180. This sits inside the T12 derivation of quark masses that begins from the Recognition Composition Law and the eight-tick octave structure.
proof idea
The proof first calls bottom_mass_pred_bounds to obtain the interval containing the predicted mass. It then proves the absolute deviation from 4180 is less than 41 by rewriting the absolute-value inequality and applying linarith to the endpoint bounds. Division by the positive experimental mass 4180 is justified by div_lt_div_of_pos_right, after which the calc block and norm_num reduce the resulting fraction below 0.01.
why it matters
This theorem supplies the numerical verification step for the bottom quark inside the T12 module on quark masses. It supports the Recognition Science mass formula that places particles at phi-ladder rungs derived from the J-uniqueness and self-similar fixed-point conditions. The result anchors the geometric prediction against experiment for the heavy-quark sector while leaving light-quark discrepancies to be addressed by later QCD corrections.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.