charm_Z_eq
plain-language theorem explainer
The declaration establishes that ZOf evaluates to 276 on the charm quark constructor in the Fermion type. Researchers assembling the RS-native heavy-quark mass anchors would cite this when building the derivation certificate. The proof is immediate reflexivity on the definition of ZOf after matching the up-sector case and the charge parameter for charm.
Claim. Let $Z(f)$ denote the integer assigned to fermion $f$ by $Z(f)=4+q^2+q^4$ for up-sector quarks, where $q=tilde{Q}(f)$. Then $Z(c)=276$ for the charm quark $c$.
background
The QuarkAnchorDerivation module obtains heavy-quark anchor masses from the RSBridge formula massAtAnchor f = M0 * exp(((rung f : ℝ) - 8 + gap (ZOf f)) * log φ) with no PDG input. ZOf is the function that returns an integer for each fermion: 4 + q² + q⁴ on up or down sectors, q² + q⁴ on leptons, and 0 on neutrinos, with q drawn from tildeQ. Fermion.c is the charm constructor in the inductive type that also contains d, s, b, u, t and the leptons.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of ZOf after the match on sectorOf Fermion.c and the value of tildeQ for charm.
why it matters
This equality supplies the Z-component for charm inside quarkAnchorDerivationCert_holds, which packages rung and Z values for the three heavy quarks into a single certificate. It therefore completes the discrete input to the phi-ladder mass formula for the charm rung, consistent with the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain. No open scaffolding questions are touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.