pow_eq_exp_log
plain-language theorem explainer
For natural numbers n and k, the real identity (n+1)^k = exp(k log(n+1)) holds. UV-summability arguments in the exact-shell path sum cite it to rewrite polynomial shell-cardinality bounds as exponential growth rates. The proof is a short positivity-plus-rewrite: log-of-power then exp-log cancellation on the positive base n+1.
Claim. For all natural numbers $n$ and $k$, $((n:\mathbb{R})+1)^k = \exp\bigl(k\cdot\log((n:\mathbb{R})+1)\bigr)$ as real numbers.
background
The module ExactShellGaugeUV organizes the quotient-class path-sum configuration space into exact complexity shells (no size caps) and proves that the shell-resummed path sum with an explicit Gaussian UV regulator exp(-ρ·n²) converges for every ρ > 0. Honesty tags in the module doc stress that the regulator is inserted by hand, the phase is a free parameter, and regulator removal (ρ → 0⁺) remains a named open.
Stage 1 supplies the shell entropy bound card(ExactPathClass n) ≤ (n+1)^(12·(n+1)). Regulated shell terms therefore carry polynomial factors (n+1)^k against the Gaussian decay. Converting those powers into exp(k log(n+1)) is the elementary bridge that lets comparison arguments treat the entropy exponent as growing like n log n, which is o(n²).
proof idea
Establish positivity: 0 < (n:ℝ)+1 by the positivity tactic. Rewrite the goal via the reverse of Real.log_pow, turning the left-hand side into exp(log((n+1)^k)). Cancel with Real.exp_log, using that the power is positive (pow_pos on the positivity hypothesis). Two rewrites, no case splits.
why it matters
Direct dependency of summable_zRSUVShell (THEOREM S2c, UV summability): for every ρ > 0 and every phase parameter, the regulated shell series is summable. That proof eventually compares exp(-ρ n²)·(n+1)^(12(n+1)) with the geometric series exp(-ρ/2)^n, using exists_gaussian_domination (entropy exponent grows like n·log n = o(n²)). The present identity is the conversion step that turns the polynomial shell bound into an exponential of a logarithm so the o(n²) comparison applies.
It sits inside Stage 2 of the seven-gaps exact-shell program. It does not touch continuum-limit flags, physical action derivation, or the open HasZRSRegulatorRemoval question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.