charm_anchor_native
plain-language theorem explainer
The definition assigns the RS-native charm quark anchor mass to the evaluation of massAtAnchor at the charm fermion. Researchers deriving heavy quark scales in Recognition Science cite it to establish the baseline without PDG input. It is a direct definition that instantiates the exponential mass formula for the specific charm case.
Claim. The RS-native charm anchor mass is $m_c := M_0 * exp(((rung(c) - 8 + gap(ZOf(c))) * log φ))$, where $c$ is the charm constructor in the Fermion type, rung(c) its ladder position, ZOf(c) its effective charge, $M_0$ the base scale, and φ the golden ratio.
background
The module derives heavy-quark anchor masses from the RSBridge formula massAtAnchor f = M0 * exp(((rung f : ℝ) - 8 + gap (ZOf f)) * log φ). The Fermion inductive type enumerates standard-model fermions with constructor c for charm. Results remain RS-native and dimensionless with no PDG masses entering the derivation.
proof idea
This is a direct definition that applies the massAtAnchor function to Fermion.c.
why it matters
It supplies the charm anchor value used by charm_anchor_eq_massAtAnchor and heavy_anchor_positive. The QuarkAnchorDerivationCert structure records the associated rung 15 and Z 276 for charm. This step applies the phi-ladder mass formula to the charm quark, advancing the heavy-quark derivation in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.