eulerDet2FactorComplex
plain-language theorem explainer
eulerDet2FactorComplex defines the regularized per-prime determinant factor as (1 - p^{-s}) exp(p^{-s}) for each prime p. Researchers bridging the Euler product of zeta(s) to the Recognition Science carrier framework cite it when assembling the holomorphic function C(s). The definition is a direct one-line substitution of the per-prime eigenvalue supplied by eulerPrimePowerComplex.
Claim. For a prime number $p$ and complex $s$, the regularized per-prime factor is $(1 - p^{-s}) e^{p^{-s}}$.
background
The EulerInstantiation module maps the classical Euler product for the Riemann zeta function onto the abstract RS carrier and sensor framework defined in AnnularCost and CostCoveringBridge. Primes is the set of natural numbers satisfying the usual primality predicate. The auxiliary definition eulerPrimePowerComplex supplies the complex value $p^{-s}$ uniformly as an exponential, allowing the factor to be written without case distinctions on the strip.
proof idea
One-line wrapper that substitutes the definition of eulerPrimePowerComplex into the product (1 - eulerPrimePowerComplex p s) * exp(eulerPrimePowerComplex p s).
why it matters
The factor is invoked by the downstream theorem eulerDet2FactorComplex_ne_zero to establish nonvanishing on Re(s) > 0, which supports the module-level carrier_nonvanishing and euler_instantiation results. These close the chain from prime sums and Hilbert-Schmidt norms to a holomorphic nonvanishing C(s) that satisfies the EulerCarrier interface, enabling the cost-covering axiom and conditional RH. The construction aligns with the Recognition Science emphasis on regularized determinants in the analytic continuation step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.