norm_eulerPrimePowerComplex
plain-language theorem explainer
The theorem states that the modulus of the complex Euler prime-power term at prime p and complex s equals exp(-Re(s) times log p). Analysts building the Euler product instantiation of the RS carrier framework cite it to control eigenvalue norms on the right half-plane. The proof is a direct calc that substitutes the definition, invokes the modulus of the exponential, and reduces the real part via the logarithm identity.
Claim. For each prime $p$ and complex number $s$, the modulus satisfies $||eulerPrimePowerComplex(p,s)|| = exp(-Re(s) · log p)$.
background
The module instantiates the abstract RS carrier/sensor framework by realizing the Euler product of zeta(s) as a concrete carrier. Primes denotes the set of prime numbers. The function eulerPrimePowerComplex supplies the complex exponential form of each prime-power factor in the product, with primeLog supplying the natural logarithm of p. This identity supplies the exact norm control needed for the Hilbert-Schmidt norm and carrier-log series on Re(s) > 1/2.
proof idea
The proof is a calc block. It first rewrites the norm via the definition of eulerPrimePowerComplex and the supplied log equality, then applies Complex.norm_exp to the exponential, and finally reduces the real part using Complex.mul_re together with the log identification.
why it matters
The result is invoked directly by norm_eulerPrimePowerComplex_eq_rpow to equate the complex norm with the real rpow form and by norm_eulerPrimePowerComplex_lt_one to obtain the strict inequality less than 1 on the open right half-plane. It fills the prime-level norm step in the EulerInstantiation chain that produces the EulerCarrier interface and thereby the conditional RH via the cost-covering axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.