top_PDG_eV
plain-language theorem explainer
The definition supplies the Particle Data Group experimental mass of the top quark as 172.69 GeV converted to electronvolts. Mass auditors in the Recognition Science framework cite this constant when testing whether the present dimensional bridge plus massAtAnchor values can close the heavy quark sector. It enters as a direct numerical constant with no internal computation or derivation.
Claim. The Particle Data Group value for the top quark mass is $172.69$ GeV, or equivalently $172.69 times 10^9$ eV.
background
The module records the numerical obstruction preventing full heavy-quark closure under the current non-mass dimensional bridge. It draws on the coherence energy E_coh_SI approximately 2.4101e-16 eV obtained from the neutron-lifetime route together with the RS-native massAtAnchor values (charm approximately 4981.65, bottom approximately 8248.93, top approximately 89392.14). These anchors produce raw SI masses many orders of magnitude below the PDG figures, so the existing bridge does not derive the observed GeV-scale masses. The module states explicitly that the content is an audit certificate, not a physics theorem, to prevent misreading of the scorecards as first-principles derivations.
proof idea
The declaration is a direct numerical assignment of the PDG top quark mass in eV units.
why it matters
The constant is referenced by the structure HeavyQuarkClosureObstructionCert, which establishes that no single universal extra phi-exponent exists among the three heavy-quark channels under the current bridge, and by the theorem top_raw_far_below_PDG that quantifies the gap for the top channel. It thereby supports the audit preventing the mass scorecards from being read as derivations. Within the Recognition framework it touches the mass formula yardstick times phi to the power (rung minus 8 plus gap(Z)) on the phi-ladder and underscores the open requirement for a further mass-sector bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.