xiMap_strictMono

formal source

  64  simp [Real.exp_neg]
  65
  66/-- The defect-coordinate map is strictly monotone on the strip. -/
  67theorem xiMap_strictMono : StrictMono xiMap := by
  68  intro a b hab
  69  simp only [xiMap]
  70  exact Real.exp_strictMono (by linarith)
  71
  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 (σ : ℝ) :