OnCriticalLine

formal source

  22noncomputable section
  23
  24/-- The critical-line predicate for a complex point. -/
  25def OnCriticalLine (ρ : ℂ) : Prop :=
  26  ρ.re = 1 / 2
  27
  28/-- Reflection across the line `Re(s) = 1/2`. -/
  29def functionalReflection (ρ : ℂ) : ℂ :=
  30  1 - ρ
  31
  32/-- Reflection across the line `Re(s) = 1/2`, composed with conjugation. -/
  33def criticalReflection (ρ : ℂ) : ℂ :=
  34  1 - conj ρ
  35
  36/-- The real deviation of `ρ` from the critical line, expressed in the
  37log-coordinate scale compatible with the RS defect functional. -/
  38def zeroDeviation (ρ : ℂ) : ℝ :=
  39  2 * (ρ.re - 1 / 2)
  40
  41/-- The RS defect attached to the zero-location deviation of `ρ`. -/
  42def zeroDefect (ρ : ℂ) : ℝ :=
  43  Foundation.LawOfExistence.defect (Real.exp (zeroDeviation ρ))
  44
  45/-- The zero-location defect is exactly `J_log` evaluated on the deviation. -/
  46theorem zeroDefect_eq_J_log (ρ : ℂ) :
  47    zeroDefect ρ =
  48      Foundation.DiscretenessForcing.J_log (zeroDeviation ρ) := by
  49  simpa [zeroDefect] using
  50    (Foundation.DiscretenessForcing.J_log_eq_J_exp (zeroDeviation ρ)).symm
  51
  52/-- Expanded closed form for the zero-location defect. -/
  53theorem zeroDefect_eq_cosh_sub_one (ρ : ℂ) :
  54    zeroDefect ρ = Real.cosh (zeroDeviation ρ) - 1 := by
  55  simpa [Foundation.DiscretenessForcing.J_log] using zeroDefect_eq_J_log ρ