fermi_weight_is_tick_fraction
plain-language theorem explainer
At D=3 the available fermion tick count over the eight-tick period equals the Fermi-Dirac thermal weight: (8−1)/8 = 7/8. Anyone assembling the g_★ arithmetic identities in the fermion DOF gap bridge cites this equality. The proof is pure definitional unfolding plus kernel arithmetic; both sides are the same rational by construction.
Claim. With spatial dimension $D=3$ and eight-tick period $2^{D}=8$, the ratio of available fermion ticks to the period equals the $D$-dependent Fermi-Dirac weight: $(\mathrm{available\_ticks\_fermion})/8 = (2^{D}-1)/2^{D}$, i.e. $7/8=7/8$.
background
This module records exact arithmetic identities that relate imported Standard Model degree-of-freedom counts to combinatorial quantities at the forced spatial dimension $D=3$. It does not derive the SM spectrum. Upstream RS results used as fixed inputs are $D=3$ (T8 / DimensionForcing) and the eight-tick period $2^{D}=8$ (EightTick).
The Fermi-Dirac thermal weight $7/8$ is the standard high-temperature integral ratio for fermions versus bosons; it is imported physics, not an RS derivation. The spin-statistics exchange sign (fermion $-1$) is derived elsewhere in the repo, but the $7/8$ weight itself is not. Sibling definitions fix $D:=3$, eightTick$:=8$, and the $D$-flavored weight $(2^{D}-1)/2^{D}$.
The local claim is only that the tick fraction $(8-1)/8$ and the thermal weight $7/8$ are the same rational. The module doc is explicit: both sides match by construction; the equation records the numerical coincidence the §7 gloss uses, nothing more.
proof idea
One-step definitional proof. Unfold the four named constants (available_ticks_fermion, eightTick, fermi_dirac_weight_D, and $D$), then discharge the resulting rational equality by norm_num. No lemmas are applied; the kernel checks that both sides evaluate to $7/8$.
why it matters
Fills the middle arithmetic link in the module's honest split: the identities $90=2\times\mathrm{dimensionGap}(3)$, $7/8=(2^{3}-1)/2^{3}$, and the assembled $28+(7/8)\times 90=106.75$. Without this equality the §7 gloss that writes the Fermi weight as a tick fraction has no kernel-checked anchor.
Framework landmarks in play are T8 ($D=3$) and the eight-tick octave $2^{D}=8$ (T7). The result does not touch RCL, $J$-uniqueness, or the mass ladder. After the 2026-06-25 external review the module was re-scoped: earlier "CONFIRMED" / "zero empirical inputs" language was withdrawn. This theorem is the cleaned residual: a proved rational identity, not a derivation of $g_{\star}$ from RS premises. No downstream users are recorded yet; it stands as a leaf identity for the bridge narrative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.