fermi_dirac_weight_D
plain-language theorem explainer
Defines the Fermi-Dirac thermal weight as a function of spatial dimension d by the closed form (2^d − 1)/2^d. Anyone checking the g_star arithmetic identities or the D=2/D=4 counterfactuals in the fermion DOF gap bridge cites this. The body is a bare real-arithmetic expression, not a derived theorem.
Claim. For each natural number $d$, the Fermi-Dirac thermal weight is $w(d) = (2^d - 1)/2^d \in \mathbb{R}$. At the forced spatial dimension $d = 3$ this is exactly $7/8$.
background
This module records exact arithmetic identities that relate imported Standard Model degree-of-freedom counts to combinatorial quantities built from the forced spatial dimension $D = 3$ (T8). It does not derive the SM spectrum.
The Fermi-Dirac factor itself is imported standard statistical mechanics: the ratio of the relativistic fermion and boson energy-density integrals is $\int x^3/(e^x+1),dx,/,\int x^3/(e^x-1),dx = 1 - 2^{-3} = 7/8$ in 3+1 dimensions, i.e. $1 - 2^{-D}$ at $D = 3$. Lean does not prove that integral; it only packages the algebraic expression $(2^d-1)/2^d$ and checks its values at concrete $d$.
Sibling constants include the forced dimension $D := 3$ and the eight-tick period $2^D = 8$. The spin-statistics exchange sign is derived elsewhere in the repository; the $7/8$ thermal weight is not.
proof idea
Bare definition: the real expression $((2:\mathbb{R})^d - 1)/(2:\mathbb{R})^d$. No tactics, no lemmas. Downstream theorems unfold this def and discharge equalities by norm_num or native_decide.
why it matters
Supplies the weight factor in the assembled identity $28 + (7/8)\times 90 = 106.75$ that the module certificate checks. Immediate consumers include the exact evaluation at $D=3$ (equals $7/8$), the bookkeeping identity that the same number equals $(\mathrm{eightTick}-1)/\mathrm{eightTick}$, and the counterfactual evaluations at $d=2$ ($3/4$) and $d=4$ ($15/16$).
Framework landmarks in play are T8 ($D=3$) and the eight-tick octave $2^D=8$. The coincidence that $(2^D-1)/2^D$ can also be read as (tick period $-1$)/(tick period) is recorded only as a hypothesis-grade interpretation, not as a derivation from Recognition premises. Closing a true RS derivation of $g_\star$ would still require deriving the gauge representations, Higgs content, neutrino chirality, and the Fermi/Bose integral from RS axioms; none of that is claimed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.