bottom_down_equal_Z
plain-language theorem explainer
The theorem establishes that the down and bottom quarks share the same ZOf label of 24 on the Recognition Science phi-ladder. Researchers checking down-type quark generation spacing in mass predictions would cite this when confirming consistency with the phi-ladder assignments. The proof extracts the explicit Z values from the ZOf_down_quarks lemma and rewrites them directly to equality.
Claim. $Z(d) = Z(b)$, where $Z$ assigns the integer rung label on the phi-ladder to each fermion and down-type quarks receive the common value 24.
background
The Quark Score Card module consolidates theorem-grade facts for the quark sector. ZOf_down_quarks supplies the explicit assignments Z(d) = 24, Z(s) = 24, Z(b) = 24. The rung function from AnchorPolicy and Constants maps each quark name to its integer position on the phi-ladder, with equal-Z fermions sharing anchor mass ratios that are pure phi-powers of the rung difference.
proof idea
The term proof obtains the triple from ZOf_down_quarks, discards the middle component, and rewrites the first and third components to obtain equality of the Z labels for d and b.
why it matters
This fills the down-generation spacing entry in the scorecard, confirming d/s/b share ZOf = 24. It supports the claim that equal-Z fermions have anchor mass ratios given by phi-powers, consistent with the phi fixed point and eight-tick octave in the forcing chain. No downstream uses appear yet; absolute mass matching within PDG bands remains open pending the bridge equivalence theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.