norm_eulerPrimePowerComplex_lt_one
plain-language theorem explainer
The theorem shows that for complex s with positive real part and any prime p the modulus of the per-prime Euler factor exp(-s log p) is strictly less than one. Analytic number theorists constructing Euler-product carriers or perturbation witnesses inside the critical strip cite it as the basic denominator-separation step. The argument rewrites the norm via the companion lemma, confirms the prime logarithm is positive, and applies the strict monotonicity of the real exponential.
Claim. Let $s$ be complex with real part strictly positive and let $p$ be prime. Then the modulus of the complex per-prime Euler factor $p^{-s}$ satisfies $e^{-s_1 log p} < 1$, where $s_1 = Re(s)$.
background
The result belongs to the EulerInstantiation module, which realizes the abstract RS carrier and sensor framework of AnnularCost and CostCoveringBridge by means of the classical Euler product for zeta. The central object is the per-prime factor eulerPrimePowerComplex p s, defined as Complex.exp(-(s * primeLog p)) and representing the regularized term p^{-s} uniformly on the complex plane. The module proceeds from prime sums and Hilbert-Schmidt norms through carrier-log convergence to the non-vanishing and bounded-derivative statements that license the cost-covering axiom and conditional RH.
proof idea
The tactic proof first rewrites the target norm by the lemma norm_eulerPrimePowerComplex. It then establishes positivity of primeLog p by casting the prime property p > 1 and invoking Real.log_pos. Nlinarith shows that the exponent -s.re * primeLog p is negative. Real.exp_lt_exp.mpr together with simpa yields the strict inequality.
why it matters
The inequality supplies the strict unit-disk containment used by the three immediate downstream results: the bound on the per-prime logarithmic derivative, the sensor-circle version, and the non-vanishing of 1 minus the factor. It therefore forms the first concrete strip estimate in the chain from Euler product to EulerCarrier satisfaction and the conditional Riemann hypothesis. The module doc-comment identifies this step as the basic denominator-separation fact required for all later prime-level perturbation estimates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.