quark_lepton_sum
plain-language theorem explainer
Quark and lepton families each contribute six types, summing to twelve fermions in the Standard Model. Cross-domain researchers in Recognition Science cite this when linking particle counts to the six faces of the three-dimensional cube. The term proof substitutes the pre-established cardinality results for each family.
Claim. $|Quark| + |Lepton| = 12$, where Quark enumerates the six quark flavors and Lepton the six lepton flavors.
background
The module establishes Cube-Face Universality for cross-domain counts of six, arising from the 3-cube having six faces. Quark is defined as an inductive type with constructors up, down, strange, charm, bottom, top. Lepton similarly lists electron, muon, tau, nuE, nuMu, nuTau. Upstream theorems quark_has_6 and lepton_has_6 prove that each satisfies HasCubeFaceCount, which encodes the cardinality being six.
proof idea
The proof proceeds by rewriting the cardinalities using the theorems quark_has_6 and lepton_has_6, which directly supply the value six for each.
why it matters
This theorem supplies the quark and lepton components to the cubeFaceUniversalityCert, which aggregates the six-counts across quarks, leptons, cortical layers, Braak stages, and robotic degrees of freedom. It fills the particle-physics instance in the C15 Cube-Face Universality claim, where six equals the product of cube dimension two and spatial dimension three. The result supports the broader pattern of recurrence of this count in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.