m_t_exp
plain-language theorem explainer
The definition supplies the PDG pole mass of the top quark as the constant 172500 MeV. Researchers comparing Recognition Science phi-ladder predictions to experimental data would cite this value for the rung-21 up-sector quark. It is a direct numerical assignment with no computation or lemmas applied.
Claim. The experimental top quark mass is defined as $m_t = 172500$ MeV (PDG pole mass).
background
The module quarantines experimental PDG values from the certified Recognition Science core. Quark masses follow sector-specific formulas on the phi-ladder: up-type quarks use $m = 2^{-1} phi^{-5} phi^{35} phi^r / 10^6$ MeV (equivalently $phi^{30+r}/(2 times 10^6)$ MeV) with rungs 4, 15, 21; down-type use $2^{23} phi^{-10+r}/10^6$ MeV. Rung is the type of possibly fractional positions on the phi-ladder, defined as the abbreviation Rung := Q.
proof idea
Direct constant assignment of the PDG 2024 pole mass value.
why it matters
Supplies the external experimental benchmark for the top quark at rung 21 in the up-sector, enabling direct comparison to the Recognition Science mass formula. It anchors the verification section of the module but remains outside the derived physics. No downstream theorems depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.