defectSensorCenter

formal source

 367/-- The current geometric center attached to a defect sensor. The present sensor
 368stores only the real part, so this uses the real-axis proxy center already used
 369elsewhere in the stack. -/
 370noncomputable def defectSensorCenter (sensor : DefectSensor) : ℂ :=
 371  (sensor.realPart : ℂ)
 372
 373/-- Sample a point on a circle around the current sensor center. This is the
 374geometric entry point for replacing abstract phase families by actual samples of
 375`ζ⁻¹` or Euler factors on circles. -/
 376noncomputable def defectSensorCirclePoint (sensor : DefectSensor) (r θ : ℝ) : ℂ :=
 377  circleMap (defectSensorCenter sensor) r θ
 378
 379/-- The reciprocal zeta function sampled on a sensor circle. -/
 380noncomputable def zetaReciprocalOnSensorCircle
 381    (sensor : DefectSensor) (r θ : ℝ) : ℂ :=
 382  zetaReciprocal (defectSensorCirclePoint sensor r θ)
 383
 384/-- Explicit real-part formula for the current sensor-circle parameterization. -/
 385theorem defectSensorCirclePoint_re (sensor : DefectSensor) (r θ : ℝ) :
 386    (defectSensorCirclePoint sensor r θ).re = sensor.realPart + r * Real.cos θ := by
 387  rw [defectSensorCirclePoint, defectSensorCenter, circleMap]
 388  simp [Complex.mul_re, Complex.exp_ofReal_mul_I_re]
 389
 390/-- Any circle around the sensor center whose radius stays inside the strip still
 391lies in the open half-plane `Re(s) > 1/2`. -/
 392theorem defectSensorCirclePoint_mem_strip
 393    (sensor : DefectSensor) {r θ : ℝ}
 394    (hr_nonneg : 0 ≤ r) (hr : r < sensor.realPart - 1 / 2) :
 395    1 / 2 < (defectSensorCirclePoint sensor r θ).re := by
 396  rw [defectSensorCirclePoint_re]
 397  have hcos : -1 ≤ Real.cos θ := Real.neg_one_le_cos θ
 398  nlinarith
 399
 400/-- Norm of the complex Euler eigenvalue is controlled exactly by the real part