quark_count
plain-language theorem explainer
Quark_count fixes the total number of quark flavors at six, matching the three-generation structure with isospin partners. Researchers deriving the CKM mass hierarchy in Recognition Science cite this when proving the φ-ladder assignments for up, down, strange, charm, bottom, and top quarks. It is introduced as a direct natural-number constant with no further reduction.
Claim. The total number of quark flavors is defined to be $6$.
background
The module treats the Standard Model as having six quarks whose masses span five orders of magnitude, from a few MeV to 172 GeV. In the RS reading these masses occupy fixed rungs on the φ-ladder, with unit mass set by $m_{unit} = φ^{-5}/8$. The definition supplies the integer count required by the master certificate that later asserts the rung list (u:8, d:9, s:14, c:17, b:22, t:30) and the geometric mass ratios.
proof idea
The declaration is a direct constant definition that assigns the value 6 to the natural number representing the quark count.
why it matters
This definition supplies the first clause of the CKMHierarchyFromPhiLadderCert structure, which collects the structural predictions for the quark mass hierarchy on the φ-ladder. It appears in the one-statement theorem ckm_hierarchy_one_statement that asserts quark_count = 6 together with the rung ordering and geometric mass ratios. The result closes the six-quark count in Track F7, linking directly to the mass formula $m_{quark}(k) = m_{unit} · φ^k$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.