norm_eulerPrimePowerComplex_lt_one_on_sensorCircle
plain-language theorem explainer
The theorem shows that each prime Euler factor p^{-s} has modulus strictly less than one at points sampled on a circle around a defect sensor when the radius keeps the circle inside the open right half-plane. Researchers building sampled perturbation witnesses for the cost-covering argument toward conditional RH would cite this bound. The short tactic proof first confirms positive real part of the sampled point via the strip membership lemma and then applies the open half-plane norm bound for the Euler factor.
Claim. Let $s$ be a point on the circle of radius $r$ centered at a defect sensor location with real part $σ > 1/2$. For $0 ≤ r < σ - 1/2$, any real $θ$, and any prime $p$, $|p^{-s}| < 1$.
background
In the Euler product instantiation module the abstract DefectSensor structure from CostCoveringBridge represents a potential zero of ζ(s), specified by its multiplicity (charge) and real part. The auxiliary definition defectSensorCirclePoint samples points on a circle around this sensor center. The upstream theorem defectSensorCirclePoint_mem_strip guarantees that any such circle whose radius satisfies the given bound remains inside the open half-plane Re(s) > 1/2.
proof idea
The proof first applies defectSensorCirclePoint_mem_strip to the radius constraints to obtain that the real part of the sampled point is positive. It then invokes the theorem norm_eulerPrimePowerComplex_lt_one, which asserts that the Euler factor has norm less than one on the open right half-plane.
why it matters
This supplies the first directly usable strip estimate for sampled perturbation witnesses in the Euler instantiation chain. It supports the passage from abstract carrier axioms to concrete Euler factors, feeding into Hilbert-Schmidt convergence and nonvanishing of the regularized determinant on Re(s) > 1/2. In the Recognition Science framework it advances the concrete realization of the cost structure via the Euler product, a prerequisite for applying the cost-covering axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.