H_top_mass_match
plain-language theorem explainer
This definition states that the top quark mass obtained by scaling the lepton structural mass by phi to the power 23/4 matches the experimental value 172690 within a relative error of 0.0005. It would be cited when verifying the quarter-ladder placement for the top quark under the hypothesis. The definition consists of a direct inequality using the predicted mass formula.
Claim. $ | (m_{struct} phi^{23/4} - 172690) / 172690 | < 0.0005 $ where $m_{struct}$ is the structural base mass shared with leptons.
background
The Quarter-Ladder Hypothesis places quarks at quarter-integer rungs on the phi-ladder while sharing the structural mass base with leptons. For the top quark the assigned residue is 23/4. The predicted mass is defined as the structural mass multiplied by phi raised to the residue power. The experimental target is fixed at 172690. This supplies the match condition for the top entry in the QuarkMassCert certificate.
proof idea
The definition is realized as a one-line inequality that invokes the predicted_mass function on the top residue and applies the relative error test against the experimental mass.
why it matters
It supplies the top_match component of QuarkMassCert and appears in the list of hypothesis_dependent_claims. The downstream theorem quark_mass_verified packages it with the other two matches. The construction fills the T12 quark mass step in the Recognition framework and highlights the open reconciliation task with the parameter-free core.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.