D2_prediction
plain-language theorem explainer
Counterfactual arithmetic at spatial dimension two: the dimension gap equals 16 and the Fermi–Dirac weight equals 3/4. Anyone checking D-dependence of the fermion DOF identities would cite the non-deprecated evaluation theorem instead. The proof is a one-line alias of that evaluation; the old name overstated epistemic status and is deprecated.
Claim. At spatial dimension $D = 2$, the dimension gap equals $16$ and the Fermi–Dirac thermal weight equals $3/4$.
background
This module records exact arithmetic identities that re-express imported Standard Model degree-of-freedom counts in D-flavored notation. It does not derive the SM spectrum. After external review the file was re-scoped: SM representations, the minimal-neutrino convention, and the Fermi/Bose thermal integrals are imported; RS contributes D = 3, the eight-tick period 2^D, and the generation count from upstream forcing.
The dimension gap is the combinatorial quantity parityCount(d) × configDim(d), equal to d²(d+2). The D-dependent Fermi–Dirac weight is written (2^D − 1)/2^D. At the physical value D = 3 these recover the familiar 90 fermionic DOF factor and the 7/8 weight that assemble into g★ = 106.75; the identities are kernel-checked re-expressions, not derivations of those target numbers.
The D = 2 case is counterfactual bookkeeping only. The weight 3/4 matches the relativistic 2+1-dimensional thermal integral; it is not a claim about nonrelativistic 2D conductors.
proof idea
One-line term wrapper: the statement is definitionally the conjunction already proved by the D = 2 evaluation theorem. That evaluation discharges the gap equality by native decision and the weight equality by unfolding the D-dependent Fermi–Dirac formula and normalizing the rational 3/4. No extra tactics or lemmas are introduced here.
why it matters
The declaration exists only as a deprecated alias. The old name suggested a predictive claim; the module doc and the evaluation theorem’s comment withdraw that reading. The live content is the counterfactual pair (gap 16, weight 3/4), which displays pure D-dependence of the same arithmetic used at D = 3 for the g★ assembly 28 + (7/8)×90 = 106.75.
It sits in the Unification fermion-DOF bridge beside the physical D = 3 identities and the equally non-physical D = 4 display case. Upstream landmarks are T8 (D = 3 forced) and the eight-tick octave 2^D; nothing here forces D = 2 or claims a physical 2D realization. No downstream theorems currently depend on this alias (used_by is empty); cite the evaluation theorem directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.