fermi_dirac_from_eight_tick
plain-language theorem explainer
At the forced spatial dimension D = 3, the Fermi–Dirac thermal weight (2^D − 1)/2^D equals (eight-tick − 1)/eight-tick. Both sides are 7/8 because the eight-tick period is defined as 2^D. Anyone assembling the g_* arithmetic identities from the eight-tick cadence would cite this. The proof is two definitional rewrites followed by norm_num.
Claim. Let $D = 3$ be the forced spatial dimension and let $T_8 = 2^D$ be the eight-tick period. Then the Fermi–Dirac weight at $D$ equals $(T_8 - 1)/T_8$. Equivalently, $(2^D - 1)/2^D = (T_8 - 1)/T_8$ holds as a numerical identity at $D = 3$ (both sides equal $7/8$).
background
This module records exact arithmetic identities that re-express Standard Model degree-of-freedom counts in D-flavored notation. Per the module header, the Fermi–Dirac thermal integral weight 7/8 is imported standard physics (the relativistic Fermi/Bose integral ratio), not an RS derivation; what is proved here is only that this number equals $(2^3 - 1)/2^3$.
Upstream, T8 forces spatial dimension $D = 3$, and the eight-tick octave is the period $T_8 := 2^D = 8$ (T7). The local definition D is that forced value 3; eightTick is that period. The Fermi–Dirac weight at general $D$ is the combinatorial ratio $(2^D - 1)/2^D$; specializing at $D = 3$ recovers the familiar 7/8 factor used in high-$T$ $g_*$ bookkeeping.
The module explicitly separates imported SM content (representations, minimal-neutrino $g_f = 90$, the 7/8 integral) from RS-derived inputs ($D = 3$, eight-tick, generation count) and from the kernel-checked arithmetic proved on top of both.
proof idea
Term/tactic hybrid, three steps. Rewrite the left-hand side with the specialized identity that the weight at $D = 3$ is $7/8$. Rewrite the right-hand side with the definitional fact that the eight-tick period equals 8. Close by norm_num, which checks $7/8 = (8-1)/8$ in $\mathbb{R}$. No nontrivial lemmas: pure definitional bookkeeping once $D$ and the eight-tick constant are fixed.
why it matters
Fills the numerical bridge between the eight-tick cadence ($T_8 = 2^D$, T7) and the imported Fermi–Dirac factor 7/8 that appears in the assembled identity $28 + (7/8)\times 90 = 106.75$ for high-$T$ $g_$. Together with the sibling identities fermionic_dof = 2 × dimensionGap(3) and the $g_$ assembly, it lets the kernel certify that the D = 3 combinatorial package matches the standard thermal count.
The doc-comment is explicit: this equation is bookkeeping, not new physics. After the 2026-06-25 external review the module was re-scoped to drop overclaims ("pure D=3 formula", "zero empirical inputs", 2D-conductor confirmation). Downstream use count is currently zero; the result exists so the arithmetic spine of the unification DOF bridge is fully kernel-checked rather than asserted in prose.
Framework landmarks: T7 (eight-tick octave $2^3$), T8 ($D = 3$). It does not touch RCL, J-uniqueness, or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.