Quark
plain-language theorem explainer
The six standard model quark flavors are enumerated as an inductive type with decidable equality and finite cardinality six. Recognition Science modelers cite this enumeration to link the particle content to the six faces of a three-dimensional cube. The declaration is a direct inductive definition with six constructors that automatically derives the finite type instance.
Claim. The set of quark flavors is the finite set $Q = {u, d, s, c, b, t}$ equipped with decidable equality and cardinality six.
background
The CubeFaceUniversality module establishes that the number 6 equals the face count of the 3-cube via the Euler characteristic $V - E + F = 8 - 12 + 6 = 2$. The HasCubeFaceCount predicate asserts that a type has cardinality exactly 6, and the Quark inductive type supplies one instance of this count. The module collects parallel 6-fold structures across domains, all attributed to spatial dimension $D = 3$.
proof idea
This is an inductive definition with six constructors. The deriving clauses for DecidableEq, Repr, BEq, and Fintype generate the required instances automatically, so that downstream theorems obtain the cardinality by unfolding HasCubeFaceCount and deciding the equality.
why it matters
This definition supplies the quark enumeration required by CubeFaceUniversalityCert and the theorems quark_has_6 and quark_lepton_sum. It realizes the T8 step of the forcing chain by fixing $D = 3$, which forces the face count to 6. The structure appears in fermion counts and mass ladder derivations downstream in BaselineDerivation and QuarkVerification modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.