xiMap_at_half

formal source

  53theorem xiMap_ne_zero (σ : ℝ) : xiMap σ ≠ 0 := (xiMap_pos σ).ne'
  54
  55/-- The critical line maps to x = 1, the unique minimum of J. -/
  56@[simp] theorem xiMap_at_half : xiMap (1 / 2) = 1 := by
  57  simp [xiMap]
  58
  59/-- **Functional reflection acts as reciprocal inversion.**
  60    This is the bridge equation: ξ(s) = ξ(1−s) becomes J(x) = J(1/x). -/
  61theorem xiMap_reflection (σ : ℝ) : xiMap (1 - σ) = (xiMap σ)⁻¹ := by
  62  simp only [xiMap]
  63  rw [show 2 * ((1 : ℝ) - σ - 1 / 2) = -(2 * (σ - 1 / 2)) from by ring]
  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