mass_top_exp
plain-language theorem explainer
The declaration supplies the observed top quark mass of 172690 MeV as the benchmark for the quarter-ladder prediction at rung 5.75. Researchers verifying the Recognition Science quark mass derivation cite it when confirming relative error below 0.05 percent. It enters as a bare numeric constant with no internal computation.
Claim. The experimental top quark mass is defined as $m_t^exp = 172690$ MeV.
background
Module T12 formalizes the Quarter-Ladder Hypothesis: quarks share the lepton structural base (Sector Gauge B=-22, R0=62) but sit at quarter-integer rungs on the phi-ladder. The top quark occupies the ideal position R=5.75=23/4. The mass formula yardstick * phi^(rung-8+gap(Z)) supplies the predicted value; this definition records the measured counterpart for error bounds.
proof idea
Direct constant definition that assigns the integer 172690 with no lemmas or tactics applied.
why it matters
It anchors the downstream theorem top_mass_match, which proves the predicted interval (172722,172755) MeV satisfies relative error less than 0.0005. The definition completes the T12 step in the quark mass chain and supplies the concrete datum needed to close the match against the eight-tick octave and phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.