quark_has_6
plain-language theorem explainer
The theorem asserts that the Quark inductive type, enumerating the six Standard Model quark flavors, has cardinality exactly 6 and therefore satisfies the cube-face count property. Recognition Science modelers and particle physicists cite it when assembling the total fermion count of 12 in the Standard Model. The proof is a one-line wrapper that unfolds the cardinality definition and decides the equality.
Claim. The inductive type Quark with constructors up, down, strange, charm, bottom, top satisfies Fintype.card Quark = 6.
background
The module CrossDomain.CubeFaceUniversality states that the count 6 equals the number of faces of a 3-cube and recurs across RS domains for spatial dimension D = 3. HasCubeFaceCount is the predicate Fintype.card T = 6 on any Fintype T. Quark is the inductive type whose six constructors list the quark flavors. The declaration supplies one concrete instance of the module's structural claim that 6 = 2·3.
proof idea
The proof is a one-line wrapper that unfolds HasCubeFaceCount and applies the decide tactic to confirm the cardinality of Quark equals 6.
why it matters
This theorem supplies the quark instance inside cubeFaceUniversalityCert. It is invoked by quark_lepton_sum to obtain the Standard Model fermion total of 12 and by fermion_antifermion_total to reach 24 when antiparticles are included. It instantiates the framework observation that 6 = D_cube · D_spatial for D = 3, as recorded in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.