fermion_dof_gap_certificate
plain-language theorem explainer
Bundles six kernel-checked arithmetic identities linking the imported SM fermionic DOF count (90) to the D=3 dimension gap (45), the Fermi–Dirac weight 7/8, and g_*=106.75, plus a D=2 counterfactual. Cosmology and unification authors cite it as a single certificate that the gap/DOF arithmetic closes. Proof is a term-mode refine packing six prior lemmas.
Claim. At spatial dimension $D=3$, the dimension gap equals $45$, the total fermionic degrees of freedom equal $2\times 45=90$, the Fermi–Dirac weight is $7/8$, and the assembled effective relativistic count is $g_*=106.75$. Equivalently, half the fermionic DOF equals the gap. As a counterfactual check at $D=2$: the gap is $16$ and the weight is $3/4$.
background
This module sits in the Unification layer and, after external review, is scoped strictly as arithmetic on imported Standard Model counts versus RS combinatorial quantities. It does not derive the SM spectrum.
The spatial dimension $D$ is the T8-forced value $3$. The dimension gap is the combinatorial quantity $\mathrm{dimensionGap}(d)=\mathrm{parityCount}(d)\cdot\mathrm{configDim}(d)$, which expands to $d^2(d+2)$; at $d=3$ this is $45$. Fermionic DOF is the imported SM total $g_f=90$ (three generations, minimal-neutrino convention) from the relativistic DOF and $g_*$ modules.
The Fermi–Dirac weight $7/8$ is the standard thermal-integral ratio, re-written here as $(2^D-1)/2^D$ at $D=3$. The assembled $g_*=28+(7/8)\times 90=106.75$ is the usual high-$T$ SM value. Upstream RS inputs cited but not re-proved: $D=3$, the eight-tick period $2^D=8$, and generation count $3$.
proof idea
Term-mode proof: a single refine ⟨...⟩ that packages six already-proved conjuncts.
dimensionGap_at_D3supplies $\mathrm{dimensionGap}(3)=45$.fermionic_dof_eq_twice_gapsupplies $g_f=2\times\mathrm{dimensionGap}(3)$.fermi_dirac_weight_D3supplies the weight $7/8$ at $D=3$.g_star_D3_eqsupplies the assembled $g_*=106.75$.matter_phi45_complementaritysupplies the half-DOF identity $g_f/2=\mathrm{dimensionGap}(3)$.D2_evaluationsupplies the counterfactual pair at $D=2$: gap $16$ and weight $3/4$.
No new arithmetic is performed in the certificate itself; it is a conjunction wrapper over sibling lemmas.
why it matters
In the Recognition framework this certificate is the honest bridge between the T8-forced spatial dimension $D=3$ (and the related eight-tick $2^D=8$ cadence) and the textbook high-temperature $g_*=106.75$ count. It records that the imported fermionic DOF $90$ is exactly twice the combinatorial gap $D^2(D+2)=45$, and that the Fermi–Dirac factor matches $(2^D-1)/2^D$.
The module header is explicit about what remains open: deriving gauge representations, the Higgs doublet, chiral neutrino content, and the thermal integral from RS premises would be required before $g_*=106.75$ could be called an RS derivation. None of that is claimed here. With used_by empty, the declaration is presently a terminal audit artifact rather than an intermediate lemma in a larger proof chain. It closes the arithmetic side of the fermion-DOF/gap story after the 2026-06-25 rescope that removed overclaims about pure $D=3$ formulas and zero empirical inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.