defectSensorCirclePoint_re
plain-language theorem explainer
Explicit real-part extraction for circle sampling around a defect sensor center yields the sensor real part plus r times cosine of theta. Researchers instantiating the Euler product into the RS carrier framework cite this when verifying sampled points remain inside the critical strip. The term proof unfolds the circle map definition and applies real-part simplification rules for complex exponentials.
Claim. Let $ρ$ be the real part of a defect sensor. The real part of the point obtained by sampling a circle of radius $r$ at angle $θ$ centered at $ρ$ equals $ρ + r cos θ$.
background
The DefectSensor structure from CostCoveringBridge consists of a charge (multiplicity of the zeta zero) and realPart (its location). defectSensorCenter maps this to a complex number on the real axis. defectSensorCirclePoint applies circleMap to that center, producing the sampled point whose real part is extracted here.
proof idea
The term proof rewrites using the definitions of defectSensorCirclePoint, defectSensorCenter, and circleMap. It then simplifies via Complex.mul_re and Complex.exp_ofReal_mul_I_re to isolate the real component of the resulting complex number.
why it matters
This result is used directly by defectSensorCirclePoint_mem_strip to show sampled circle points lie in Re(s) > 1/2 when the radius is sufficiently small. It supplies the geometric sampling step in the EulerInstantiation chain (primes to Hilbert-Schmidt norm to det2 to EulerCarrier), enabling the cost-covering axiom and conditional RH as described in the module architecture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.