fermionic_matter_antimatter_split
plain-language theorem explainer
The imported SM fermionic DOF count equals twice the dimension gap at D=3, written additively as 90=45+45. Cited by anyone assembling g_star or checking the fermion half of the thermal count in RS units. Proof is a one-line reduction through the twice-gap identity, closed by omega.
Claim. The total fermionic degrees of freedom equal the sum of two copies of the dimension gap at the forced spatial dimension $D=3$: $g_f=\Delta(D)+\Delta(D)$.
background
This module records exact arithmetic identities that re-express the imported Standard Model fermionic count $g_f=90$ in D=3 combinatorial language. Spatial dimension $D$ is forced to 3 by the upstream T8 result (Foundation.DimensionForcing). The dimension gap $\Delta(D)$ is the combinatorial quantity tied to $D^2(D+2)$ in GapDerivation; at $D=3$ it evaluates to 45.
The fermionic DOF total itself is imported particle content: quarks, charged leptons, and neutrinos across three generations (Cosmology.GStarDerivation.fermionic_dof). Module status is explicit after the 2026-06-25 rescope: these identities do not derive the SM spectrum. They only verify that $90=2\times\Delta(3)$ holds as kernel-checked arithmetic on already-known counts.
proof idea
Invokes the sibling lemma fermionic_dof_eq_twice_gap, which already states fermionic_dof = 2 * dimensionGap D, then closes with omega. The present claim is only the additive spelling of that equality ($a+a$ rather than $2a$), so the tactic needs nothing beyond unfolding the arithmetic.
why it matters
Packages the 45+45 reading of the fermionic count that feeds the assembled identity $28+(7/8)\times 90=106.75$ for $g_\star$ inside FermionDOFGapBridge and GStarDerivation. Framework landmarks in play are T8 ($D=3$) and the eight-tick period $2^D=8$, both cited as upstream RS results rather than re-proved here.
The doc-comment is careful: the particle/antiparticle interpretation of the two halves is interpretive only. Nothing derives matter-antimatter from the dimension gap. After the external-review rescope, the module no longer claims a pure $D=3$ derivation of the SM DOF spectrum; the identity is a re-expression of a known number.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.