row_top_pos
plain-language theorem explainer
The theorem asserts positivity of the top-quark structural mass prediction on the phi-ladder. Researchers assembling Recognition Science mass scorecards cite it to complete the top-quark certificate. The proof is a one-line wrapper selecting the third conjunct from the joint positivity theorem for all structural quark predictions.
Claim. $0 < phi^{51}/2000000$ (in MeV), where $phi$ is the self-similar fixed point of the Recognition Composition Law.
background
In the Recognition Science framework the top-quark structural mass is defined as $phi^{51}/2000000$ MeV on the phi-ladder at rung 51. The upstream theorem quark_preds_pos states that the up, charm and top structural predictions are simultaneously positive; its proof unfolds the three definitions and invokes positivity of phi-powers together with positivity of division by a positive constant. The module TopQuarkMassScoreCard assembles order-of-magnitude checks for the top quark in Phase 2 without asserting sub-percent numerical agreement with the PDG anchor value.
proof idea
This is a one-line wrapper that applies the third conjunct of quark_preds_pos.
why it matters
The result supplies the positive field required by topQuarkMassScoreCardCert_holds to certify the TopQuarkMassScoreCard. It contributes to the partial theorem status noted in the module for the top-quark row, consistent with the phi-ladder mass formula but without claiming tight absolute match. The declaration therefore closes one positivity obligation in the masses domain while leaving open the question of finer calibration to experimental data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.