fermionic_dof_eq
plain-language theorem explainer
The imported Standard Model fermionic degree-of-freedom total equals 90. Cosmology and SM g_star certificates, and the eta_B rung bridge, cite this equality as a kernel-checked integer fact. The proof is a one-step native_decide on the closed natural-number definition; no analytic argument is required.
Claim. The total fermionic relativistic degree-of-freedom count equals $90$. Equivalently, with three generations and $30$ fermionic DOF per generation, $n_{\mathrm{gen}}\times(\mathrm{DOF}/\mathrm{gen})=3\times 30=90$, and this matches twice the $D=3$ dimension gap: $90=2\times D^{2}(D+2)|_{D=3}=2\times 45$.
background
This module records exact arithmetic identities between imported Standard Model degree-of-freedom counts and combinatorial quantities forced at spatial dimension $D=3$. After external review it was re-scoped: the identities are kernel-checked re-expressions of known integers, not a derivation of the SM spectrum from Recognition Science premises.
Upstream, $D:=3$ is the forced spatial dimension (T8 / DimensionForcing). The dimension gap at $D=3$ evaluates to $D^{2}(D+2)=45$. The fermionic DOF total is defined in the GStar path as the sum of quark, charged-lepton, and neutrino contributions under the minimal-neutrino convention, giving the textbook count $72+12+6=90$. Generation count $3$ is identified with $D$ (Q₃ face pairs) elsewhere; the $7/8$ Fermi–Dirac thermal weight is the standard integral ratio and is imported, not derived here.
Local siblings package the same arithmetic as $n_{\mathrm{gen}}\times(\mathrm{DOF}/\mathrm{gen})=3\times 30$ and as $2\times\mathrm{dimensionGap}(3)$. The honest split is: SM representations and $g_f=90$ are imported; $D=3$, the eight-tick period $2^D=8$, and the statistics sign are RS-derived upstream; only the integer equalities are proved in this file.
proof idea
One-line tactic proof: native_decide. The left-hand side is a closed natural-number definition (sum of fixed quark, charged-lepton, and neutrino DOF constants, or equivalently $3\times 30$), so the kernel reduces both sides to the numeral $90$ and discharges equality by computation. No rewrite chain or upstream lemma application is needed in this copy of the statement; the parallel Cosmology.GStarDerivation proof instead unfolds and rewrites the three sector equalities to the same numeral.
why it matters
The equality is the integer hinge for several downstream certificates. fermionic_half_equals_gap uses it to show that half the fermionic DOF equals the $D=3$ dimension gap ($45$), the stated bridge that matter and antimatter each carry one full gap worth of fermions. eta_B_rung_from_fermionic_eq rewrites through $90$ to obtain the rung value $-44$. In GStarDerivation and StandardModel.RelativisticDOF it feeds gStarDerivationCert, g_star_derived_eq, and fermionic_traces_to_Q3, assembling the high-$T$ identity $28+(7/8)\times 90=106.75$.
Framework landmarks in play are only the forced $D=3$ (T8) and the combinatorial gap $D^{2}(D+2)$; the match $90=2\times 45$ is recorded because it is exact. The module doc is explicit that whether the match is structural or accidental remains OPEN: no derivation of gauge representations, Higgs content, or chiral neutrinos from RS premises is claimed here or elsewhere in the bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.