IndisputableMonolith.Verification.RecognitionStabilityAudit.BackEnd

   1import Mathlib
   2
   3import IndisputableMonolith.Verification.RecognitionStabilityAudit.Core
   4
   5/-!
   6# Recognition Stability Audit (RSA): back-end (Schur/Herglotz “pinch” ⇒ no boundary hits)
   7
   8This file is the RSA “back-end” abstraction from the manuscript:
   9
  10- we assume a **Schur bound** `‖Ξ z‖ ≤ 1` on an audited region `Ω`,
  11- plus **analyticity** (holomorphic / complex differentiable on `Ω`),
  12- plus **nontriviality** (Ξ is not identically constant),
  13
  14and derive the “pinch” conclusion:
  15
  16> `¬ BoundaryHitAt Ξ z0` for any `z0 ∈ Ω`.
  17
  18Implementation note (RL-friendly): we build the proof from small, reusable lemmas:
  19
  201. `BoundaryHitAt Ξ z0` plus continuity at `z0` implies `Ξ z0 = 1`;
  212. Schur bound + `Ξ z0 = 1` makes `‖Ξ‖` attain a maximum at `z0`;
  223. Maximum modulus principle (strictly convex codomain) forces `Ξ` to be constant;
  234. Nontriviality contradicts constancy.
  24-/
  25
  26namespace IndisputableMonolith
  27namespace Verification
  28namespace RecognitionStabilityAudit
  29
  30open scoped Real Topology
  31open Filter Set
  32
  33/-! ## Helper: boundary-hit forces the value at the point -/
  34
  35theorem boundaryHit_implies_value_eq_one
  36    {Ξ : ℂ → ℂ} {z0 : ℂ}
  37    (hCont : ContinuousAt Ξ z0)
  38    (hHit : BoundaryHitAt Ξ z0) :
  39    Ξ z0 = (1 : ℂ) := by
  40  -- Compare two limits along the same (punctured) filter:
  41  --   (i) continuity gives `Ξ → Ξ z0`,
  42  --  (ii) boundary hit gives `Ξ → 1`.
  43  let l : Filter ℂ := (𝓝[({z0} : Set ℂ)ᶜ] z0)
  44  have hCont' : Tendsto Ξ l (𝓝 (Ξ z0)) :=
  45    tendsto_nhdsWithin_of_tendsto_nhds (s := ({z0} : Set ℂ)ᶜ) (hCont.tendsto)
  46  have hHit' : Tendsto Ξ l (𝓝 (1 : ℂ)) := hHit
  47  haveI : NeBot l := by
  48    -- `ℂ` has no isolated points, so punctured neighborhoods are nontrivial.
  49    simpa [l] using (show NeBot (𝓝[≠] z0) from inferInstance)
  50  exact tendsto_nhds_unique hCont' hHit'
  51
  52/-! ## Pinch lemma: Schur bound + holomorphic + nontrivial ⇒ no boundary hits -/
  53
  54/-- Back-end “pinch” lemma: if `Ξ` is holomorphic on a preconnected open region `Ω` and Schur-bounded
  55there, then any boundary hit forces `Ξ` to be constant `1` on `Ω`. -/
  56theorem eq_const_one_of_boundaryHit
  57    {Ω : Set ℂ} (hΩ_open : IsOpen Ω) (hΩ_conn : IsPreconnected Ω)
  58    {Ξ : ℂ → ℂ} (hHol : DifferentiableOn ℂ Ξ Ω)
  59    (hSchur : SchurOn Ω Ξ)
  60    {z0 : ℂ} (hz0 : z0 ∈ Ω) (hHit : BoundaryHitAt Ξ z0) :
  61    Set.EqOn Ξ (fun _ => (1 : ℂ)) Ω := by
  62  -- Step 1: continuity gives `Ξ z0 = 1`.
  63  have hContAt : ContinuousAt Ξ z0 :=
  64    (hHol.differentiableAt (hΩ_open.mem_nhds hz0)).continuousAt
  65  have hXi0 : Ξ z0 = (1 : ℂ) :=
  66    boundaryHit_implies_value_eq_one (Ξ := Ξ) (z0 := z0) hContAt hHit
  67
  68  -- Step 2: `‖Ξ‖` attains a maximum at `z0` on `Ω`.
  69  have hMax : IsMaxOn (norm ∘ Ξ) Ω z0 := by
  70    intro z hz
  71    have hz_le : ‖Ξ z‖ ≤ 1 := hSchur z hz
  72    -- rewrite the RHS as `‖Ξ z0‖ = 1`
  73    simpa [Function.comp, hXi0] using hz_le
  74
  75  -- Step 3: maximum modulus (strictly convex codomain) ⇒ Ξ is constant on Ω.
  76  have hConst : Set.EqOn Ξ (Function.const ℂ (Ξ z0)) Ω :=
  77    Complex.eqOn_of_isPreconnected_of_isMaxOn_norm
  78      (F := ℂ) (hc := hΩ_conn) (ho := hΩ_open) (hd := hHol) (hcU := hz0) (hm := hMax)
  79
  80  -- Step 4: substitute `Ξ z0 = 1`.
  81  refine hConst.trans ?_
  82  intro z hz
  83  simp [Function.const, hXi0]
  84
  85/-- Main back-end lemma: under Schur bound + holomorphic + nontriviality, `BoundaryHitAt` is impossible
  86at any `z0 ∈ Ω`. -/
  87theorem no_boundaryHit_of_schur_holomorphic_nontrivial
  88    {Ω : Set ℂ} (hΩ_open : IsOpen Ω) (hΩ_conn : IsPreconnected Ω)
  89    {Ξ : ℂ → ℂ} (hHol : DifferentiableOn ℂ Ξ Ω)
  90    (hSchur : SchurOn Ω Ξ)
  91    (hNontriv : ∃ z ∈ Ω, Ξ z ≠ (1 : ℂ)) :
  92    ∀ {z0 : ℂ}, z0 ∈ Ω → ¬ BoundaryHitAt Ξ z0 := by
  93  intro z0 hz0 hHit
  94  have hEq : Set.EqOn Ξ (fun _ => (1 : ℂ)) Ω :=
  95    eq_const_one_of_boundaryHit (Ω := Ω) hΩ_open hΩ_conn (Ξ := Ξ) hHol hSchur hz0 hHit
  96  rcases hNontriv with ⟨z1, hz1, hz1ne⟩
  97  exact hz1ne (hEq hz1)
  98
  99/-! ## A `BackEnd` constructor (certificate builder) -/
 100
 101/-- Build an RSA `BackEnd` from Schur bound + holomorphicity + nontriviality. -/
 102def backEnd_of_schur_holomorphic_nontrivial (P : Problem)
 103    (hΩ_open : IsOpen P.Ω) (hΩ_conn : IsPreconnected P.Ω)
 104    (hHol : DifferentiableOn ℂ P.Xi P.Ω)
 105    (hSchur : SchurOn P.Ω P.Xi)
 106    (hNontriv : ∃ z ∈ P.Ω, P.Xi z ≠ (1 : ℂ)) :
 107    BackEnd P :=
 108by
 109  refine ⟨hSchur, ?_⟩
 110  intro z0 hz0
 111  exact no_boundaryHit_of_schur_holomorphic_nontrivial
 112    (Ω := P.Ω) hΩ_open hΩ_conn (Ξ := P.Xi) hHol hSchur hNontriv hz0
 113
 114end RecognitionStabilityAudit
 115end Verification
 116end IndisputableMonolith
 117