top_raw_eV
plain-language theorem explainer
The definition supplies the raw top-quark mass in eV obtained from the Recognition Science massAtAnchor under the neutron-lifetime bridge. Auditors of the heavy-quark sector cite this constant when measuring the gap to PDG values. It is a direct numerical assignment with no derivation steps inside the module.
Claim. The raw top-quark mass in electron-volts computed from the current bridge equals $2.1544198712797816 times 10^{-11}$.
background
The module records the numerical obstruction to full heavy-quark closure from the existing non-mass dimensional bridge. It employs E_coh_SI approximately 2.4101e-16 eV taken from the neutron-lifetime route together with RS-native massAtAnchor values (top approximately 89392.14). The resulting raw SI masses lie many orders of magnitude below PDG masses, so the present bridge plus massAtAnchor does not derive the observed GeV-scale heavy-quark masses. This is an audit certificate, not a physics theorem, whose purpose is to block misreading of scorecards as first-principles derivations.
proof idea
The declaration is a direct numerical definition that assigns the floating-point constant 2.1544198712797816e-11 to the identifier.
why it matters
The constant is referenced by the HeavyQuarkClosureObstructionCert structure, whose doc-comment states there is no single universal extra φ-exponent among the three evaluated heavy-quark channels under the current bridge. It likewise supports the theorem top_raw_far_below_PDG that unfolds the definition and applies norm_num to establish the inequality. Within the Recognition framework the value underscores the requirement for an additional mass-sector bridge beyond the eight-tick octave and D=3 landmarks, consistent with the mass formula on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.