strange_down_equal_Z
The declaration establishes that the integer label assigned to the down quark equals the label assigned to the strange quark. Researchers grouping fermions by shared Z-labels for phi-ladder mass predictions in Recognition Science would cite this result. The proof extracts the relevant pair from the conjunction that fixes the label at 24 for all down-sector quarks and rewrites the two components.
claimLet $Z(f)$ be the integer label for fermion $f$ given by $Z(f)=4+q^2+q^4$ with $q$ the tilde-charge of $f$ in the down sector. Then $Z$ of the down quark equals $Z$ of the strange quark.
background
The Quark Score Card module consolidates existing proofs for the quark sector in Phase 0 of the physical derivation plan. It records theorem-grade facts such as the shared Z-label of 24 for down, strange, and bottom quarks without introducing new physics. The Z label is computed from the sector and tilde-charge via the formula that yields 24 for each down-sector quark.
proof idea
The term proof obtains the conjunction from the upstream ZOf_down_quarks theorem that fixes the label at 24 for down, strange, and bottom quarks, then rewrites the two relevant components to obtain the desired equality.
why it matters in Recognition Science
This result supports the scorecard claim that down-type quarks share the Z-label 24, which enters the anchor mass ratio theorem for equal-Z fermions as a pure phi-power of the rung difference. It fills the equal-Z grouping step in the Recognition Science framework where shared labels determine mass relations on the phi-ladder. The module notes that absolute mass matches within PDG bands remain open pending the bridge equivalence theorem.
scope and limits
- Does not compute absolute quark masses in MeV.
- Does not incorporate gap(Z) corrections from the RSBridge.
- Does not address up-sector or lepton Z-labels.
- Does not prove the phi-power mass ratios themselves.
formal statement (Lean)
66theorem strange_down_equal_Z : ZOf .d = ZOf .s := by
proof body
Term-mode proof.
67 obtain ⟨hd, hs, _⟩ := ZOf_down_quarks
68 rw [hd, hs]
69