top_mass_pred_bounds
plain-language theorem explainer
The theorem places the predicted top quark mass strictly between 172722 and 172756 in Recognition Science units. Researchers comparing the quarter-ladder hypothesis to experimental collider data cite this interval to quantify geometric accuracy for the top quark. The proof pulls in pre-established bounds on the structural mass and on phi to the 5.75 power, rewrites the residue, and applies linear arithmetic to sandwich the product.
Claim. $172722 < m_0 phi^{5.75} < 172756$ where $m_0$ is the structural mass scale shared by leptons and quarks, and the exponent 5.75 is the quarter-ladder residue assigned to the top quark.
background
Module T12 formalizes quark masses under the Quarter-Ladder Hypothesis: quarks share the same structural base $m_0 = Y phi^{r-8}$ as leptons but sit at quarter-integer rungs on the phi-ladder. The top quark is assigned residue 23/4 = 5.75. The predicted mass is defined as $m = m_0 phi^{res}$. Upstream, structural_mass_bounds supplies the tight interval 10856 < m_0 < 10858, obtained from the closed form 2^{-22} phi^{51} and Fibonacci bounds on phi powers.
proof idea
The tactic proof simplifies the predicted_mass definition, obtains the structural mass bounds and the two phi^{5.75} bounds, rewrites the top residue, then splits into a constructor. Each side uses a calc that applies nlinarith with the structural and phi bounds followed by norm_num on the explicit constants.
why it matters
This supplies the numerical interval required by the downstream top_mass_match theorem, which verifies the prediction lies within 0.05 percent relative error of the observed top mass. It completes the top-quark case inside the T12 derivation of the Quarter-Ladder Hypothesis. In the larger framework it shows how the phi-ladder with quarter steps produces high-precision mass predictions for the heaviest quark without additional parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.