xiMap

formal source

  46
  47/-- The defect-coordinate map: σ ↦ e^{2(σ − 1/2)}.
  48    Maps the critical strip to ℝ₊ with the critical line 1/2 ↦ 1. -/
  49def xiMap (σ : ℝ) : ℝ := Real.exp (2 * (σ - 1 / 2))
  50
  51@[simp] theorem xiMap_pos (σ : ℝ) : 0 < xiMap σ := Real.exp_pos _
  52
  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 -/