particle_antiparticle
plain-language theorem explainer
Defines the particle–antiparticle multiplicity as the natural number 2. Anyone assembling Standard Model relativistic fermion degrees of freedom cites it as the final factor in per-generation counts. The body is a one-line constant definition with no proof obligations.
Claim. The particle–antiparticle factor is the natural number $2$, counting a particle species together with its antiparticle.
background
The module performs textbook high-temperature bookkeeping for the Standard Model effective relativistic degrees of freedom $g_\star = g_b + (7/8)g_f = 106.75$, valid only for $T \gtrsim T_{\mathrm{EW}}$. Status is explicit: correct arithmetic over adopted SM content, not a novel Recognition Science prediction.
Fermion species enter $g_f$ with a product of flavor, color, chirality, and particle–antiparticle factors. The sibling constant chiralities is likewise fixed at 2 (left plus right). RS supplies the gauge group and the generation count 3; the matter representations and the minimal-neutrino convention are imported from standard physics.
This constant is the last multiplicative slot in those products: every Dirac fermion doubles once for its antiparticle.
proof idea
Pure definitional assignment: the natural-number constant is set equal to 2. No lemmas, tactics, or algebraic reduction are involved.
why it matters
It is the shared particle–antiparticle factor in every per-generation fermion DOF definition in the module: quarks ($2\times 3\times 2\times 2 = 24$), charged leptons ($1\times 2\times 2 = 4$), minimal neutrinos ($1\times 1\times 2 = 2$), and the Dirac-neutrino branch ($1\times 2\times 2 = 4$). Those products feed the global $g_f$ tally that yields $g_\star = 106.75$ (or 112 on the Dirac branch).
Within the Recognition framework this sits under Standard Model bookkeeping that consumes RS-derived inputs (SU(3)×SU(2)×U(1) from cube automorphisms, three generations from $D=3$) while leaving the representation content and the 7/8 thermal weight as imported physics. No open forcing-chain step is closed here; the declaration is pure assembly glue.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.