charm_anchor_eq_massAtAnchor
plain-language theorem explainer
The equality confirms that the native charm quark anchor mass is identical to the general RS massAtAnchor formula evaluated at the charm fermion. Researchers deriving RS-native quark masses on the phi-ladder would cite this to verify definitional consistency for the charm case. The proof is a direct reflexivity that follows from the definition of charm_anchor_native as massAtAnchor Fermion.c.
Claim. The native charm anchor mass equals the RS anchor mass for the charm fermion: $m_c^{anchor} = M_0 exp(((rung_c - 8 + gap(Z_c)) log phi))$, where the left side is defined directly as the right side applied to the charm fermion.
background
The module derives heavy-quark anchor-scale masses from the RSBridge formula massAtAnchor(f) = M0 * exp(((rung f : R) - 8 + gap(ZOf f)) * log phi), producing RS-native dimensionless results with no PDG masses. charm_anchor_native is the definition that sets this formula for the charm fermion. Fermion is the inductive type containing the constructor c for charm, alongside other quarks and leptons. Upstream, massAtAnchor supplies the exponential phi-ladder expression, while rung and ZOf extract the integer rung and gap(Z) correction for each fermion.
proof idea
The proof is a one-line wrapper that applies reflexivity. It holds immediately because charm_anchor_native is defined exactly as massAtAnchor Fermion.c, so the two sides are definitionally equal.
why it matters
This theorem completes the charm case inside the heavy quark anchor derivation, aligning the native definition with the general massAtAnchor function from the RSBridge. It supports the module goal of obtaining all heavy-quark anchors directly from the phi-ladder formula without external data. No downstream theorems are listed yet, but the result contributes to the consistency of Recognition Science mass derivations across the eight-tick octave and D=3 framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.