defectSensorCirclePoint_mem_strip
plain-language theorem explainer
The theorem shows that any circle of radius r centered at a defect sensor remains inside the open half-plane Re(s) > 1/2 whenever r is nonnegative and strictly less than the sensor real part minus 1/2. Researchers instantiating the Euler product as an RS carrier would cite it to justify domain restrictions for subsequent norm estimates on prime-power factors. The proof rewrites the real-part expression and finishes with a linear-arithmetic solver after inserting the bound -1 ≤ cos θ.
Claim. Let σ₀ be the real part of a defect sensor. For all real r, θ with 0 ≤ r < σ₀ - 1/2, the point s constructed as the circle of radius r about the sensor satisfies Re(s) > 1/2.
background
The EulerInstantiation module realizes the abstract carrier/sensor framework of AnnularCost and CostCoveringBridge by means of the Euler product for ζ(s). A DefectSensor is a point whose real part lies to the right of the critical line; the circle-point construction places points at Euclidean distance r from this center while preserving the angular coordinate θ. The module shows that the associated Hilbert–Schmidt operator A(s), its determinant C(s) = det₂²(I - A(s)), and the logarithmic derivative remain controlled precisely when Re(s) > 1/2, which is the content of the carrier nonvanishing and log-convergence statements quoted in the module documentation.
proof idea
The proof rewrites the real part of the circle point via the lemma defectSensorCirclePoint_re, records the elementary inequality -1 ≤ Real.cos θ, and concludes the desired strict lower bound by the nlinarith tactic.
why it matters
The result is used directly by the downstream theorem norm_eulerPrimePowerComplex_lt_one_on_sensorCircle, which establishes that each prime-power Euler factor lies strictly inside the unit disk on any such circle. Together these lemmas verify that the concrete Euler carrier satisfies the RegularCarrier interface on Re(s) > 1/2, thereby discharging the cost-covering axiom and yielding the conditional Riemann hypothesis for the zeta function realized as the RS carrier. It closes the third layer of the instantiation chain described in the module documentation and touches the open question of extending the same strip control to the critical line itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.