D4_prediction
plain-language theorem explainer
Counterfactual arithmetic at spatial dimension four: the dimension-gap expression equals 96 and the Fermi-Dirac weight equals 15/16. Anyone checking D-dependence of the fermion-DOF identities would cite the evaluation theorem this aliases. The proof is a one-line term wrapper; the old name is deprecated because it overstated epistemic status.
Claim. At spatial dimension $D=4$, the combinatorial dimension gap equals $96$ and the Fermi-Dirac thermal weight equals $15/16$ (i.e. $(2^4-1)/2^4$).
background
This module records kernel-checked arithmetic identities that re-express imported Standard Model degree-of-freedom counts in D-flavored notation. It does not derive the SM spectrum. The honest split is: SM matter representations, the minimal-neutrino $g_f=90$ convention, and the Fermi-Dirac integral weight $7/8$ are imported physics; $D=3$ (T8), the eight-tick period $2^D=8$, and generation count 3 are upstream RS results cited here, not re-proved.
The dimension gap is the combinatorial quantity that at $D=3$ equals 45, so that fermionic DOF $=2\times$ gap $=90$. The D-dependent Fermi-Dirac weight is $(2^D-1)/2^D$, which is $7/8$ at $D=3$ and $15/16$ at $D=4$. Assembled high-$T$ $g_\star=28+(7/8)\times 90=106.75$ is standard SM bookkeeping, machine-checked as an identity only.
The $D=4$ case is explicitly counterfactual: it displays how the same algebraic expressions scale with $D$, with no claim that any physical system realizes those values.
proof idea
One-line term wrapper: the statement is definitionally the conjunction proved by D4_evaluation. That evaluation discharges the two conjuncts by native_decide on the gap identity and by unfolding the weight definition plus norm_num on $15/16$. No extra reasoning appears at this alias.
why it matters
Sits in the module's arithmetic-certificate section (counterfactual $D=2$ and $D=4$ rows alongside the physical $D=3$ identities). It makes the pure D-dependence of gap and Fermi-Dirac weight inspectable next to the $D=3$ facts used in $g_\star$ assembly. Framework landmarks in view are T8 ($D=3$ forced) and the eight-tick octave $2^D$; the $D=4$ numbers are not predictions for nature.
The declaration is deprecated in favor of the evaluation theorem because the old name suggested a stronger claim than arithmetic re-expression. No downstream theorems currently depend on it (used_by empty). It closes no open derivation gap: deriving gauge reps, Higgs content, or the thermal integral from RS premises remains out of scope for this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.