xiMap_eq_exp_zeroDeviation

formal source

  72/-! ## §2. Connection to ZeroLocationCost -/
  73
  74/-- xiMap agrees with exp(zeroDeviation) from ZeroLocationCost. -/
  75theorem xiMap_eq_exp_zeroDeviation (ρ : ℂ) :
  76    xiMap ρ.re = Real.exp (zeroDeviation ρ) := by
  77  simp [xiMap, zeroDeviation]
  78
  79/-! ## §3. J-cost in strip coordinates -/
  80
  81/-- J-cost on defect coordinates gives the cosh form of the zero defect:
  82    J(e^{2η}) = cosh(2η) − 1  where η = σ − 1/2. -/
  83theorem jcost_xiMap_eq_cosh (σ : ℝ) :
  84    Jcost (xiMap σ) = Real.cosh (2 * (σ - 1 / 2)) - 1 :=
  85  jcost_exp_eq_cosh (2 * (σ - 1 / 2))
  86
  87/-- J-cost vanishes on the critical line. -/
  88@[simp] theorem jcost_xiMap_at_half : Jcost (xiMap (1 / 2)) = 0 := by
  89  rw [xiMap_at_half, Jcost_unit0]
  90
  91/-- J-cost is nonneg on the strip. -/
  92theorem jcost_xiMap_nonneg (σ : ℝ) : 0 ≤ Jcost (xiMap σ) :=
  93  Jcost_nonneg (xiMap_pos σ)
  94
  95/-- J-cost on defect coordinates is symmetric under functional reflection.
  96    This IS the bridge:  ξ(s)=ξ(1−s)  ↔  J(x)=J(1/x). -/
  97theorem jcost_xiMap_functional_symmetry (σ : ℝ) :
  98    Jcost (xiMap (1 - σ)) = Jcost (xiMap σ) := by
  99  rw [xiMap_reflection, Jcost_symm (xiMap_pos σ)]
 100
 101/-- RH is equivalent to all zeros having zero J-cost. -/
 102theorem rh_equivalent_to_zero_cost (ρ : ℂ) :
 103    OnCriticalLine ρ ↔ Jcost (xiMap ρ.re) = 0 := by
 104  constructor
 105  · intro h