fermion_antifermion_total
plain-language theorem explainer
The declaration establishes that the total number of fermion species, counting each of the six quark flavors and six lepton types together with their antiparticles, equals 24. Particle physicists working inside the Recognition Science framework would cite this count when verifying that standard-model fermions obey the cube-face enumeration for three spatial dimensions. The proof is a direct rewriting step that substitutes the two prior cardinality results for the quark and lepton types.
Claim. $2 · (6 + 6) = 24$, where the two 6's are the cardinalities of the six quark flavors and the six lepton flavors under the cube-face count for spatial dimension 3.
background
The CubeFaceUniversality module asserts that the number 6 recurs across domains because a 3-cube has exactly six faces (V-E+F = 8-12+6 = 2), yielding the relation 6 = 2·3. The Quark inductive type enumerates the six flavors up, down, strange, charm, bottom, top; the Lepton inductive type enumerates electron, muon, tau, nuE, nuMu, nuTau. Two upstream theorems establish each cardinality by unfolding HasCubeFaceCount and deciding the equality to 6.
proof idea
The proof is a one-line wrapper that rewrites with the two cardinality theorems quark_has_6 and lepton_has_6, which unfold HasCubeFaceCount and decide each type has cardinality 6, immediately producing the doubled total of 24.
why it matters
This theorem completes the fermion side of the C15 Cube-Face Universality claim, confirming that the standard-model fermions fit the 6-count pattern required by D = 3. It aligns with the framework's derivation of spatial dimension from the eight-tick octave and self-similar fixed point. No downstream uses are recorded, but the result supports broader cross-domain counting arguments that rely on the same face-level enumeration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.