fermion_boltzmann
plain-language theorem explainer
The fermionic Boltzmann factor is the exact rational 7/8, the ratio of Fermi-Dirac to Bose-Einstein contributions to relativistic energy density when integrated against T^3. Cosmologists deriving the high-temperature effective degrees of freedom g_⋆ cite this constant when weighting fermionic helicity states against bosonic ones. It is a one-line rational definition with no proof obligations.
Claim. The fermionic Boltzmann weight equals $7/8$, the exact ratio of the Fermi-Dirac to Bose-Einstein contribution to the relativistic energy density integrated against $T^3$.
background
In early-universe thermodynamics the relativistic energy density is proportional to $g_\star T^4$. Bosons enter with weight 1; fermions enter with the Fermi-Dirac integral factor $7/8$ relative to the Bose-Einstein integral, both taken against the $T^3$ measure that appears after integrating the distribution functions.
This module derives the standard high-$T$ value $g_\star = 106.75$ from explicit Standard Model helicity counts forced by the $Q_3$ chord-cube content, rather than treating $106.75$ as a hand-entered real. Bosonic degrees of freedom total 28 (12 gauge generators times 2 polarisations, plus 4 real Higgs scalars); fermionic degrees of freedom total 90 (quarks, charged leptons, and neutrinos across three generations).
The factor $7/8$ is the sole remaining coefficient needed to assemble $g_\star = g_b + (7/8) g_f$ as an exact rational.
proof idea
One-line definition: the constant is introduced as the rational literal $7/8$ on $\mathbb{Q}$. No lemmas, tactics, or analytic evaluation are required; the physical content is recorded in the doc-comment and consumed algebraically by the downstream assembly of $g_\star$.
why it matters
Parent definitions and theorems are the derived $g_\star$ rational and its equality proof. The assembly is $g_\star = g_b + (7/8) g_f = 28 + (7/8)\cdot 90 = 427/4 = 106.75$, with the equality discharged by unfolding the particle-content counters and a single native_decide. That derived value is then bridged to the existing baryogenesis constant so the high-$T$ effective DOF used in baryon-asymmetry calculations is no longer an opaque float. Within Recognition Science this closes a bookkeeping step: SM content forced by the $Q_3$ structure, plus the classical Boltzmann weight, yields an exact rational rather than a decimal input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.