defectSensorCirclePoint
plain-language theorem explainer
This definition parameterizes points on a circle of given radius and angle centered at the real part of a defect sensor. Researchers constructing explicit samples of the reciprocal zeta function or Euler factors inside the critical strip cite it when building concrete witnesses for cost-covering arguments. It is realized as a direct one-line application of the circle mapping operation to the sensor center coordinate.
Claim. For a defect sensor $s$ with real part $σ_s$, radius $r≥0$ and angle $θ$, the sampled point on the circle is $σ_s + r( cos θ + i sin θ)$.
background
The EulerInstantiation module supplies the concrete layer that realizes the abstract carrier and sensor framework of AnnularCost and CostCoveringBridge via the Euler product for ζ(s). A DefectSensor records the multiplicity (charge) of a zero of ζ together with its real part, acting as a probe where ζ⁻¹ has a pole of that order. The upstream defectSensorCenter extracts this real part as a complex number lying on the real axis, providing the geometric center for subsequent circle sampling.
proof idea
This is a one-line wrapper that applies the circleMap function to the result of defectSensorCenter on the given sensor, together with the supplied radius and angle.
why it matters
The definition supplies the geometric sampling primitive required by defectSensorCirclePoint_mem_strip, defectSensorCirclePoint_re, norm_eulerPrimePowerComplex_lt_one_on_sensorCircle and zetaReciprocalOnSensorCircle. It completes the concrete instantiation step in the chain from prime sums through Hilbert–Schmidt norms to a carrier satisfying the cost-covering axiom, thereby supporting the conditional Riemann hypothesis. It touches the open question of explicit strip bounds on the logarithmic derivative of the Euler product.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.