ZOf_down_quarks
plain-language theorem explainer
The declaration establishes that the ZOf invariant equals 24 for the down, strange, and bottom quarks. Mass modelers working on the Recognition Science phi-ladder cite it to confirm that these three fermions share a common rung offset. The proof is a one-line wrapper that splits the conjunction and reduces each equality by direct computation from the definition of ZOf.
Claim. $ZOf(d) = 24 ∧ ZOf(s) = 24 ∧ ZOf(b) = 24$
background
ZOf is the integer label assigned to each fermion by the formula 4 + q² + q⁴ in the down sector, where q = tildeQ(f) is the charge quantum number. The QuarkScoreCard module consolidates existing proofs without introducing new physics and records that d/s/b share ZOf = 24 as one of the theorem-grade facts supporting the phi-ladder mass formula. The upstream definition of ZOf appears in both RSBridge.Anchor and Masses.RSBridge.Anchor and evaluates the label directly from the fermion sector and charge.
proof idea
The proof is a one-line wrapper that applies refine to split the three-way conjunction into separate goals and then uses decide to evaluate each equality by unfolding ZOf and reducing the arithmetic.
why it matters
This result is invoked by the equal-Z theorems for strange and bottom quarks and by the main quarkScoreCardCert_holds certificate. It fills the module claim that d/s/b share ZOf = 24, which anchors the rung spacing used in the Recognition framework mass formula yardstick * phi^(rung - 8 + gap(Z)). The open question it touches is the absolute mass match that still requires the gap(ZOf) correction from RSBridge.Anchor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.