charm_raw_far_below_PDG
plain-language theorem explainer
The theorem proves that the raw charm mass in eV from the current non-mass bridge lies more than 18 orders of magnitude below the PDG value. Auditors of the Recognition Science mass sector cite it inside the heavy-quark closure obstruction certificate to document the gap. The proof is a direct numerical comparison obtained by unfolding the two constant definitions and normalizing.
Claim. Let $m_{charm,raw}$ be the raw charm mass in eV computed from the non-mass bridge and $m_{charm,PDG}$ the PDG value. Then $m_{charm,raw} < m_{charm,PDG}/10^{18}$.
background
The module records the numerical obstruction preventing full heavy-quark closure from the existing bridge. Raw masses are obtained by scaling RS-native massAtAnchor values with the coherence energy $E_{coh,SI}$ taken from the neutron-lifetime route, producing charm_raw_eV = 1.2006170448628038e-12. The PDG reference is supplied by the sibling definition charm_PDG_eV = 1.27e9. The module states explicitly that the present bridge plus massAtAnchor does not derive the GeV-scale masses and functions only as an audit certificate.
proof idea
The proof is a term-mode one-liner. It unfolds the definitions of charm_raw_eV and charm_PDG_eV, then applies norm_num to discharge the numerical inequality.
why it matters
The result supplies the charm_below field of HeavyQuarkClosureObstructionCert, which aggregates the three heavy-quark obstructions together with the required-exponent split. It implements the audit role described in the module documentation, blocking any claim that the current T0-T8 forcing and phi-ladder already close the mass sector. The certificate therefore flags the need for an additional mass-sector bridge before the framework can be read as deriving the observed heavy-quark spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.