fermiEntropyIntegrand
plain-language theorem explainer
Defines the Fermi–Dirac entropy integrand σ_F(t)=t²[−f ln f−(1−f)ln(1−f)] with occupation f=1/(e^t+1). Cosmologists deriving s=(4/3)ρ/T for a massless fermion gas cite it as the microscopic entropy-density kernel. Pure definitional encoding of the binary entropy of the FD distribution times t²; no proof content.
Claim. For each real $t$, the Fermi–Dirac entropy integrand is $\sigma_F(t)=t^2\bigl[-f\ln f-(1-f)\ln(1-f)\bigr]$, where $f=1/(e^t+1)$ is the Fermi–Dirac occupation number.
background
The module derives the radiation identity $s=(4/3)\cdot\rho/T$ for a massless quantum gas from the microscopic entropy functional of quantum statistics, rather than taking the $4/3$ factor as a thermodynamic input. Dimensionless energy is $t=E/T$. For Fermi–Dirac statistics the occupation is $f=1/(e^t+1)$; the entropy density kernel is the binary Shannon entropy of that occupation, multiplied by $t^2$.
The Bose counterpart uses $\sigma_B(t)=t^2[(1+f)\ln(1+f)-f\ln f]$ with $f=1/(e^t-1)$. Both sit next to the energy kernels $t^3/(e^t\pm 1)$. Pointwise identities later split each entropy integrand into energy kernel plus logarithmic kernel (Fermi: $\sigma_F(t)=t^3/(e^t+1)+t^2\ln(1+e^{-t})$).
proof idea
Definition only. The body multiplies $t^2$ by the binary-entropy expression $-f\ln f-(1-f)\ln(1-f)$ with $f=1/(e^t+1)$ written out in place. No lemmas, no tactics.
why it matters
Supplies the fermionic entropy kernel whose integral is the content of the module's Fermi theorems. Downstream: fermi_entropy_pointwise rewrites it as energy kernel plus log kernel; fermi_entropy_integral_value evaluates $\int_0^\infty\sigma_F=7\pi^4/90$; fermi_entropy_eq_four_thirds_energy gives $s=(4/3)\rho/T$ for massless fermions; fermi_div_bose_entropy and fermi_entropy_eq_weight_mul_bose place the $7/8$ fermionic weight at the entropy-functional layer (not only energy). NeutrinoDilution.radiationEntropy builds plasma entropy density as $(g/2\pi^2)T^3\int\sigma$ with this integrand for the fermionic piece. Closes a MODEL step in the $\eta_B$ chain: the $4/3$ and $7/8$ factors are no longer assumed inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.