phaseSpaceDensity_congr_pos
plain-language theorem explainer
If two dimensionless kernels agree on every positive argument, their three-dimensional massless phase-space densities coincide at fixed degeneracy and temperature. Cosmology proofs that swap Bose/Fermi log or energy kernels for partition-function expressions cite this congruence. The argument is almost-everywhere integral equality: the kernels may differ only at k = 0, a null set.
Claim. Fix degeneracy $g\in\mathbb{R}$ and temperature $T>0$. Let $K_1,K_2:\mathbb{R}\to\mathbb{R}$ satisfy $K_1(t)=K_2(t)$ whenever $t>0$. Then the grand-canonical phase-space densities in three spatial dimensions agree: $$\frac{g}{(2\pi)^3}\int_{\mathbb{R}^3} T\,K_1(\|k\|/T)\,dk = \frac{g}{(2\pi)^3}\int_{\mathbb{R}^3} T\,K_2(\|k\|/T)\,dk.$$
background
The module StatisticsKernels rebuilds the Bose/Fermi pressure and energy kernels from a single-mode grand partition function at $\mu=0$. The only inputs are the Gibbs weight $e^{-n t}$ and the occupancy sets ($n\in\mathbb{N}$ for bosons, $n\in{0,1}$ for fermions). Partition functions, $\ln Z$ pressure kernels, mean occupations, and $t\langle n\rangle$ energy kernels are all derived rather than postulated.
Upstream, phaseSpaceDensity is the grand-canonical integral of one massless sector in $d$ spatial dimensions: degeneracy $g$, temperature $T$, dimensionless kernel $K$ at $E/T$ with $E=|k|$, and mode density $1/(2\pi)^d$. Pressure uses $K(t)=\mp\ln(1\mp e^{-t})$; energy density uses $K(t)=t/(e^t\mp 1)$.
Here $d=3$ is fixed, matching the forced spatial dimension in the Recognition chain. The lemma is the measure-theoretic glue that lets two pointwise-on-$(0,\infty)$ presentations of $K$ define the same integral.
proof idea
Unfold the definition of the phase-space density. The prefactor $g/(2\pi)^3$ and the factor $T$ match on both sides, so it remains to show the integrals of $K_1(|k|/T)$ and $K_2(|k|/T)$ over Euclidean $3$-space agree.
Apply almost-everywhere integral congruence. The singleton ${0}$ has Lebesgue measure zero. Off that null set, $|k|>0$, hence $|k|/T>0$ by positivity of $T$. The hypothesis then rewrites $K_1(|k|/T)$ as $K_2(|k|/T)$ pointwise a.e., and the integrals coincide.
why it matters
This is the technical bridge into the two module capstones. plasmaPressure_from_partitionFunction replaces the old log kernels by $\ln Z_B$ and $\ln Z_F$ inside the phase-space integral, recovering the $\eta_B$-chain plasma pressure as pure grand-canonical $T\ln Z$ from Gibbs weights and occupancy sets alone. plasmaEnergy_from_occupation likewise swaps $t\cdot\langle n\rangle$ for the classical energy kernels, so plasma energy is the integral of mode energy times mean occupation.
Without a.e. congruence, those rewrites would be blocked wherever the algebraic identities for $Z$ or $\langle n\rangle$ are stated only for $t>0$ (the physical regime $E/T>0$). The lemma closes that gap in $D=3$ massless sectors and keeps the StatisticsKernels provenance ledger honest: log and energy kernels are no longer independent MODEL inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.