quark_count_eq
plain-language theorem explainer
The Recognition Science model fixes the total number of quarks at exactly six to match three generations with up- and down-type partners under the phi-ladder assignment. Researchers deriving CKM mass hierarchies cite this count as the base for rung placement and geometric progression. The proof is a direct reflexivity step on the definition that introduces quark_count as the constant 6.
Claim. The canonical number of quarks equals 6, corresponding to three generations each with one up-type and one down-type partner on the phi-ladder.
background
The module CKMHierarchyFromPhiLadder derives quark masses from the phi-ladder forced by recognition geometry, with rung assignments fixed by SU(3)×SU(2)×U(1) structure on Q3. The sibling definition quark_count : ℕ := 6 encodes the canonical six-quark structure (3 generations × 2 isospin partners). Upstream rung definitions map specific fermions to ladder positions, for example RSBridge.Anchor.rung sends u to 4, c to 15, t to 21 and likewise for down-type quarks.
proof idea
Term-mode proof consisting of a single reflexivity application (rfl) to the definition of quark_count.
why it matters
This equality supplies the first field of the CKMHierarchyFromPhiLadderCert structure, the master certificate for Track F7 that also requires strict rung ordering and geometric mass ratios. It anchors the six-quark count presupposed by the phi-ladder mass formula m_quark(k) = m_unit · φ^k with m_unit = φ^{-5}/8. The certificate is the structural theorem closing the hierarchy derivation from Constants.phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.