bottom_raw_eV
plain-language theorem explainer
The definition bottom_raw_eV supplies the raw SI mass in electron-volts for the bottom quark obtained by scaling the RS-native massAtAnchor value by the coherence energy E_coh_SI. Mass-sector auditors cite this constant when checking that the current bridge produces values many orders below PDG data. It is introduced by direct numerical assignment with no derivation steps.
Claim. The raw bottom-quark mass in electron-volts is defined as $1.988055339759384 × 10^{-12}$.
background
The Heavy Quark Full-Closure Obstruction module records that the Recognition Science mass formula, using E_coh_SI ≈ 2.4101e-16 eV from the neutron-lifetime route together with massAtAnchor values (bottom ≈ 8248.93), yields raw SI masses far below PDG values. This prevents the massAtAnchor constants from being read as a complete first-principles derivation of GeV-scale quark masses. The module defines parallel raw constants for charm, bottom and top and imports only Mathlib.
proof idea
Direct numerical assignment of the constant 1.988055339759384e-12. No lemmas or tactics are invoked.
why it matters
This definition is referenced by the theorem bottom_raw_far_below_PDG, which establishes bottom_raw_eV < bottom_PDG_eV / 1e18, and by the structure HeavyQuarkClosureObstructionCert that certifies the obstruction across the three heavy-quark channels. It implements the audit role stated in the module documentation and marks the open requirement for an additional mass-sector bridge beyond the current phi-ladder anchor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.