IndisputableMonolith.Verification.RecognitionStabilityAudit.Core

   1import Mathlib
   2
   3import IndisputableMonolith.Cost
   4import IndisputableMonolith.Verification.RecognitionStabilityAudit.Cayley
   5
   6/-!
   7# Recognition Stability Audit (RSA): core interface (RL-friendly)
   8
   9This module is the Lean “home” for the **Recognition Stability Audit** described in
  10`papers/tex/Recognition_Stability_Audit.tex`.
  11
  12## What this file is (and why it’s structured this way)
  13
  14RSA is best read as a **compiler**:
  15
  16- **Front-end**: compile a candidate existence claim into a *boundary hit* condition for a
  17  bounded Cayley field `Ξ` (morally: candidate ⇒ sensor pole ⇒ `Ξ → 1`).
  18- **Back-end**: produce a **finite certificate** that `Ξ` stays inside the Schur class on the
  19  audited region (and therefore cannot hit the forbidden boundary state).
  20- **Correctness theorem**: if both sides succeed, the candidate is impossible in the audited
  21  region.
  22
  23This file is intentionally **RL-friendly**:
  24
  25- We represent each RSA step as a small `structure` (a checklist of proof obligations).
  26- The top-level theorem only uses those obligations, so an LLM can “train” by learning to
  27  fill in the structures (front-end encodings + back-end certificates).
  28
  29## Relation to the canonical RS cost `J`
  30
  31RSA uses the canonical reciprocal cost `J(x) = ½(x + x⁻¹) − 1` on `ℝ_{>0}` as its
  32foundational cost primitive. In this repository that function is already formalized as
  33`IndisputableMonolith.Cost.Jcost`.
  34
  35This file doesn’t re-prove cost uniqueness; it only *references* the cost layer and focuses
  36on the audit pipeline interface.
  37-/
  38
  39namespace IndisputableMonolith
  40namespace Verification
  41namespace RecognitionStabilityAudit
  42
  43open scoped Real Topology
  44open Filter
  45
  46/-! ## Small reusable predicates -/
  47
  48/-- Schur bound (disk bound) on a region `Ω`: `‖f z‖ ≤ 1` for all `z ∈ Ω`. -/
  49def SchurOn (Ω : Set ℂ) (f : ℂ → ℂ) : Prop :=
  50  ∀ z ∈ Ω, ‖f z‖ ≤ 1
  51
  52/-- Boundary hit at a point: along the punctured neighborhood of `z0`, the field tends to `1`.
  53
  54This is the *compiled* forbidden-event predicate in RSA:
  55candidate ⇒ boundary hit (usually via `sensor pole ⇒ Ξ → 1`). -/
  56def BoundaryHitAt (Ξ : ℂ → ℂ) (z0 : ℂ) : Prop :=
  57  Tendsto Ξ (𝓝[({z0} : Set ℂ)ᶜ] z0) (𝓝 (1 : ℂ))
  58
  59/-! ## The RSA problem interface -/
  60
  61/-- An RSA “problem instance”: a region `Ω` to audit, a candidate predicate, and the Cayley
  62field `Ξ` that the audit will certify as Schur-bounded. -/
  63structure Problem where
  64  /-- Audited region (typically a chart domain after normalization to `𝔻`). -/
  65  Ω : Set ℂ
  66  /-- Candidate predicate (“the monster”): the existence claim we try to rule out on `Ω`. -/
  67  Candidate : ℂ → Prop
  68  /-- Audited Cayley field. In the paper this is `Ξ = (2𝓙-1)/(2𝓙+1)` after pullback. -/
  69  Xi : ℂ → ℂ
  70
  71namespace Problem
  72
  73/-- Convenience: the paper-facing Cayley field `Ξ` arising from a “sensor” `𝓙`. -/
  74noncomputable def XiFromSensor (𝓙 : ℂ → ℂ) : ℂ → ℂ :=
  75  fun z => theta (𝓙 z)
  76
  77end Problem
  78
  79/-! ## RSA front-end: candidate ⇒ boundary hit -/
  80
  81/-- Front-end obligations: compile the candidate into a boundary-hit statement for `Ξ`. -/
  82structure FrontEnd (P : Problem) : Prop where
  83  /-- If the candidate holds at `z0 ∈ Ω`, then the Cayley field hits the forbidden boundary:
  84  `Ξ → 1` along the punctured neighborhood. -/
  85  candidate_implies_boundaryHit :
  86      ∀ {z0 : ℂ}, z0 ∈ P.Ω → P.Candidate z0 → BoundaryHitAt P.Xi z0
  87
  88/-! ## RSA back-end: finite certificate ⇒ no boundary hits -/
  89
  90/-- Back-end obligations: a (finite) certificate that prevents boundary hits.
  91
  92In the paper, this is realized via Schur / Herglotz theory (bounded-real / Pick-gap-plus-tail)
  93plus the “pinch” argument. Here we keep the interface explicit: the certificate must supply
  94both the global Schur bound and the derived “no boundary hit” conclusion.
  95-/
  96structure BackEnd (P : Problem) : Prop where
  97  /-- Global Schur bound for `Ξ` on `Ω`. -/
  98  schur_bound : SchurOn P.Ω P.Xi
  99  /-- The “pinch” outcome: `Ξ` cannot hit the forbidden boundary at any interior point of `Ω`.
 100  (Domain instantiations discharge this from `schur_bound` + analyticity + nontriviality.) -/
 101  no_boundary_hit : ∀ {z0 : ℂ}, z0 ∈ P.Ω → ¬ BoundaryHitAt P.Xi z0
 102
 103/-! ## RSA correctness theorem (the training target) -/
 104
 105/-- **RSA correctness (audit soundness)**:
 106
 107If the front-end compiles the candidate into a boundary hit, and the back-end certificate
 108rules out boundary hits on the audited region, then the candidate cannot occur in the region.
 109-/
 110theorem correctness (P : Problem) (FE : FrontEnd P) (BE : BackEnd P) :
 111    ∀ {z0 : ℂ}, z0 ∈ P.Ω → ¬ P.Candidate z0 := by
 112  intro z0 hz0 hCand
 113  have hHit : BoundaryHitAt P.Xi z0 :=
 114    FE.candidate_implies_boundaryHit hz0 hCand
 115  exact (BE.no_boundary_hit (z0 := z0) hz0) hHit
 116
 117end RecognitionStabilityAudit
 118end Verification
 119end IndisputableMonolith
 120