eulerDet2FactorComplex_ne_zero
plain-language theorem explainer
Each regularized Euler factor attached to a prime remains nonzero for any complex s whose real part is positive. Analysts verifying the holomorphic nonvanishing of the regularized determinant in the right half-plane cite this step when building the concrete Euler product inside the abstract carrier framework. The proof is a one-line term wrapper that unfolds the factor and applies the product nonvanishing rule together with the known nonvanishing of the complex exponential.
Claim. For every complex number $s$ with positive real part and every prime $p$, the regularized complex Euler factor at $p$ and $s$ is nonzero.
background
The module instantiates the abstract RS carrier/sensor framework by replacing the abstract annular cost with the concrete Euler product of the zeta function. Core objects include the prime sum $P(σ) = ∑_p p^{-σ}$, the Hilbert–Schmidt norm squared $∑_p p^{-2σ}$, and the carrier log series that converges for Re(s) > 1/2. The architecture proceeds in three layers: AnnularCost supplies the abstract cost axioms, CostCoveringBridge converts those axioms into a conditional Riemann hypothesis, and the present file supplies the concrete Euler product that satisfies the carrier interface.
proof idea
The proof is a term-mode one-liner. It unfolds the definition of the Euler factor, then applies the lemma that a product of two complex numbers is nonzero when each factor is nonzero, invoking the universal nonvanishing of the complex exponential and the prior result that the subtracted prime-power term is nonzero on the open right half-plane.
why it matters
This nonvanishing statement is required for the carrier_nonvanishing theorem that closes the Euler instantiation chain. Once the regularized determinant C(s) is shown holomorphic and nonzero for Re(s) > 1/2, the logarithmic derivative remains bounded, the EulerCarrier and RegularCarrier interfaces are satisfied, and the cost-covering axiom becomes applicable, yielding the conditional Riemann hypothesis. The result therefore supplies the concrete analytic object that a future phase-lift witness can sample on circles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.