bottom_PDG_eV
plain-language theorem explainer
The definition supplies the Particle Data Group experimental value for the bottom quark mass in electronvolts. Auditors of the Recognition Science mass bridge cite it to measure the shortfall between the phi-ladder anchor prediction and observed data. It is introduced as a plain numerical constant with no derivation steps or lemmas.
Claim. The Particle Data Group value for the bottom quark rest mass is $4.18 times 10^9$ eV.
background
This module records the numerical gap between the current non-mass dimensional bridge and the observed heavy-quark masses. It combines the coherent energy scale from the neutron-lifetime route with Recognition Science native massAtAnchor values (bottom approximately 8248.93) to produce raw SI masses many orders of magnitude below experiment. The bottom_PDG_eV entry supplies the experimental benchmark used in the comparison theorems that follow.
proof idea
The definition is a direct numerical assignment of the PDG bottom quark mass in eV. No lemmas are applied and no tactics are executed; it functions as a constant reference value for the obstruction calculations.
why it matters
The value feeds the bottom_below field of the HeavyQuarkClosureObstructionCert structure and the bottom_raw_far_below_PDG comparison theorem. It supports the audit conclusion that no single extra phi-exponent closes the heavy-quark channels under the present bridge, consistent with the Recognition Science mass formula on the phi-ladder. The module prevents misreading of the scorecards as a complete first-principles derivation of the GeV-scale masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.