dof_includes_three_gen
plain-language theorem explainer
Three particle generations contribute exactly three units in the face-pair bookkeeping that feeds the relativistic DOF count g_★. Anyone assembling the structural baryon asymmetry η_B ∝ J_CP/g_★ from RS particle content would cite this. The equality is definitional: a one-line reflexivity proof.
Claim. Evaluating the face-pair count at three yields three: the generation index $3$ contributes three units to the degrees-of-freedom tally. In other words, the three Standard Model generations enter the relativistic DOF count used for the structural baryon asymmetry.
background
This module treats the baryon-to-photon ratio η_B under an honest split: a proved sign theorem (η_B > 0 from J_CP > 0 plus Sakharov), a structural scaffold η_B ∝ J_CP/g_★ that is numerically ~500× too large because the washout constant is open, and a separate φ-rung hypothesis φ^{-44}(1-φ^{-8})².
Here g_★ is the effective number of relativistic degrees of freedom at the electroweak temperature. In the RS ledger it is SM bookkeeping built from the RS-sourced gauge group and generation count (ParticleGenerations, Gray-code chirality, CKM-from-cube). The face-pair count is the local arithmetic that records how many generation slots enter that tally.
Upstream, the Jarlskog invariant supplies the CP source and the sphaleron package (κ_sph = 3/4 from Q_3 topology, dimensionless rate κ_sph α_W^5) supplies B+L violation; neither is needed for this equality, which is pure DOF bookkeeping.
proof idea
One-line term proof by rfl. Both sides reduce definitionally to the numeral 3, so no lemmas are invoked. The declaration only pins that the face-pair function, evaluated at the generation index three, is definitionally three.
why it matters
In electroweak baryogenesis the structural skeleton is η_B ∝ ε_CP/g_★ with ε_CP ∝ J_CP. This lemma records that the three generations forced by the cube/Gray-code chain actually enter the g_★ side of that ratio, rather than being an external SM assumption.
It sits among the module siblings that build g_★ and eta_B_structural; the module header stresses that only the sign of η_B is derived content, while the magnitude scaffold and the separate φ^{-44}(1-φ^{-8})² rung match remain distinct objects. No downstream theorem currently depends on it (used_by is empty), so it is a local bookkeeping anchor inside the DOF assembly, not a load-bearing step of the forcing chain T0–T8.
It does not close the open washout/Boltzmann-transport gap flagged in the module status tags.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.