pith. sign in
def

charm_raw_eV

definition
show as:
module
IndisputableMonolith.Masses.HeavyQuarkFullClosureObstruction
domain
Masses
line
28 · github
papers citing
none yet

plain-language theorem explainer

The definition supplies the raw SI charm quark mass in eV obtained from the Recognition Science massAtAnchor value scaled by the current coherence energy bridge. Auditors of the mass sector cite it when checking the gap to observed PDG values. It is introduced as a direct numerical assignment with no internal derivation or lemmas.

Claim. Let $m_c^raw$ be the raw charm quark mass in electron-volts computed from the Recognition Science anchor without additional phi-exponent adjustment. Then $m_c^raw = 1.2006170448628038 times 10^{-12}$.

background

The module records numerical obstructions to closing the heavy-quark masses under the existing non-mass dimensional bridge. It imports the coherence energy E_coh_SI approximately 2.4101e-16 eV from the neutron-lifetime route and the RS-native massAtAnchor values (charm approximately 4981.65). The raw SI masses are formed by scaling these anchors and are shown to lie many orders of magnitude below PDG values, serving as an audit certificate rather than a derivation.

proof idea

Direct numerical definition with no lemmas or tactics. The constant is assigned verbatim from prior computation of the massAtAnchor scaled by E_coh_SI.

why it matters

This supplies the concrete input for the comparison theorem charm_raw_far_below_PDG and the structure HeavyQuarkClosureObstructionCert, which records that no single extra phi-exponent closes all three heavy-quark channels. It implements the module's stated audit role: preventing scorecards from being read as first-principles derivations of the GeV-scale masses. It highlights the open requirement for a further mass-sector bridge.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.