charm_rung_eq
plain-language theorem explainer
The charm quark occupies rung 15 on the Recognition Science phi-ladder. Researchers deriving heavy-quark anchor masses from the RSBridge formula would cite this equality to fix the integer position without external mass data. The proof is immediate reflexivity against the explicit case in the rung definition.
Claim. $rung(c) = 15$, where $c$ is the charm quark in the Fermion enumeration and rung assigns each fermion its integer position on the mass ladder.
background
The module derives heavy-quark anchor-scale masses from the RSBridge formula massAtAnchor f = M0 * exp(((rung f : ℝ) - 8 + gap (ZOf f)) * log φ). The rung function is defined by cases on the Fermion inductive type, which enumerates the three up-type quarks, three down-type quarks, and leptons. Upstream definitions in AnchorPolicy and RSBridge.Anchor supply the matching case | .c => 15.
proof idea
The proof is a one-line wrapper that applies reflexivity to the explicit case for Fermion.c in the rung definition.
why it matters
This equality is packaged into the QuarkAnchorDerivationCert record, which certifies the complete set of heavy-quark rung and Z assignments. It supplies the rung input required by the massAtAnchor formula, placing charm at the phi-ladder position consistent with the eight-tick octave and self-similar scaling in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.