D2_evaluation
plain-language theorem explainer
Counterfactual arithmetic at spatial dimension two: the dimension gap equals 16 and the Fermi–Dirac weight formula equals 3/4. Cited by anyone auditing D-dependence of the fermion DOF/gap identities, or checking the withdrawn 2D-conductor claim. Proof is a two-conjunct term: native decision on the gap equality, unfold-plus-norm_num on the weight.
Claim. At spatial dimension $d=2$, the dimension gap equals $16$ and the $D$-dependent Fermi–Dirac weight equals $3/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. After external review, earlier overclaims ("CONFIRMED in 2D conductors", "zero empirical inputs") were withdrawn; the honest split is imported SM counts and thermal weights versus RS-derived $D=3$, eight-tick period $2^D$, and generation count.
The dimension gap is the combinatorial quantity $\mathrm{dimensionGap}(d)=\mathrm{parityCount}(d)\cdot\mathrm{configDim}(d)$, equivalently $d^2(d+2)$. The $D$-dependent Fermi–Dirac weight is the pure power-of-two ratio $(2^d-1)/2^d$. At the physical value $d=3$ these give 45 and $7/8$; the present theorem evaluates the same expressions at the counterfactual $d=2$.
Upstream, $D=3$ is forced by T8 (DimensionForcing). The physical certificate assembles $90=2\times\mathrm{dimensionGap}(3)$ and $g_\star=28+(7/8)\times 90=106.75$. The $d=2$ case is kept only to display $D$-dependence.
proof idea
Term-mode pair constructor, no tactics beyond the two conjuncts. Left conjunct: native_decide discharges the closed natural-number equality $\mathrm{dimensionGap},2=16$ (since $2^2(2+2)=16$). Right conjunct: unfold the definition of the $D$-dependent Fermi–Dirac weight, then norm_num reduces $(2^2-1)/2^2$ to $3/4$.
why it matters
Supplies the $d=2$ row of the D-dependence table used by fermion_dof_gap_certificate, which packages the physical $d=3$ identities (gap 45, fermionic DOF 90, weight $7/8$, $g_\star=106.75$). Also the sole body of the deprecated alias D2_prediction (old name overstated epistemic status).
Framework landmark: T8 forces physical $D=3$; this theorem is explicitly counterfactual and exists to show how gap and weight scale with $D$. The doc-comment records that $3/4$ matches the relativistic $2+1$-dimensional thermal integral, while the earlier claim of confirmation by 2D conductors was a category error (nonrelativistic Fermi gases with chemical potential are a different object) and is withdrawn. No open scaffold: the result is fully proved arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.