gamma_three
plain-language theorem explainer
The complex gamma function satisfies Γ(3) = 2. Cosmology proofs of Bose and Fermi number-density Mellin integrals at s = 3 cite this to replace Γ(3)ζ(3) and Γ(3)η(3) by explicit multiples of ζ(3). The argument is a short reduction through Mathlib's natural-argument factorial identity for Gamma, followed by numerical simplification of 2!.
Claim. The complex gamma function evaluates to $\Gamma(3) = 2$ (equivalently $\Gamma(3) = 2!$).
background
In the number-density layer of RS cosmology, photon and fermion number densities are Mellin transforms of the Bose and Fermi kernels at $s = 3$:
$$\int_0^\infty \frac{t^{2}}{e^{t}\mp 1},dt = \Gamma(3),{\zeta(3),\eta(3)}.$$
The module already treats $\zeta(3)$ (Apéry's constant) and the Dirichlet eta value $\eta(3) = (3/4)\zeta(3)$ as unconditional sums; the remaining scalar is $\Gamma(3)$. The companion energy-density module closed the same story at $s = 4$; here $s = 3$ is the last analytic input to the entropy-per-photon ratio.
Mathlib supplies $\Gamma(n+1) = n!$ on natural arguments. Instantiating at $n = 2$ yields exactly $\Gamma(3) = 2!$.
proof idea
One short tactic proof. Invoke Mathlib's Complex.Gamma_ofNat_eq_factorial at $2$, obtaining $\Gamma(3) = 2!$. Reduce the factorial by norm_num, then convert the resulting equality (with a final norm_num to align the numeric literals). No series or integral reasoning appears here; the lemma is pure special-function arithmetic.
why it matters
Parent lemmas mellin_bose3_value and mellin_fermi3_value quote this identity to conclude
$$\mathrm{mellin}(1/(e^{t}-1),3) = 2\zeta(3),\qquad \mathrm{mellin}(1/(e^{t}+1),3) = (3/2)\zeta(3).$$
Those evaluations give the number-density fermion weight $\eta(3)/\zeta(3) = 3/4$, the companion of the $7/8$ entropy weight, and feed the capstone rewrite of entropy-per-photon as a pure ratio of thermodynamic integrals. Related log-kernel Mellin values in RadiationEntropyRelation reuse the same $\Gamma(3) = 2$ factor when converting Dirichlet series at shift $4$ into $\pi^{4}$ multiples. Within the RS forcing picture this is bookkeeping, not a new physical axiom: it closes the $s = 3$ integral layer so the entropy formula is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.