topMSBarCert_holds
plain-language theorem explainer
The theorem certifies that the top-quark mass scorecard satisfies the Recognition Science rung assignment together with positivity of the PDG pole mass, the MS-bar mass at the top scale, and the RS-predicted pole mass for couplings in (0, 0.5). QCD phenomenologists would cite it to anchor the rung-21 prediction against the PDG 2024 central value of 172.69 GeV. The proof is a direct term-mode record construction that supplies reflexivity for the rung and central value together with three imported positivity lemmas.
Claim. The top-quark mass scorecard certificate holds when the assigned rung equals 21, the PDG pole mass is positive and equals 172.69 GeV, the MS-bar mass evaluated at the top-quark scale is positive, and the RS-predicted pole mass remains positive for every strong coupling constant lying in the open interval (0, 0.5).
background
The module records the top-quark pole and MS-bar masses inside the Recognition Science framework. The PDG 2024 central value is given as 172.69 GeV with the note that the collaboration reports the pole mass; the RS assignment places the top on rung 21 of the phi-ladder (up-type, third generation). The certificate structure TopMSBarCert packages four positivity statements and the rung equality into a single proposition whose body is free of axioms or sorry placeholders.
proof idea
The term proof builds the record by four field assignments: reflexivity discharges the rung-equality and PDG-central-value fields; the remaining three fields are supplied directly by the sibling theorems m_t_pole_PDG_pos, m_t_MS_at_mt_pos, and m_t_pole_predicted_pos. No additional tactics or reductions are required.
why it matters
This declaration closes the top-quark scorecard inside the Physics.TopMSBarScoreCard module and thereby confirms that the rung-21 mass formula is consistent with the measured central value. It supplies the concrete instance of the general mass-ladder relation (yardstick times phi to the power rung minus eight plus gap) for the heaviest up-type quark. The result sits downstream of the two-loop alpha_s and pole-to-MS-bar conversion lemmas imported from the QCD RGE submodules; no downstream theorems yet consume it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.