bosonic_dof_eq_poly
plain-language theorem explainer
At spatial dimension D = 3 the imported Standard Model bosonic degree count equals the polynomial 4D² − 2D − 2, recovering the familiar 28. Cosmology and unification bookkeeping that packages g_★ from frozen SM counts would cite this. The proof is a one-line native_decide check that both sides evaluate to 28.
Claim. With the forced spatial dimension $D = 3$ and the imported high-temperature Standard Model bosonic degree-of-freedom count $g_b$ (gauge plus Higgs, equal to 28), one has the exact arithmetic identity $g_b = 4D^2 - 2D - 2$.
background
The module FermionDOFGapBridge collects kernel-checked arithmetic identities that rewrite imported Standard Model relativistic degree-of-freedom counts in D-flavored notation. After the 2026-06-25 external review it explicitly does not claim to derive the SM spectrum: matter representations, the minimal-neutrino convention, and the Fermi–Dirac 7/8 weight remain imported physics.
Here $D$ is the spatial dimension forced by the T8 step of the forcing chain (Foundation.DimensionForcing), fixed at the natural number 3. The symbol bosonic_dof is the upstream Cosmology.GStarDerivation total of gauge plus Higgs degrees of freedom above the electroweak transition; its value is the standard SM bookkeeping number 28, not an RS prediction.
Sibling identities in the same file re-express the fermionic count 90 and the thermal weight 7/8, then assemble $g_\star = 28 + (7/8)\cdot 90 = 106.75$ at high temperature. The present lemma is the bosonic half of that packaging.
proof idea
Both sides are closed natural-number expressions once D is substituted: the left-hand side is the imported constant 28, and the right-hand side is $4\cdot 3^2 - 2\cdot 3 - 2 = 36 - 6 - 2 = 28$. The tactic native_decide discharges the equality by kernel evaluation; no intermediate lemmas are required.
why it matters
Inside Recognition Science this lemma is bookkeeping, not a derivation. It packages the frozen SM bosonic count into the same D-polynomial language used for the fermionic identity $90 = 2\cdot D^2(D+2)$ and the eight-tick weight $(2^D-1)/2^D$, so the assembled high-T identity $g_\star = 106.75$ can be written uniformly in D. Framework landmarks it touches are only T8 (D = 3) and the eight-tick octave $2^D = 8$; it does not invoke J-uniqueness, RCL, or the mass ladder.
No downstream theorem currently depends on it (used_by is empty). Its value is local honesty: the module doc and the declaration doc both state that the polynomial is a re-expression obtained after the target number is known, not an RS derivation of gauge or Higgs content. A genuine variable-D $g_\star(D)$ theory would still need matter representations at each D, which the repository does not supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.