norm_eulerPrimePowerComplex_eq_rpow
plain-language theorem explainer
The equality states that the modulus of the complex per-prime Euler factor for a prime p at complex s equals p raised to the power of minus the real part of s. Researchers instantiating the RS carrier framework via the Euler product cite this to equate complex norms with real rpow expressions. The proof is a short rewriting sequence that applies the prior norm theorem, invokes the positive rpow definition, and simplifies the prime logarithm with ring arithmetic.
Claim. For a prime number $p$ and complex $s$, the modulus of the complex per-prime Euler factor equals $p$ raised to the power of minus the real part of $s$.
background
The module shows that the Euler product of zeta(s) instantiates the abstract RS carrier/sensor framework from AnnularCost and CostCoveringBridge. Core objects include the prime sum P(sigma) = sum_p p^{-sigma}, the Hilbert-Schmidt norm squared of A(s), and the carrier log series. The complex per-prime Euler factor is defined as exp(-s * primeLog p) where primeLog p is the real logarithm of p. The upstream norm theorem already gives this factor's modulus as exp(-s.re * primeLog p).
proof idea
The proof rewrites the left-hand side via the upstream norm theorem for the complex Euler factor. It then applies the real rpow definition for positive base, reduces by congruence, simplifies the prime logarithm, and normalizes with ring.
why it matters
This bridges complex and real carrier theories in the Euler instantiation chain, feeding directly into the norm-form equality for the carrier derivative term. That term supports the logarithmic derivative bound required for the cost-covering axiom and conditional Riemann hypothesis. It closes the gap between the complex Euler eigenvalue and the real rpow expression used in the prime zeta and Hilbert-Schmidt convergence results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.