top_Z_eq
plain-language theorem explainer
The theorem states that the ZOf function applied to the top quark evaluates to exactly 276. Researchers deriving RS-native heavy quark masses would cite this when completing the anchor certification bundle. The proof is a direct reflexivity step that follows immediately from evaluating the ZOf definition on the top quark in the up sector.
Claim. For the top quark, the integer $Z$ computed by the ZOf function equals 276.
background
The QuarkAnchorDerivation module derives heavy-quark anchor-scale masses from the RSBridge formula massAtAnchor f = M0 * exp(((rung f : ℝ) - 8 + gap (ZOf f)) * log φ), with no PDG masses entering. The Fermion inductive type includes the top quark constructor t. The ZOf function returns an integer: for up-sector fermions it is 4 + qq + qqqq where q = tildeQ f; for down-sector it is the same form; leptons and neutrinos use reduced expressions.
proof idea
This is a one-line wrapper that applies reflexivity to the definition of ZOf on the top quark constructor.
why it matters
The result feeds directly into the quarkAnchorDerivationCert_holds theorem, which assembles rung and Z equations for charm, bottom, and top to certify the full QuarkAnchorDerivationCert. It supplies the top-quark entry in the RS-native mass formula, consistent with the phi-ladder mass formula and the eight-tick octave of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.