one_sub_eulerPrimePowerComplex_ne_zero
plain-language theorem explainer
The result shows that 1 minus p to the power minus s stays nonzero for every prime p when the real part of s is positive. Analysts building Euler products or regularized determinants for the zeta function would cite the fact to keep individual factors from vanishing. The proof assumes equality to one, derives that the norm must equal one, and reaches a contradiction with the strict norm bound less than one on the open right half-plane.
Claim. For any complex number $s$ with real part greater than zero and any prime $p$, $1 - p^{-s} = 0$ is false, where $p^{-s}$ is realized as the complex exponential of minus $s$ times the logarithm of $p$.
background
The EulerInstantiation module embeds the classical Euler product for the zeta function into the Recognition Science carrier framework. The per-prime term is realized as the complex exponential exp of minus s times the logarithm of p, which equals p to the power minus s and serves as the eigenvalue of the associated Hilbert-Schmidt operator. The upstream norm theorem establishes that the modulus of each such term is strictly less than one whenever the real part of s exceeds zero; this separation property is the direct input to the present non-vanishing argument.
proof idea
Assume for contradiction that the term equals one. Then its norm equals one. This contradicts the upstream norm theorem that the modulus is strictly less than one under the positive real-part hypothesis. The conclusion follows by applying the general fact that one minus z is nonzero whenever z differs from one.
why it matters
The lemma is invoked directly in the proof of the companion statement that the regularized Euler factor is nonzero on the right half-plane. That companion result supports the claim that the full determinant C(s) is nonvanishing for real part greater than one half, which allows the Euler product to satisfy the abstract EulerCarrier interface. The step therefore closes the prime-level non-vanishing requirement in the chain from primes through Hilbert-Schmidt convergence to the cost-covering axiom and conditional Riemann hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.