boseEntropyIntegrand
plain-language theorem explainer
Defines the Bose–Einstein entropy integrand σ_B(t)=t²[(1+f)ln(1+f)−f ln f] with occupation number f=1/(e^t−1). Cosmology and statistical-mechanics arguments cite it as the microscopic density whose integral yields s=(4/3)ρ/T for a massless boson gas. The body is a direct noncomputable encoding of that classical kernel; no proof is required.
Claim. For real $t$, the Bose–Einstein entropy integrand is $\sigma_B(t)=t^2\bigl[(1+f)\ln(1+f)-f\ln f\bigr]$, where the occupation number is $f=1/(e^t-1)$.
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 integrals are written in the variable $t=E/T$.
For bosons the occupation number is $f=1/(e^t-1)$. The entropy density kernel is the standard expression $\sigma_B(t)=t^2[(1+f)\ln(1+f)-f\ln f]$. A parallel Fermi–Dirac kernel $\sigma_F$ is defined beside it. Upstream entropy notions in the repo (defect entropy, horizon microstate log, Boltzmann $S=k\beta\langle E\rangle+k\ln Z$) supply the broader thermodynamic vocabulary; this definition is the continuum radiation specialisation used in the $\eta_B$ chain.
Sibling kernels (boseLogKernel, Mellin transforms of the log series) support the integral evaluations that follow.
proof idea
Pure definition: the body substitutes $f=1/(e^t-1)$ into the classical Bose entropy density and multiplies by $t^2$. No lemmas, tactics, or algebraic reductions are involved. Downstream lemmas such as bose_entropy_pointwise rewrite this expression into the energy kernel plus a logarithmic kernel.
why it matters
This kernel is the microscopic starting point for the module’s main theorems. bose_entropy_pointwise splits it into $t^3/(e^t-1)+t^2(-\ln(1-e^{-t}))$; integrating that split yields bose_entropy_integral_value ($\int\sigma_B=4\pi^4/45$) and then bose_entropy_eq_four_thirds_energy ($\int\sigma_B=(4/3)\int t^3/(e^t-1)$), the dimensionless content of $s=(4/3)\rho/T$ for massless bosons.
From the same integral, entropy_coeff_from_functional recovers the photon prefactor $2\pi^2/45$ without assuming $4/3$, and fermi_div_bose_entropy places the $7/8$ fermionic weight at the entropy-functional layer. Downstream, NeutrinoDilution.radiationEntropy builds plasma entropy density as $(g/2\pi^2)T^3\int\sigma$ using this integrand for the bosonic sector. In the Recognition Science $\eta_B$ chain this closes a MODEL element previously taken as thermodynamic input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.