dimensionGap_at_D3
plain-language theorem explainer
At spatial dimension D = 3 the dimension-gap polynomial evaluates to 45. Unification and g_star bookkeeping cite this as the exact integer bridge between D-flavored combinatorics and the imported fermionic DOF count 90 = 2 × 45. The proof is a one-line native_decide on the closed form d²(d+2).
Claim. With spatial dimension $D = 3$, the dimension gap $D^{2}(D+2)$ equals $45$.
background
In this module the spatial dimension is fixed at the RS value $D = 3$ forced by T8 (DimensionForcing). The local dimension-gap function is the elementary polynomial $\mathrm{dimensionGap}(d) = d^{2}(d+2)$; the in-module doc records the evaluation $9 \times 5 = 45$ at $d = 3$. Upstream GapDerivation uses a related product form (parity count times configuration dimension) that agrees on $\mathbb{N}$ at $D = 3$.
The module itself is deliberately re-scoped: it proves only kernel-checked arithmetic identities linking imported Standard Model degree-of-freedom counts to these $D = 3$ combinatorial quantities. It does not derive the SM spectrum, gauge representations, or the Fermi–Dirac thermal weight from RS premises. Those counts and the $7/8$ weight are imported; $D = 3$ and the eight-tick period $2^{D} = 8$ are the RS inputs cited from Foundation.
proof idea
One-line computational proof: native_decide evaluates $\mathrm{dimensionGap}, D$ with $D := 3$ and the definition $d^{2}(d+2)$, confirming equality to the numeral 45. No lemmas are invoked beyond definitional unfolding and decidable arithmetic on $\mathbb{N}$.
why it matters
This is the first bullet of the packaged certificate fermion_dof_gap_certificate, which assembles the exact identities $\mathrm{dimensionGap}(3) = 45$, fermionic DOF $= 90 = 2 \times 45$, Fermi–Dirac weight $(2^{3}-1)/2^{3} = 7/8$, and the high-$T$ assembly $28 + (7/8)\times 90 = 106.75$. Downstream bookkeeping therefore treats 45 as the integer hinge between the T8-forced dimension and the imported $g_{f} = 90$ convention.
In the broader RS chain it sits under T8 ($D = 3$) and the eight-tick octave $2^{D} = 8$, but only as arithmetic re-expression: the module doc is explicit that obtaining $g_{\star} = 106.75$ as a true RS derivation would still require deriving representations, Higgs content, chiral neutrinos, and the thermal integral from RS premises, none of which is claimed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.