bottom_raw_far_below_PDG
plain-language theorem explainer
The theorem proves that the raw bottom-quark mass in eV computed from the current non-mass dimensional bridge lies more than eighteen orders of magnitude below the PDG value. Mass-sector auditors in the Recognition Science framework cite this result when documenting the incompleteness of the heavy-quark closure. The proof is a direct numerical check obtained by unfolding the two constant definitions and applying norm_num.
Claim. Let $m_b^{raw}$ be the raw bottom-quark mass in eV obtained from the current bridge and $m_b^{PDG}$ the PDG mass in eV. Then $m_b^{raw} < m_b^{PDG}/10^{18}$.
background
This theorem sits inside the Heavy Quark Full-Closure Obstruction module, whose purpose is to record the numerical gap between raw masses derived from the neutron-lifetime/Fermi route (via $E_{coh,SI} approx 2.4101 times 10^{-16}$ eV) and the observed PDG values. The raw value is produced by scaling the RS-native massAtAnchor for bottom (approximately 8248.93) by that coherence energy; the PDG anchor is fixed at 4.18 GeV. The module states explicitly that these raw SI masses lie many orders of magnitude below the PDG masses and therefore function only as an audit certificate, not as a first-principles derivation.
proof idea
The proof is a one-line wrapper that unfolds the definitions of bottom_raw_eV and bottom_PDG_eV, then applies norm_num to discharge the numerical inequality.
why it matters
The result is collected directly into the HeavyQuarkClosureObstructionCert structure (together with the corresponding charm and top statements and the exponent-mismatch lemma), which certifies that the current bridge plus massAtAnchor does not derive the heavy-quark GeV masses. This forces the recognition that a further mass-sector bridge must still be proved. Within the broader framework it underscores the separation between the T0-T8 dimensional chain and the phi-ladder mass construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.