fermionic_dof_eq_twice_gap
plain-language theorem explainer
The Standard Model fermionic degree-of-freedom count equals twice the D=3 dimension gap: 90 = 2 × 45. Cosmology and unification arguments that rewrite g_* through gap-flavored notation cite this identity. The proof is a one-shot native_decide check that both sides evaluate to the same natural number.
Claim. With spatial dimension $D = 3$, the imported Standard Model fermionic degree-of-freedom total equals twice the dimension gap at $D$: $g_f = 2 \cdot \mathrm{dimensionGap}(3)$. Explicitly $90 = 2 \times 45$, since $\mathrm{dimensionGap}(D) = D^2(D+2)$ and $g_f = n_{\mathrm{gen}} \times 30 = 3 \times 30$.
background
This module records exact arithmetic identities between imported Standard Model relativistic DOF counts and combinatorial quantities built from the forced spatial dimension $D = 3$ (T8 / DimensionForcing). It does not derive the SM spectrum; the module doc states that earlier "zero empirical inputs" language was overclaiming and has been removed.
The left-hand side fermionic_dof is the imported total $g_f = 90$ (quarks + charged leptons + neutrinos under the minimal-neutrino convention), assembled upstream in Cosmology.GStarDerivation. The right-hand side uses dimensionGap d := parityCount d * configDim d, which at $d = D = 3$ is $D^2(D+2) = 45$. The local $D$ is the same forced spatial dimension used throughout GapDerivation and AlphaDerivation.
The honest split is: RS contributes $D = 3$, the eight-tick period $2^D = 8$, and generation count 3; the SM representations, $g_f = 90$, the Fermi–Dirac $7/8$ weight, and high-$T$ $g_* = 106.75$ are imported physics.
proof idea
One-line kernel check: native_decide evaluates both closed natural-number expressions and confirms equality. No lemmas are invoked; both fermionic_dof and dimensionGap D reduce by unfolding to concrete numerals (90 and 45), so $90 = 2 \times 45$ is decided by computation.
why it matters
This is the central arithmetic bridge of FermionDOFGapBridge. Downstream, fermion_dof_gap_certificate packages it with dimensionGap D = 45, the $7/8$ weight identity, and the assembled $g_* = 106.75$. fermionic_matter_antimatter_split rewrites $90 = 45 + 45$ via this theorem (particle/antiparticle reading is interpretation only). g_star_via_gap substitutes the identity to obtain $g_* = 28 + (7/8)(2 \times 45)$, the gap-flavored form of the standard high-$T$ count.
In the Recognition framework it sits after T8 ($D = 3$) and the eight-tick octave, but only as a re-expression: the doc-comment is explicit that whether $90 = 2 \times D^2(D+2)$ is structural or accidental remains OPEN. No claim is made that RS derives the SM fermion content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.