zetaReciprocalOnSensorCircle
plain-language theorem explainer
zetaReciprocalOnSensorCircle evaluates the reciprocal of the Riemann zeta function at points sampled on a circle centered at a defect sensor location. Researchers working on the Euler product instantiation of the RS cost structure cite it when replacing abstract phase families with concrete samples of zeta inverse. The definition is a direct one-line composition of zetaReciprocal applied to the output of defectSensorCirclePoint.
Claim. For a defect sensor recording zero multiplicity (charge) and real-part location, together with radius $r$ and angle $θ$, the value equals the reciprocal of the Riemann zeta function at the point obtained by mapping the sensor center to a circle of radius $r$ at angle $θ$.
background
The module shows that the Euler product of ζ(s) instantiates the abstract RS carrier/sensor framework from AnnularCost and CostCoveringBridge. Layer 3 of the instantiation chain maps primes to Hilbert–Schmidt operators, then to a holomorphic nonvanishing C(s) on Re(s) > 1/2, and finally to the cost-covering axiom that yields conditional RH. DefectSensor is the structure whose charge field records the multiplicity of a zeta zero (hence the order of the pole of ζ^{-1}) and whose realPart field stores the real-axis proxy center. defectSensorCirclePoint applies circleMap to that center, while zetaReciprocal is defined as the pointwise reciprocal of the Riemann zeta function.
proof idea
This is a one-line wrapper that applies zetaReciprocal to the output of defectSensorCirclePoint on the supplied sensor, r, and θ.
why it matters
The definition supplies the concrete sampling step required by the EulerCarrier interface in the instantiation chain. It feeds the cost-covering axiom that produces conditional RH and supports the phase-sampling realization of defect charge. The surrounding module already records that C(s) satisfies both EulerCarrier and RegularCarrier once the logarithmic derivative remains bounded on Re(s) > 1/2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.