cpow_shift
plain-language theorem explainer
For every natural number n, the complex power (n+1)^(4:ℂ) of the positive real n+1 equals the ordinary real fourth power cast into ℂ. Downstream Mellin evaluations of the Bose and Fermi kernels at s=4 need this cast identity to match Dirichlet series written with real rpow against Mathlib's complex cpow. The proof rewrites the exponent as a natural cast and applies Complex.cpow_natCast, then finishes by push_cast and ring.
Claim. For every $n \in \mathbb{N}$, writing $x = n+1 > 0$ as a real, one has $x^{4} = x^{4}$ after viewing the left side as a complex power with exponent $4 \in \mathbb{C}$ and the right side as the real fourth power cast into $\mathbb{C}$.
background
The module closes the integral-layer gap between the series identity $\eta(4)=(7/8)\zeta(4)$ and the thermodynamic Fermi–Dirac versus Bose–Einstein energy integrals
$$\int_0^\infty t^3/(e^t+1),dt = (7/8)\int_0^\infty t^3/(e^t-1),dt.$$
Both sides are Mellin transforms at $s=4$ of geometric series in $e^{-t}$. Mathlib's hasSum_mellin turns those into Dirichlet series $\sum \Gamma(s),a_n/(n+1)^s$. At $s=4$ one has $\Gamma(4)=6$, so the sums are shifted $\zeta(4)$ and $\eta(4)$.
The Dirichlet terms are written with real powers $(n+1)^4$, while the Mellin interface works in $\mathbb{C}$ with complex powers. This lemma equates the two presentations of the fourth power for every positive integer base $n+1$.
proof idea
Short tactic proof. First rewrite the complex exponent $4:\mathbb{C}$ as the natural number $4$ cast into $\mathbb{C}$ (via norm_num). Apply Complex.cpow_natCast, which reduces $z^{\uparrow n}$ for $n:\mathbb{N}$ to ordinary iterated multiplication. Then push_cast aligns the real/complex coercions of the base $n+1$, and ring finishes the equality of the two fourth powers.
why it matters
Parent lemmas mellin_bose_value and mellin_fermi_value evaluate
$$\mathrm{mellin}\bigl(1/(e^t-1)\bigr)(4)=\pi^4/15,\qquad \mathrm{mellin}\bigl(1/(e^t+1)\bigr)(4)=7\pi^4/120$$
by uniqueness of unconditional sums against the shifted zeta/eta series. Those uniqueness arguments convert real rpow denominators into the complex cpow form expected by the Mellin interface; cpow_shift is the cast bridge they invoke.
With both Mellin values in hand, the module obtains the thermodynamic 7/8 ratio as a pure theorem (axiom-clean). That ratio is the entire mathematical content of EntropyPerPhoton.fermionWeight = 7/8; only the $g^*$ species census remains model-level physics bookkeeping. No Recognition forcing-chain landmark (T5–T8, RCL, phi) is touched here: the lemma is pure complex-analysis plumbing inside the cosmology entropy stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.