defectSensorCenter
plain-language theorem explainer
defectSensorCenter extracts the real part stored in a DefectSensor and casts it to the complex plane, supplying the origin for circle sampling of Euler factors. Researchers instantiating the abstract carrier axioms with the zeta Euler product would cite this when parameterizing sensor positions in the cost-covering bridge. The definition is a direct one-line field projection with type coercion.
Claim. Let $s$ be a defect sensor storing only a real part. The geometric center is the complex number whose real part equals the value stored in $s$.
background
The module shows that the Euler product of zeta instantiates the abstract RS carrier/sensor framework from AnnularCost and CostCoveringBridge. Layer 1 supplies the abstract cost structure, Layer 2 the carrier axioms yielding conditional RH, and Layer 3 the concrete Euler product that satisfies those axioms via Hilbert-Schmidt norms, det2 convergence, and bounded logarithmic derivatives. DefectSensor belongs to this sensor layer and stores only its real part as a proxy center on the real axis.
proof idea
one-line wrapper that projects the realPart field of the input DefectSensor and coerces the result to ℂ.
why it matters
This supplies the center argument to defectSensorCirclePoint, the geometric entry point for replacing abstract phase families by samples of zeta inverse or Euler factors on circles. It supports the euler_instantiation result that the concrete C(s) satisfies the EulerCarrier interface, advancing the module's Layer 3 instantiation chain. The construction connects to the eight-tick phases used for complex sampling in the RS framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.