charm_PDG_eV
plain-language theorem explainer
charm_PDG_eV supplies the PDG experimental mass of the charm quark at 1.27 GeV expressed in electron-volts. Mass auditors in Recognition Science cite it when quantifying the gap between raw model outputs and measured values under the current bridge. The declaration is a direct numerical assignment with no reduction steps required.
Claim. The PDG mass of the charm quark is defined as $1.27 times 10^9$ eV.
background
The module records the numerical obstruction to full heavy-quark closure from the existing non-mass dimensional bridge. It deploys E_coh_SI from the neutron-lifetime route together with RS-native massAtAnchor values for charm, bottom and top. This definition supplies the experimental benchmark, as the module states: the raw SI masses are many orders of magnitude below the PDG masses, so the current bridge plus massAtAnchor does not derive the heavy-quark GeV masses.
proof idea
The declaration is a direct numerical definition. Downstream theorems unfold it to perform the required inequality comparisons.
why it matters
It anchors the comparisons inside charm_raw_far_below_PDG and the HeavyQuarkClosureObstructionCert structure. The structure concludes there is no single universal extra phi-exponent among the three heavy-quark channels under the current bridge. This supplies the audit certificate that prevents scorecards from being misread as first-principles derivations and flags the need for a further mass-sector bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.