mass_top_exp
plain-language theorem explainer
The definition supplies the PDG experimental top quark mass of 172690 MeV as a numeric constant. Researchers verifying the quarter-ladder hypothesis for quark masses cite it when checking geometric predictions against data. It is introduced by direct assignment with no computation or derivation steps.
Claim. The experimental top quark mass equals 172690 MeV.
background
The module derives quark masses from the Quarter-Ladder Hypothesis: quarks share the structural base mass with leptons but sit at quarter-integer rungs on the phi-ladder. The top quark occupies rung R = 5.75 = 23/4, with the module noting that light-quark discrepancies arise from unmodeled non-perturbative QCD effects. This definition supplies the observed target used for match verification. The identical numeric constant is imported from the RRF.Physics.QuarkMasses sibling module.
proof idea
The definition is a direct numeric assignment of the PDG value 172690 with no lemmas or tactics applied.
why it matters
It supplies the benchmark for the top_mass_match theorem, which proves agreement to within 0.038 percent between the quarter-ladder prediction and this experimental value. The result supports the T12 quark-mass derivation and the phi-ladder structure in the Recognition framework. An open question remains explicit reconciliation with the parameter-free core mass model via QuarkCoordinateReconciliation.lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.