ZOf_up_quarks
plain-language theorem explainer
The declaration establishes that the ZOf invariant equals 276 for each of the up, charm, and top quarks. Mass modelers cite it when grouping up-type fermions by shared Z values ahead of phi-ladder mass assignments. The proof is a one-line wrapper that invokes the definition of ZOf on each quark and discharges the resulting numerical claims by decision.
Claim. Let $ZOf(f)$ be the integer invariant on fermions defined by $ZOf(f) = 4 + q^2 + q^4$ where $q = tildeQ(f)$ for up-sector quarks. Then $ZOf(u) = 276$, $ZOf(c) = 276$, and $ZOf(t) = 276$.
background
The Quark Score Card module consolidates existing proofs for quark-sector facts in the Recognition Science mass model without adding new physics. It records that the three up-type quarks share the same ZOf value as one of its theorem-grade statements, alongside parallel facts for down quarks (ZOf = 24) and charged leptons (ZOf = 1332). The ZOf function itself is supplied by the upstream definition in RSBridge.Anchor: for any fermion f in the up or down sector, ZOf(f) equals 4 plus q squared plus q to the fourth, where q is tildeQ(f).
proof idea
The proof is a one-line wrapper that applies the definition of ZOf to each of the three quarks and uses the decide tactic to verify the three numerical equalities.
why it matters
This result supplies the shared ZOf = 276 fact used directly by charm_up_equal_Z, top_up_equal_Z, and the construction of QuarkScoreCardCert in quarkScoreCardCert_holds. It fills the module-level claim that u/c/t share ZOf = 276, which in turn supports the equal-Z anchor mass ratio being a pure phi-power of the rung difference. Within the Recognition framework the shared value anchors rung assignments on the phi-ladder for the up sector, consistent with the mass formula that places each fermion at yardstick times phi to the power of (rung minus 8 plus gap(Z)).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.