fermionWeight
plain-language theorem explainer
The fermionic entropy weight is the rational 7/8, equal to the Fermi–Dirac / Bose–Einstein integral ratio η(4)/ζ(4) = 1 − 2⁻³. Anyone building present-day g*s, the e± annihilation dilution factor, or the entropy-per-photon ratio cites this constant. It is a plain rational definition; the series and integral identities that justify the value live in sibling modules that import it.
Claim. The fermionic entropy weight is the rational number $7/8$. Equivalently, it is the ratio of the Fermi–Dirac to Bose–Einstein thermodynamic integrals $\int_0^\infty x^3/(e^x+1)\,dx \big/ \int_0^\infty x^3/(e^x-1)\,dx = \eta(4)/\zeta(4) = 1-2^{-3}$.
background
The EntropyPerPhoton module derives the present-day entropy-per-photon ratio $s/n_\gamma = \pi^4 g_{*s}/(45\zeta(3))$ in the window $(7.0393, 7.0396)$, replacing a bare $7.04$ constant in the baryogenesis lane. Three ingredients enter: a $\zeta(3)$ window, a $\pi^4$ window, and the arithmetic value $g_{*s}=43/11$ built from Standard Model particle content.
In that arithmetic, bosonic species contribute their polarization count directly, while fermionic species are weighted by $7/8$. The photon carries $2$ polarizations; $e^\pm$ carry $4$ fermionic degrees of freedom; three neutrino generations carry $6$. Before $e^\pm$ annihilation the plasma entropy dof is therefore $2+(7/8)\cdot 4=11/2$; after annihilation the photon temperature is diluted relative to neutrinos by $(T_\nu/T_\gamma)^3=4/11$.
The value $7/8$ is no longer a model input. Sibling modules prove $\eta(4)=(7/8)\zeta(4)$ at the series layer and $\int t^3/(e^t+1)=(7/8)\int t^3/(e^t-1)$ (both integrals closed: $\pi^4/15$ and $7\pi^4/120$) at the integral layer. Those modules import this definition, so the constant itself stays a plain rational.
proof idea
Plain definitional assignment: the rational literal $7/8$ is bound as a term of type $\mathbb{Q}$. No tactics, no lemmas, no computation. Justification that this rational equals the eta/zeta ratio and the Fermi/Bose integral ratio is deferred to the importing modules FermionWeight and FermionWeightIntegral.
why it matters
This constant is the single fermionic weight threaded through the entire $g_{*s}$ arithmetic. Downstream it appears in gBefore ($2+(7/8)\cdot 4$), dilutionCubed (which unfolds to $4/11$), gStarS, and the theorem gStarS_eq proving $g_{*s}=43/11$. The same value is the right-hand side of eta4_div_zeta4 and fermionWeight_eq_eta_zeta_ratio in Cosmology.FermionWeight, and of the integral identities fermi_div_bose_integral and fermi_integral_eq_weight_mul_bose in FermionWeightIntegral.
In the module narrative the upgrade from MODEL to THEOREM (2026-07-01) is exactly the move of $7/8$ from an unexplained input to a derived series/integral identity, while the particle-content counts (photon $2$, electron $4$, neutrino $6$) remain the only model data. That closes the third ingredient of the entropy-per-photon derivation used by the baryogenesis dynamical prefactor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.