fermi_weight_in_D4
plain-language theorem explainer
At spatial dimension parameter d = 4 the D-flavored Fermi–Dirac weight equals 15/16. Anyone checking the counterfactual arithmetic of the fermion thermal factor against the physical d = 3 case (7/8) would cite this. The proof is a one-line unfold of the closed form (2^d−1)/2^d followed by numeric normalization.
Claim. The D-parameterized Fermi–Dirac thermal weight at $d = 4$ equals $15/16$: $(2^4 - 1)/2^4 = 15/16$.
background
This module records exact arithmetic identities that rewrite imported Standard Model degree-of-freedom counts in D-flavored notation. It does not derive the SM spectrum. The Fermi–Dirac thermal weight is the standard integral ratio, imported here as the closed form $(2^d-1)/2^d$; at the forced spatial dimension $D = 3$ (T8 / DimensionForcing) this is the familiar $7/8$.
The local definition fermi_dirac_weight_D is that closed form as a function of a natural-number dimension parameter. Physical bookkeeping uses $d = D = 3$; the present statement evaluates the same expression at the counterfactual value $d = 4$. Upstream, $D := 3$ is the spatial dimension forced by the recognition chain (T8), and the eight-tick period is $2^D = 8$.
proof idea
Unfold the definition of the D-parameterized Fermi–Dirac weight (the map $d \mapsto (2^d-1)/2^d$), then discharge the resulting rational equality $15/16 = 15/16$ by norm_num. No lemmas beyond the definition are required.
why it matters
Sits in the honest split of FermionDOFGapBridge: proved kernel-checked arithmetic on imported thermal weights, not an RS derivation of $g_\star$. The physical identity used downstream in the module is $7/8 = (2^3-1)/2^3$ at $D = 3$; this $d = 4$ evaluation is the matching counterfactual check that the same formula yields $15/16$.
It anchors the D-flavored bookkeeping against the forced dimension $D = 3$ (T8) and the eight-tick octave $2^D = 8$ (T7), without claiming that $d = 4$ is physical. After the 2026-06-25 re-scope, such identities exist only to keep the arithmetic machine-checked; closing a true RS derivation of $g_\star = 106.75$ would still require deriving gauge representations, Higgs content, and the thermal integral from RS premises, none of which is done here. Currently unused by other declarations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.