gamma_four
plain-language theorem explainer
The complex gamma value at 4 equals 6, i.e. Γ(4) = 3! = 6. Cosmology proofs that evaluate Bose and Fermi Mellin transforms at s = 4 cite this constant. The argument is a short reduction to Mathlib's factorial formula for Γ at positive integers, followed by numeric simplification of 3!.
Claim. The complex gamma function satisfies $\Gamma(4) = 6$, equivalently $\Gamma(4) = 3!$.
background
This module sits at the thermodynamic (integral) layer of the Recognition Science entropy-per-photon chain. The series identity $\eta(4) = (7/8)\zeta(4)$ is already available from Cosmology.FermionWeight. What remains is to identify the Fermi–Dirac and Bose–Einstein energy integrals
$$\int_0^\infty \frac{t^3}{e^t\pm 1},dt$$
with closed forms $\Gamma(4)\eta(4)$ and $\Gamma(4)\zeta(4)$.
Both integrals arise as Mellin transforms at $s = 4$ of geometric series in $e^{-t}$. Mathlib's Mellin–Dirichlet bridge produces a factor $\Gamma(s)$ in front of the shifted zeta or eta sum. At the integer point $s = 4$ one therefore needs the elementary evaluation $\Gamma(4) = 3! = 6$ before the known values $\zeta(4) = \pi^4/90$ and $\eta(4) = (7/8)\zeta(4)$ can be inserted.
proof idea
One-line style reduction to Mathlib. Apply Complex.Gamma_ofNat_eq_factorial at $n = 3$, which gives $\Gamma(3+1) = 3!$. Rewrite the factorial by norm_num to obtain the concrete integer 6, then convert the equality back to $\Gamma(4) = 6$ with a second numeric check on the index shift.
why it matters
Without $\Gamma(4) = 6$ the Mellin evaluations stay symbolic. Downstream lemmas mellin_bose_value and mellin_fermi_value multiply the shifted zeta/eta HasSum statements by 6 and conclude
$$\mathrm{mellin},\frac{1}{e^t-1},4 = \pi^4/15,\qquad \mathrm{mellin},\frac{1}{e^t+1},4 = 7\pi^4/120.$$
Those closed forms are exactly the Bose and Fermi energy integrals used in the entropy bookkeeping. With them, the entire mathematical content of the fermion weight $7/8$ becomes a theorem; only the $g_*$ species census remains model-level physics. The result is local arithmetic scaffolding inside the cosmology chain, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.