cpow_shift3
plain-language theorem explainer
For each natural n, the complex power (n+1)^3 equals the ordinary real cube of (n+1), cast back to ℂ. Cosmology proofs that identify Mellin transforms of Bose/Fermi kernels with Dirichlet series at s=3 cite this cast bridge. The argument is a short rewrite through natural-number complex power and ring normalization.
Claim. For every natural number $n$, $((n+1):\mathbb{C})^{3}=\bigl((n+1)^{3}:\mathbb{C}\bigr)$, where the left-hand side is complex exponentiation of the positive real $n+1$ and the right-hand side is the real cube cast into $\mathbb{C}$.
background
The module closes the number-density layer of radiation thermodynamics: the Mellin transforms at $s=3$ of the Bose and Fermi kernels $1/(e^{t}-1)$ and $1/(e^{t}+1)$. Those integrals equal $\Gamma(3)\zeta(3)=2\zeta(3)$ and $\Gamma(3)\eta(3)=(3/2)\zeta(3)$, which feed the photon number density $n_{\gamma}=(2\zeta(3)/\pi^{2})T^{3}$ and the fermionic number-weight $3/4$.
Series expansions of the kernels produce terms of the form $1/(n+1)^{3}$ (or signed eta variants). Lean’s complex power cpow is the ambient operation on Mellin side, while the zeta/eta sums are real. This lemma equates the two presentations of the cubic power so that real HasSum statements can be transported into ℂ.
The same cast pattern appears for the logarithmic kernels used in radiation entropy relations (powers $4$ rather than $3$), so the lemma is the $s=3$ instance of a recurring coercion step.
proof idea
Rewrite the complex exponent $3:\mathbb{C}$ as the natural $3$ cast into ℂ (norm_num). Apply Complex.cpow_natCast, which reduces complex power with natural exponent to iterated multiplication. push_cast aligns the real/complex coercions on the base $n+1$, and ring finishes the equality of the two cubic expressions.
why it matters
Parent lemmas mellin_bose3_value and mellin_fermi3_value use the cast inside HasSum.congr_fun to match the complex Mellin series term-by-term with the real shifted zeta/eta sums, yielding $\mathrm{mellin}(1/(e^{t}-1),3)=2\zeta(3)$ and $\mathrm{mellin}(1/(e^{t}+1),3)=(3/2)\zeta(3)$. Those values are the last analytic inputs to entropyPerPhoton_from_integrals and the number-density fermion weight $\eta(3)/\zeta(3)=3/4$.
The same lemma is reused in RadiationEntropyRelation for the log-kernel Mellin values at exponent $3$ in the series indexing (paired with zeta/eta at $4$), so it sits on the shared coercion path between number-density and entropy-density integral layers. It does not itself touch RS forcing landmarks (T5–T8, RCL, phi); it is pure analytic plumbing for the cosmological integral layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.