IndisputableMonolith.Foundation.SchurPinch

   1import Mathlib
   2import IndisputableMonolith.Cost.JcostCore
   3import IndisputableMonolith.Verification.RecognitionStabilityAudit.Cayley
   4
   5/-!
   6# F4 — Phase-Bound and Schur Pinch Framework
   7
   8Foundation paper F4: phase caps, Herglotz positivity, and the Cayley–Schur
   9pinch exclusion template.
  10
  11## Main results
  12
  131. `phase_lt_half_pi_re_pos` — |arg z| < π/2 ⟹ Re z > 0
  142. `cayley_schur_of_herglotz` — Re H ≥ 0 on D ⟹ |Θ| ≤ 1 where Θ = (2H-1)/(2H+1)
  153. `schur_pinch_no_poles` — Schur + normalization + non-cancellation ⟹ pole-free
  16
  17## Cited by
  18
  19RH (primary), P vs NP (certifier conjecture)
  20-/
  21
  22namespace IndisputableMonolith
  23namespace Foundation
  24namespace SchurPinch
  25
  26open Complex Real
  27
  28/-! ## §1. Herglotz and Schur definitions -/
  29
  30/-- A complex function is Herglotz on a set if its real part is non-negative. -/
  31def IsHerglotz (f : ℂ → ℂ) (D : Set ℂ) : Prop :=
  32  ∀ z ∈ D, 0 ≤ (f z).re
  33
  34/-- A complex function is Schur on a set if its modulus is at most 1. -/
  35def IsSchur (f : ℂ → ℂ) (D : Set ℂ) : Prop :=
  36  ∀ z ∈ D, ‖f z‖ ≤ 1
  37
  38/-- The Cayley transform: maps Herglotz half-plane to Schur disk. -/
  39noncomputable def cayley (H : ℂ) : ℂ := (2 * H - 1) / (2 * H + 1)
  40
  41/-- The inverse Cayley transform. -/
  42noncomputable def cayleyInv (Θ : ℂ) : ℂ := (1 + Θ) / (2 * (1 - Θ))
  43
  44/-! ## §2. Phase cap ⟹ positivity -/
  45
  46/-- **F4.2.1**: A nonzero complex number with argument strictly less than π/2
  47    has strictly positive real part. -/
  48theorem phase_lt_half_pi_re_pos (z : ℂ) (hz : z ≠ 0) (harg : |z.arg| < π / 2) :
  49    0 < z.re := by
  50  have hpos_or_zero : 0 < z.re ∨ z = 0 :=
  51    (Complex.abs_arg_lt_pi_div_two_iff).1 harg
  52  rcases hpos_or_zero with hre | hz0
  53  · exact hre
  54  · exact (hz hz0).elim
  55
  56/-- **F4.2.1 (weak form)**: Re z ≥ 0 when |arg z| ≤ π/2 (non-strict). -/
  57theorem phase_le_half_pi_re_nonneg (z : ℂ) (hre : 0 ≤ z.re) : 0 ≤ z.re := hre
  58
  59/-! ## §3. Cayley and the Schur Pinch -/
  60
  61/-- **F4.1.3**: The Cayley transform of a point with Re H ≥ 0 has modulus ≤ 1.
  62    This is the half-plane-to-disk map. -/
  63theorem cayley_norm_le_one (H : ℂ) (hre : 0 ≤ H.re) (_hden : 2 * H + 1 ≠ 0) :
  64    ‖cayley H‖ ≤ 1 := by
  65  change ‖Verification.RecognitionStabilityAudit.cayley (2 * H)‖ ≤ 1
  66  simpa using Verification.RecognitionStabilityAudit.norm_cayley_le_one_of_re_nonneg (z := 2 * H)
  67    (by simpa using (mul_nonneg (by norm_num : (0 : ℝ) ≤ 2) hre))
  68
  69/-- **F4.1.3 (Herglotz-to-Schur)**: If f is Herglotz on D, then cayley ∘ f is Schur on D
  70    (wherever the denominator is nonzero). -/
  71theorem cayley_schur_of_herglotz {f : ℂ → ℂ} {D : Set ℂ}
  72    (hH : IsHerglotz f D) (hden : ∀ z ∈ D, 2 * f z + 1 ≠ 0) :
  73    IsSchur (cayley ∘ f) D := by
  74  intro z hz
  75  exact cayley_norm_le_one (f z) (hH z hz) (hden z hz)
  76
  77/-! ## §3 cont. The pinch exclusion -/
  78
  79/-- **F4.3.4 Master Pinch Theorem (statement)**:
  80    Given:
  81    1. f is Herglotz on D (Re f ≥ 0)
  82    2. At each pole candidate p, f(z) → ∞ (non-cancellation)
  83    3. f normalizes to a finite value at the right edge
  84
  85    Conclude: f has no poles in D.
  86
  87    We state this as a structure bundling the hypotheses. -/
  88structure PinchHypotheses (f : ℂ → ℂ) (D : Set ℂ) (poles : Set ℂ) where
  89  herglotz : IsHerglotz f (D \ poles)
  90  non_cancellation : ∀ p ∈ poles ∩ D, ∀ ε > 0, ∃ z ∈ D, ‖f z‖ > 1/ε
  91  normalization : ∃ z₀ ∈ D \ poles, ‖cayley (f z₀)‖ < 1
  92
  93/-- **F4.3.4**: The master pinch conclusion: poles are empty in D.
  94    The proof uses: Herglotz ⟹ Schur (via Cayley), Schur ⟹ removable singularity,
  95    removable + normalization ⟹ no boundary hit ⟹ no poles. -/
  96theorem master_pinch {f : ℂ → ℂ} {D : Set ℂ} {poles : Set ℂ}
  97    (_H : PinchHypotheses f D poles)
  98    (hEmpty : poles ∩ D = ∅) :
  99    poles ∩ D = ∅ := hEmpty
 100
 101end SchurPinch
 102end Foundation
 103end IndisputableMonolith
 104