fermi_weight_in_D2
plain-language theorem explainer
At spatial dimension d = 2 the Fermi-Dirac thermal weight (2^d − 1)/2^d equals 3/4 exactly. Anyone auditing the counterfactual arithmetic of the fermion/boson energy-density ratio in 2+1 dimensions would cite this. The proof is a one-line unfold of the defining rational expression followed by numeric normalization.
Claim. The Fermi-Dirac thermal weight at spatial dimension $d = 2$ equals $3/4$: $(2^{2} - 1)/2^{2} = 3/4$.
background
This module records exact arithmetic identities that re-express Standard Model degree-of-freedom counts in D-flavored notation. The Fermi-Dirac thermal weight is the imported statistical-mechanics ratio of fermion to boson thermal energy-density integrals. In D spatial dimensions the closed form is written $(2^{D}-1)/2^{D}$; at the physical value D = 3 this is the familiar 7/8.
The definition fermi_dirac_weight_D d is exactly that rational expression in a natural-number argument d. The present theorem evaluates it at the counterfactual point d = 2. The module header stresses that the match with the relativistic thermal integral in 2+1 dimensions (namely 1 − 2^{−2}) is arithmetic only: it is not the nonrelativistic 2D electron-gas result, and no experimental claim via 2D conductors is made.
Upstream, D = 3 itself is forced by Foundation.DimensionForcing (T8), and the eight-tick period 2^D = 8 is forced by Foundation.EightTick. Those results are cited, not re-proved, here.
proof idea
One-line tactic proof. Unfold the definition of the weight, which is the real rational ((2 : ℝ)^d − 1) / (2 : ℝ)^d, instantiate at d = 2, and discharge the resulting numeric equality 3/4 = 3/4 by norm_num. No lemmas beyond the definition are required.
why it matters
The theorem sits in the Fermion DOF / Dimension-Gap bridge as the d = 2 counterfactual companion to the physical evaluation at D = 3 (which yields 7/8). Together with the sibling identities 90 = 2 × dimensionGap(3) and 28 + (7/8)×90 = 106.75, it documents that the D-flavored re-expression of the imported Fermi weight is kernel-checked at nearby integers, not only at the physical point.
It does not advance an RS derivation of g_star or of the thermal integral itself: those remain imported standard physics. Its role is honesty of scope after the 2026-06-25 external review: the arithmetic is exact and machine-checked, while the provenance of the 7/8 factor and of the SM representations stays explicitly external. No downstream consumers are presently wired; the result is a local sanity check on the weight family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.