top_raw_far_below_PDG
plain-language theorem explainer
The raw top-quark mass obtained from the current non-mass bridge equals 2.154e-11 eV and therefore lies more than eighteen orders of magnitude below the PDG value 172.69 GeV. Mass-sector auditors cite the inequality to certify that the existing phi-ladder bridge cannot yet produce the observed heavy-quark spectrum. The proof is a one-line term that unfolds the two numeric constants and lets norm_num discharge the comparison.
Claim. $m_{top,raw} < m_{top,PDG}/10^{18}$, where $m_{top,raw} := 2.1544198712797816×10^{-11}$ eV is the value returned by the present massAtAnchor construction and $m_{top,PDG} := 172.69×10^9$ eV is the experimental central value.
background
The module records a numerical obstruction to full heavy-quark closure. It imports the RS-native massAtAnchor values (charm ≈ 4981.65, bottom ≈ 8248.93, top ≈ 89392.14) together with the coherence energy E_coh_SI ≈ 2.4101e-16 eV taken from the neutron-lifetime route. These inputs produce raw SI masses many orders of magnitude below the PDG GeV-scale values, so the current dimensional bridge plus massAtAnchor does not derive the observed spectrum. top_raw_eV and top_PDG_eV are the concrete numeric constants for the top sector.
proof idea
The proof is a one-line term wrapper. It unfolds the two definitions top_raw_eV and top_PDG_eV, then applies norm_num to evaluate the resulting concrete inequality 2.1544198712797816e-11 < 172.69e9 / 1e18.
why it matters
The theorem supplies one of the three concrete witnesses required by heavyQuarkClosureObstructionCert_holds, the audit certificate that prevents scorecards from being read as first-principles derivations. It documents the gap that any future mass-sector bridge must close and therefore belongs to the obstruction side of the Recognition Science mass-ladder program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.