IndisputableMonolith.Verification.RecognitionStabilityAudit.FrontEnd

   1import Mathlib
   2
   3import IndisputableMonolith.Verification.RecognitionStabilityAudit.Core
   4import IndisputableMonolith.Verification.RecognitionStabilityAudit.Cayley
   5
   6/-!
   7# Recognition Stability Audit (RSA): front-end (obstruction/sensor ⇒ boundary hit)
   8
   9This file formalizes the RSA “front-end” step from the manuscript:
  10
  111. **Obstruction** `G` (holomorphic representative of a defect/claim).
  122. **Sensor** `𝓙 := 1/G`.
  133. **Cayley field** `Ξ := theta 𝓙 = (2𝓙-1)/(2𝓙+1)`.
  144. **Pole ⇒ boundary hit**: if `𝓙` blows up at `z0`, then `Ξ → 1` along the punctured neighborhood.
  15
  16We intentionally phrase “pole” as a *norm blow-up* condition. This is strong enough for RSA
  17and avoids dragging in meromorphic machinery at the interface layer (domain instantiations can
  18later strengthen it to “has a pole” in the analytic sense).
  19-/
  20
  21namespace IndisputableMonolith
  22namespace Verification
  23namespace RecognitionStabilityAudit
  24
  25open scoped Real Topology
  26open Filter Bornology
  27
  28/-! ## Sensor blow-up and the Cayley boundary hit -/
  29
  30/-- “Pole”/blow-up condition for a sensor `𝓙` at `z0`: the norm tends to `+∞` on a punctured
  31neighborhood. -/
  32def SensorBlowsUpAt (𝓙 : ℂ → ℂ) (z0 : ℂ) : Prop :=
  33  Tendsto (fun z => ‖𝓙 z‖) (𝓝[({z0} : Set ℂ)ᶜ] z0) atTop
  34
  35/-- Core lemma: **sensor blow-up ⇒ Cayley field hits 1**.
  36
  37This is the paper identity `Ξ(J) - 1 = -2/(2J+1)` plus the fact that `‖2J+1‖ → ∞` when `‖J‖ → ∞`. -/
  38theorem boundaryHit_theta_of_sensorBlowsUp {𝓙 : ℂ → ℂ} {z0 : ℂ}
  39    (hBlow : SensorBlowsUpAt 𝓙 z0) :
  40    BoundaryHitAt (fun z => theta (𝓙 z)) z0 := by
  41  -- Write `l` for the punctured neighborhood filter.
  42  set l : Filter ℂ := (𝓝[({z0} : Set ℂ)ᶜ] z0)
  43
  44  have hNorm_atTop : Tendsto (fun z => ‖𝓙 z‖) l atTop := hBlow
  45
  46  -- First, `‖2*𝓙 z + 1‖ → +∞` by a reverse-triangle lower bound.
  47  have hDen_atTop : Tendsto (fun z => ‖(2 * 𝓙 z + 1 : ℂ)‖) l atTop := by
  48    refine (tendsto_atTop.2 ?_)
  49    intro A
  50    -- Choose `B := (A+1)/2` and ask that `‖𝓙 z‖ ≥ B`.
  51    have hB : ∀ᶠ z in l, (A + 1) / 2 ≤ ‖𝓙 z‖ :=
  52      hNorm_atTop.eventually (eventually_ge_atTop ((A + 1) / 2))
  53    filter_upwards [hB] with z hz
  54    -- `‖2J+1‖ ≥ 2‖J‖ - 1`
  55    have htri : ‖(2 * 𝓙 z : ℂ)‖ ≤ ‖(2 * 𝓙 z + 1 : ℂ)‖ + ‖(1 : ℂ)‖ := by
  56      -- `2J = (2J+1) - 1`
  57      have hsub : ‖(2 * 𝓙 z + 1 : ℂ) - (1 : ℂ)‖ ≤ ‖(2 * 𝓙 z + 1 : ℂ)‖ + ‖(1 : ℂ)‖ :=
  58        norm_sub_le (2 * 𝓙 z + 1) (1 : ℂ)
  59      -- rewrite `((2J+1)-1) = 2J` in `hsub`
  60      simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using hsub
  61    have hrev : ‖(2 * 𝓙 z : ℂ)‖ - ‖(1 : ℂ)‖ ≤ ‖(2 * 𝓙 z + 1 : ℂ)‖ := by
  62      linarith [htri]
  63    have hLower : (2 : ℝ) * ‖𝓙 z‖ - 1 ≤ ‖(2 * 𝓙 z + 1 : ℂ)‖ := by
  64      -- `‖2J‖ = 2‖J‖`, `‖1‖ = 1`
  65      simpa [norm_mul, (by norm_num : ‖(2 : ℂ)‖ = (2 : ℝ))] using hrev
  66    -- From `hz : (A+1)/2 ≤ ‖J‖` we get `A ≤ 2‖J‖ - 1`.
  67    have hA : A ≤ (2 : ℝ) * ‖𝓙 z‖ - 1 := by
  68      nlinarith
  69    exact le_trans hA hLower
  70
  71  -- Convert `‖den‖ → ∞` into `den → cobounded`, then invert to get `den⁻¹ → 0`.
  72  have hDen_cob : Tendsto (fun z => (2 * 𝓙 z + 1 : ℂ)) l (cobounded ℂ) :=
  73    (tendsto_norm_atTop_iff_cobounded).1 hDen_atTop
  74  have hInv : Tendsto (fun z => (2 * 𝓙 z + 1 : ℂ)⁻¹) l (𝓝 (0 : ℂ)) :=
  75    (Filter.tendsto_inv₀_cobounded (α := ℂ)).comp hDen_cob
  76
  77  -- We will use the identity `theta(J) = 1 + (-2)/(2J+1)` (valid when `2J+1 ≠ 0`).
  78  have hDen_ne : ∀ᶠ z in l, (2 * 𝓙 z + 1 : ℂ) ≠ 0 := by
  79    have hpos : ∀ᶠ z in l, (0 : ℝ) < ‖(2 * 𝓙 z + 1 : ℂ)‖ :=
  80      hDen_atTop.eventually (eventually_gt_atTop (0 : ℝ))
  81    filter_upwards [hpos] with z hz
  82    exact (norm_pos_iff.1 hz)
  83
  84  have hTheta_eq :
  85      (fun z => theta (𝓙 z)) =ᶠ[l] (fun z => (-2 : ℂ) * (2 * 𝓙 z + 1)⁻¹ + (1 : ℂ)) := by
  86    filter_upwards [hDen_ne] with z hz
  87    -- `field_simp` uses `hz` to justify clearing denominators.
  88    have hz' : (2 * 𝓙 z + 1 : ℂ) ≠ 0 := hz
  89    -- Expand `theta`, then compute.
  90    simp [theta_eq_div]
  91    field_simp [hz']
  92    ring
  93
  94  -- The RHS tends to `1` since `(2J+1)⁻¹ → 0`.
  95  have hRhs :
  96      Tendsto (fun z => (-2 : ℂ) * (2 * 𝓙 z + 1)⁻¹ + (1 : ℂ)) l (𝓝 (1 : ℂ)) := by
  97    have hMul : Tendsto (fun z => (-2 : ℂ) * (2 * 𝓙 z + 1)⁻¹) l (𝓝 (0 : ℂ)) := by
  98      simpa using ((tendsto_const_nhds (x := (-2 : ℂ))).mul hInv)
  99    -- Add the constant `1`.
 100    -- Keep the normal form `(-2*inv)+1` to avoid commutativity issues.
 101    have : Tendsto (fun z => (-2 : ℂ) * (2 * 𝓙 z + 1)⁻¹ + (1 : ℂ)) l (𝓝 ((0 : ℂ) + (1 : ℂ))) :=
 102      hMul.add_const (1 : ℂ)
 103    simpa [add_comm, add_left_comm, add_assoc] using this
 104
 105  -- Transfer along the eventual equality.
 106  exact hRhs.congr' hTheta_eq.symm
 107
 108/-! ## From obstruction `G` to sensor blow-up `𝓙 = 1/G` -/
 109
 110/-- Sensor associated to an obstruction `G`: `𝓙 = 1/G`. -/
 111noncomputable def sensorOfObstruction (G : ℂ → ℂ) : ℂ → ℂ :=
 112  fun z => (G z)⁻¹
 113
 114/-- If `G z → 0` in a punctured neighborhood and is eventually nonzero, then `‖1/G z‖ → ∞`.
 115
 116This packages the generic filter lemma needed by RSA, and it is exactly what domain instantiations
 117prove when they show “candidate ⇒ obstruction has a (simple) zero”.
 118-/
 119theorem sensorBlowsUpAt_of_tendsto_zero
 120    {G : ℂ → ℂ} {z0 : ℂ}
 121    (h0 : Tendsto G (𝓝[({z0} : Set ℂ)ᶜ] z0) (𝓝 (0 : ℂ)))
 122    (hne : ∀ᶠ z in (𝓝[({z0} : Set ℂ)ᶜ] z0), G z ≠ 0) :
 123    SensorBlowsUpAt (sensorOfObstruction G) z0 := by
 124  -- First upgrade `G → 0` to `G → 0` within `≠ 0` (in the codomain).
 125  have h0' : Tendsto G (𝓝[({z0} : Set ℂ)ᶜ] z0) (𝓝[{(0 : ℂ)}ᶜ] (0 : ℂ)) :=
 126    tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
 127      (f := G) (a := (0 : ℂ)) (s := ({(0 : ℂ)}ᶜ : Set ℂ)) h0 (hne.mono (fun z hz => by
 128        simpa using hz))
 129  -- Now apply the Mathlib lemma: `‖x⁻¹‖ → ∞` as `x → 0` punctured.
 130  -- (`tendsto_norm_inv_nhdsNE_zero_atTop` is the codomain statement at `0`.)
 131  have hInv :
 132      Tendsto (fun w : ℂ => ‖w⁻¹‖) (𝓝[{(0 : ℂ)}ᶜ] (0 : ℂ)) atTop :=
 133    (tendsto_norm_inv_nhdsNE_zero_atTop (α := ℂ))
 134  -- Compose and simplify.
 135  simpa [SensorBlowsUpAt, sensorOfObstruction, Function.comp] using (hInv.comp h0')
 136
 137/-! ## A reusable `FrontEnd` constructor for “obstruction ⇒ boundary hit” -/
 138
 139/-- A front-end “compiler” instance built from an obstruction `G` and two analytic obligations:
 140
 141- candidate ⇒ `G → 0` in the punctured neighborhood;
 142- candidate ⇒ `G ≠ 0` eventually on the punctured neighborhood.
 143
 144Then the RSA Cayley field `Ξ = theta(1/G)` hits the boundary state `1`.
 145-/
 146def frontEnd_of_obstruction (Ω : Set ℂ) (Candidate : ℂ → Prop) (G : ℂ → ℂ)
 147    (h0 : ∀ {z0}, z0 ∈ Ω → Candidate z0 → Tendsto G (𝓝[({z0} : Set ℂ)ᶜ] z0) (𝓝 (0 : ℂ)))
 148    (hne : ∀ {z0}, z0 ∈ Ω → Candidate z0 → ∀ᶠ z in (𝓝[({z0} : Set ℂ)ᶜ] z0), G z ≠ 0) :
 149    FrontEnd
 150      { Ω := Ω
 151        Candidate := Candidate
 152        Xi := fun z => theta ((G z)⁻¹) } :=
 153by
 154  refine ⟨?_⟩
 155  intro z0 hz0 hC
 156  have hBlow : SensorBlowsUpAt (sensorOfObstruction G) z0 :=
 157    sensorBlowsUpAt_of_tendsto_zero (G := G) (z0 := z0) (h0 hz0 hC) (hne hz0 hC)
 158  -- Pole ⇒ boundary hit.
 159  simpa [sensorOfObstruction] using
 160    (boundaryHit_theta_of_sensorBlowsUp (𝓙 := sensorOfObstruction G) (z0 := z0) hBlow)
 161
 162end RecognitionStabilityAudit
 163end Verification
 164end IndisputableMonolith
 165