top_quark_pred
plain-language theorem explainer
The structural mass prediction for the top quark at rung 21 in the up sector is supplied as the golden ratio raised to the 51st power divided by two million. Researchers verifying quark mass ladders and ratio agreements in scorecards cite this value when checking structural predictions. The definition is introduced by a direct one-line assignment from the phi constant.
Claim. The structural mass prediction for the top quark is $m_t = phi^{51}/2000000$, where $phi$ is the golden ratio constant from the CPM bundle.
background
The Masses.Verification module supplies structural mass formulas for comparison against PDG experimental values, which are imported as constants rather than derived. Quark masses follow the phi-ladder placement with sector-specific rungs; the top quark occupies rung 21 in the up sector. The upstream Constants structure from LawOfExistence bundles the required constants, including phi defined via the golden ratio equation.
proof idea
This is a one-line definition that directly assigns the value of the phi constant raised to the natural number 51, followed by division by 2000000.
why it matters
The definition supplies the top quark entry required by QuarkScoreCardCert and QuarkAbsoluteBridgeScoreCardCert, which certify positive predictions and the top-to-charm ratio equaling phi to the sixth. It completes the rung-21 slot in the phi-ladder mass formula, supporting the absolute quark-mass bridge in the Recognition framework. No open questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.