IndisputableMonolith.Verification.RecognitionStabilityAudit.Cayley

   1import Mathlib
   2
   3/-!
   4# Recognition Stability Audit (RSA): Cayley plumbing (algebraic core)
   5
   6This file is the **purely algebraic** part of the Recognition Stability Audit described in
   7`papers/tex/Recognition_Stability_Audit.tex`.
   8
   9RSA repeatedly uses the Cayley transform that maps:
  10
  11- the (closed) right half-plane `Re(z) ≥ 0`
  12- into the (closed) unit disk `‖·‖ ≤ 1`.
  13
  14We provide:
  15
  16- `cayley z = (z - 1)/(z + 1)`
  17- the paper-facing variant `theta J = (2J - 1)/(2J + 1)`
  18- the explicit inverse `invTheta ξ = ((1+ξ)/(1-ξ))/2`
  19
  20These are small, local lemmas that are ideal “RL training targets”: they are self-contained
  21and give immediate, checkable progress in the RSA pipeline.
  22-/
  23
  24namespace IndisputableMonolith
  25namespace Verification
  26namespace RecognitionStabilityAudit
  27
  28open scoped Real
  29
  30/-! ## Cayley: right half-plane → unit disk -/
  31
  32/-- Cayley transform sending the right half-plane to the unit disk. -/
  33noncomputable def cayley (z : ℂ) : ℂ :=
  34  (z - 1) / (z + 1)
  35
  36theorem normSq_add_one_sub_normSq_sub_one (z : ℂ) :
  37    Complex.normSq (z + 1) - Complex.normSq (z - 1) = 4 * z.re := by
  38  simp [Complex.normSq_apply]
  39  ring
  40
  41/-- If `Re z ≥ 0`, then `‖cayley z‖ ≤ 1`. -/
  42theorem norm_cayley_le_one_of_re_nonneg {z : ℂ} (hz : 0 ≤ z.re) :
  43    ‖cayley z‖ ≤ 1 := by
  44  have hz1 : z + 1 ≠ 0 := by
  45    intro h
  46    have hzneg : z = (-1 : ℂ) := by
  47      have : z = -(1 : ℂ) := eq_neg_of_add_eq_zero_left h
  48      simpa using this
  49    have : (0 : ℝ) ≤ (-1 : ℂ).re := by simpa [hzneg] using hz
  50    have : (0 : ℝ) ≤ (-1 : ℝ) := by simpa using this
  51    nlinarith
  52  have hpos : 0 < Complex.normSq (z + 1) :=
  53    (Complex.normSq_pos).2 hz1
  54
  55  have hle : Complex.normSq (z - 1) ≤ Complex.normSq (z + 1) := by
  56    have : 0 ≤ Complex.normSq (z + 1) - Complex.normSq (z - 1) := by
  57      have : 0 ≤ 4 * z.re := by nlinarith [hz]
  58      simpa [normSq_add_one_sub_normSq_sub_one z] using this
  59    exact (sub_nonneg).1 this
  60
  61  have hnSq : Complex.normSq ((z - 1) / (z + 1)) ≤ 1 := by
  62    have : Complex.normSq (z - 1) / Complex.normSq (z + 1) ≤ 1 :=
  63      (div_le_one hpos).2 hle
  64    simpa [Complex.normSq_div] using this
  65  have hsq : ‖(z - 1) / (z + 1)‖ ^ 2 ≤ 1 := by
  66    calc
  67      ‖(z - 1) / (z + 1)‖ ^ 2 = Complex.normSq ((z - 1) / (z + 1)) := by
  68        simpa using (Complex.sq_norm ((z - 1) / (z + 1)))
  69      _ ≤ 1 := hnSq
  70  have hw : 0 ≤ ‖(z - 1) / (z + 1)‖ := norm_nonneg _
  71  have : ‖(z - 1) / (z + 1)‖ ≤ 1 := by
  72    nlinarith [hsq, hw]
  73  simpa [cayley] using this
  74
  75/-! ## Paper-facing `Θ(J) = (2J - 1)/(2J + 1)` -/
  76
  77/-- RSA’s paper-facing Cayley transform. -/
  78noncomputable def theta (J : ℂ) : ℂ :=
  79  cayley (2 * J)
  80
  81@[simp] lemma theta_eq_div (J : ℂ) :
  82    theta J = (2 * J - 1) / (2 * J + 1) := by
  83  simp [theta, cayley]
  84
  85theorem norm_theta_le_one_of_re_nonneg {J : ℂ} (hJ : 0 ≤ J.re) :
  86    ‖theta J‖ ≤ 1 := by
  87  have : 0 ≤ (2 * J).re := by
  88    simpa using (mul_nonneg (by norm_num : (0 : ℝ) ≤ 2) hJ)
  89  simpa [theta] using (norm_cayley_le_one_of_re_nonneg (z := 2 * J) this)
  90
  91/-! ## Explicit inverse (for the “Cayley inverse” step) -/
  92
  93/-- Inverse of the paper-facing Cayley transform:
  94`2J = (1+Ξ)/(1-Ξ)` so `J = ((1+Ξ)/(1-Ξ))/2`. -/
  95noncomputable def invTheta (Ξ : ℂ) : ℂ :=
  96  ((1 + Ξ) / (1 - Ξ)) / 2
  97
  98theorem invTheta_theta {J : ℂ} (h : (2 * J + 1) ≠ 0) :
  99    invTheta (theta J) = J := by
 100  -- A direct field computation; `field_simp` uses `h` to clear the only real denominator.
 101  have h' : (1 - (2 * J - 1) / (2 * J + 1)) ≠ 0 := by
 102    -- `1 - (2J-1)/(2J+1) = 2/(2J+1)` and `2/(2J+1) ≠ 0` since `2 ≠ 0` and `2J+1 ≠ 0`.
 103    have : (1 - (2 * J - 1) / (2 * J + 1)) = (2 : ℂ) / (2 * J + 1) := by
 104      field_simp [h]
 105      ring
 106    -- Rewrite by this identity and reduce to `2/(2J+1) ≠ 0`.
 107    intro h0
 108    have : (2 : ℂ) / (2 * J + 1) = 0 := by simpa [this] using h0
 109    -- `a / b = 0` forces `a = 0` or `b = 0`.
 110    have h2 : (2 : ℂ) ≠ 0 := by
 111      norm_num
 112    have : (2 : ℂ) = 0 ∨ (2 * J + 1) = 0 := (div_eq_zero_iff).1 this
 113    cases this with
 114    | inl h20 => exact h2 h20
 115    | inr hb  => exact h hb
 116
 117  -- Main identity.
 118  -- Note: we explicitly expand `theta` to avoid any `simp` unfolding surprises.
 119  -- `field_simp` generates a ring goal.
 120  simp [invTheta, theta_eq_div]
 121  field_simp [h, h']
 122  ring
 123
 124theorem theta_invTheta {Ξ : ℂ} (h : Ξ ≠ 1) :
 125    theta (invTheta Ξ) = Ξ := by
 126  have h' : (1 - Ξ) ≠ 0 := sub_ne_zero.mpr (Ne.symm h)
 127  -- Direct algebra.
 128  simp [theta_eq_div, invTheta]
 129  field_simp [h']
 130  ring
 131
 132end RecognitionStabilityAudit
 133end Verification
 134end IndisputableMonolith
 135