primeLog

formal source

 339
 340/-- The real logarithm of a prime, recorded once to keep the complex Euler
 341factor formulas unambiguous. -/
 342noncomputable def primeLog (p : Nat.Primes) : ℝ :=
 343  Real.log (p : ℝ)
 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