D4_evaluation
plain-language theorem explainer
At spatial dimension 4 the combinatorial dimension gap equals 96 and the Fermi–Dirac weight equals 15/16. The result is purely counterfactual arithmetic showing D-dependence of the same formulas used at D=3; no physical 4D realization is claimed. Anyone checking the gap/weight identities against the physical D=3 case would cite it. The proof is a two-conjunct term: native decision for the gap and unfold-plus-norm_num for the weight.
Claim. The dimension gap at $d=4$ equals $96$, and the $d$-dependent Fermi–Dirac weight at $d=4$ equals $15/16$. Explicitly, $\mathrm{dimensionGap}(4)=4^{2}(4+2)=96$ and $(2^{4}-1)/2^{4}=15/16$.
background
The module FermionDOFGapBridge records exact arithmetic identities that re-express imported Standard Model degree-of-freedom counts in D-flavored notation. After external review it no longer claims to derive the SM spectrum: gauge representations, Higgs content, and the thermal 7/8 integral are imported; only the kernel-checked equalities are proved here.
Upstream, T8 forces spatial dimension $D=3$, and the eight-tick period is $2^{D}=8$. The dimension gap is the combinatorial quantity $\mathrm{dimensionGap}(d)=\mathrm{parityCount}(d)\cdot\mathrm{configDim}(d)$, equivalently $d^{2}(d+2)$. The Fermi–Dirac weight in this file is the pure power-of-two ratio $(2^{d}-1)/2^{d}$ (the physical 7/8 at $d=3$), not a derivation of spin-statistics.
This declaration evaluates those same expressions at the counterfactual value $d=4$, so the D-dependence is visible side-by-side with the physical $d=3$ identities (gap 45, weight 7/8) used in the $g_{\star}$ assembly.
proof idea
Term-mode pair proof. The left conjunct $\mathrm{dimensionGap},4=96$ is discharged by native_decide (closed natural-number arithmetic on the gap definition). The right conjunct unfolds fermi_dirac_weight_D to the ratio $(2^{4}-1)/2^{4}$ and finishes with norm_num, yielding $15/16$. No external lemmas beyond the in-module definitions are required.
why it matters
It anchors the counterfactual side of the D-dependence story in this unification bridge: the same formulas that give gap 45 and weight 7/8 at the forced $D=3$ (T8) evaluate to 96 and 15/16 at $d=4$. Downstream, D4_prediction is only a deprecated alias of this theorem, so the evaluation is the canonical citation.
Within Recognition Science the point is negative as much as positive. The module status text is explicit that these identities are re-expressions after the target numbers are known, not a derivation of $g_{\star}=106.75$ from RS premises. Displaying the $d=4$ values makes that honesty concrete: the arithmetic works for any $d$, while physics selects $D=3$ via DimensionForcing and the eight-tick octave. No open scaffold is closed here; the declaration is fully proved arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.