eulerPrimePowerComplex
plain-language theorem explainer
eulerPrimePowerComplex supplies the complex exponential form of the per-prime factor p^{-s} for the Euler product in the Recognition Science carrier framework. Number theorists working on zeta-function regularizations cite it when instantiating abstract cost structures with concrete primes. It is a direct one-line definition that rewrites the power as an exponential using the precomputed prime logarithm.
Claim. For a prime number $p$ and complex $s$, define the per-prime Euler factor by $e(p,s) = e^{-s log p}$, where $log p$ is the real logarithm of $p$. This supplies the complex eigenvalue $p^{-s}$ uniformly on the complex plane.
background
The EulerInstantiation module shows that the Euler product of zeta(s) instantiates the abstract RS carrier/sensor framework from AnnularCost and CostCoveringBridge. Core objects include PrimeSum sigma = sum_p p^{-sigma}, HilbertSchmidtNorm sigma = sum_p p^{-2sigma}, carrierLogSeries, and carrierDerivBound. The module establishes that the product yields holomorphic nonvanishing C(s) on Re(s) > 1/2 satisfying the EulerCarrier interface, leading to the cost-covering axiom and conditional RH.
proof idea
It is a one-line definition that applies Complex.exp to the negation of s multiplied by the complex cast of primeLog p.
why it matters
This definition supplies the per-prime building block for complex Euler factors, feeding eulerDet2FactorComplex, eulerPrimeLogDerivTermComplex, and the norm bounds norm_eulerPrimePowerComplex and norm_eulerPrimeLogDerivTermComplex_le_carrierDerivTerm. It supports the module's chain from primes to Hilbert-Schmidt convergence to carrier nonvanishing, instantiating the RS cost structure on the strip and bridging real and complex carrier theories.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.