eulerPrimePowerComplex

formal source

 344
 345/-- The actual complex per-prime Euler eigenvalue `p^{-s}` on the strip, written
 346as an exponential so it is available uniformly on `ℂ`. -/
 347noncomputable def eulerPrimePowerComplex (p : Nat.Primes) (s : ℂ) : ℂ :=
 348  Complex.exp (-(s * (primeLog p : ℂ)))
 349
 350/-- The complex per-prime regularized determinant factor
 351`(1 - p^{-s}) exp(p^{-s})`. -/
 352noncomputable def eulerDet2FactorComplex (p : Nat.Primes) (s : ℂ) : ℂ :=
 353  (1 - eulerPrimePowerComplex p s) * Complex.exp (eulerPrimePowerComplex p s)
 354
 355/-- The complex per-prime logarithmic derivative contribution
 356`(log p) p^{-2s} / (1 - p^{-s})`. This is the natural prime-level quantity whose
 357norm should feed the perturbation budget on sampled circles. -/
 358noncomputable def eulerPrimeLogDerivTermComplex (p : Nat.Primes) (s : ℂ) : ℂ :=
 359  ((primeLog p : ℂ) * (eulerPrimePowerComplex p s) ^ 2) /
 360    (1 - eulerPrimePowerComplex p s)
 361
 362/-- The actual reciprocal zeta function. Around a hypothetical zero, this is the
 363meromorphic object whose sampled phase should realize the defect charge. -/
 364noncomputable def zetaReciprocal (s : ℂ) : ℂ :=
 365  (riemannZeta s)⁻¹
 366
 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 θ