IndisputableMonolith.Verification.RecognitionStabilityAudit.RL

   1import Mathlib
   2
   3import Mathlib.Lean.Meta.Simp
   4
   5import IndisputableMonolith.Verification.RecognitionStabilityAudit
   6import IndisputableMonolith.Verification.RecognitionStabilityAudit.RL.Attr
   7
   8/-!
   9# RSA Reinforcement Learning (RL) module
  10
  11This module makes the Recognition Stability Audit pipeline **RL-friendly** inside Lean:
  12
  13- **Custom tags**
  14  - `@[rsa_simp]` marks *whitelisted rewrite/unfold lemmas* used by `rsa_simp`.
  15  - `@[rsa_milestone]` marks *milestone lemmas* that `rsa_step` is allowed to apply.
  16
  17- **Whitelisted tactics**
  18  - `rsa_simp` runs `simp` using **only** the `@[rsa_simp]` whitelist
  19    (plus Lean's `simp only` builtins).
  20  - `rsa_step` does one bounded step: try `assumption`, otherwise try applying a
  21    `@[rsa_milestone]` lemma (then discharge trivial subgoals), and finally fall back to `rsa_simp`.
  22
  23- **Canonical training goals**
  24  A small library of proved “gold” theorems (no `sorry`) that exercise the RSA pipeline.
  25
  26The intended use is: an LLM proposes the next `rsa_step`/`rsa_simp`/`apply` etc., and Lean provides
  27the reward signal by goal closure / checklist completion.
  28-/
  29
  30public meta section
  31
  32namespace IndisputableMonolith
  33namespace Verification
  34namespace RecognitionStabilityAudit
  35
  36open Lean Meta Elab Tactic
  37open scoped Topology
  38open Filter
  39
  40/-! ## Tactics -/
  41
  42private def getRsaSimpNames : MetaM (List Name) := do
  43  let env ← getEnv
  44  return (rsaSimpLemmaExt.getState env).toList
  45
  46private def getRsaMilestoneNames : MetaM (List Name) := do
  47  let env ← getEnv
  48  return (rsaMilestoneExt.getState env).toList
  49
  50/-- `rsa_simp` simplifies the goal using **only** the `@[rsa_simp]` whitelist (plus Lean's
  51`simp only` builtins). -/
  52elab "rsa_simp" : tactic => do
  53  let g ← getMainGoal
  54  g.withContext do
  55    let names ← getRsaSimpNames
  56    -- Build simp theorems from the whitelist, and also add *all Prop hypotheses* (like `simp [*]`)
  57    -- so simp can discharge side conditions (e.g. `ξ ≠ 1`) deterministically.
  58    let mut thms ← Lean.Meta.simpTheoremsOfNames names true
  59    let hyps ← Lean.Meta.Simp.getPropHyps
  60    for f in hyps do
  61      let decl ← f.getDecl
  62      thms ← thms.add (.fvar f) #[] decl.toExpr
  63    let ctx : Simp.Context ← Simp.mkContext { failIfUnchanged := false }
  64      (simpTheorems := #[thms])
  65      (congrTheorems := ← getSimpCongrTheorems)
  66    let (result?, _stats) ← simpGoal g ctx
  67    -- `simpGoal` returns `none` iff the goal is closed; otherwise it returns a fresh goal `g'`.
  68    match result? with
  69    | none => replaceMainGoal []
  70    | some (_fvars, g') => replaceMainGoal [g']
  71
  72/-- One bounded RL step: try `assumption`; otherwise try applying a `@[rsa_milestone]` lemma
  73(then discharge trivial subgoals); finally fall back to `rsa_simp`. -/
  74elab "rsa_step" : tactic => do
  75  -- First: if the goal is already in context, close it deterministically.
  76  try
  77    evalTactic (← `(tactic| assumption))
  78    return
  79  catch _ =>
  80    pure ()
  81
  82  -- Next: try applying a milestone lemma *before* simplifying,
  83  -- so we don't unfold away the high-level wrappers (e.g. `BoundaryHitAt`).
  84  let names ← getRsaMilestoneNames
  85  for n in names do
  86    try
  87      evalTactic (← `(tactic| apply $(mkIdent n)))
  88      evalTactic (← `(tactic| all_goals (try assumption)))
  89      evalTactic (← `(tactic| all_goals (try rsa_simp)))
  90      evalTactic (← `(tactic| all_goals (try assumption)))
  91      return
  92    catch _ =>
  93      continue
  94
  95  -- Fallback: a simplification-only step (useful when no milestone matches).
  96  try
  97    evalTactic (← `(tactic| rsa_simp))
  98    evalTactic (← `(tactic| all_goals (try assumption)))
  99    return
 100  catch _ =>
 101    pure ()
 102
 103  throwError "rsa_step: no applicable `@[rsa_milestone]` lemma"
 104
 105/-! ## Default RSA whitelist + milestones -/
 106
 107-- Small definitional rewrites we want available to `rsa_simp`.
 108@[rsa_simp] theorem BoundaryHitAt_def (Ξ : ℂ → ℂ) (z0 : ℂ) :
 109    BoundaryHitAt Ξ z0 = Tendsto Ξ (𝓝[({z0} : Set ℂ)ᶜ] z0) (𝓝 (1 : ℂ)) := rfl
 110
 111@[rsa_simp] theorem SchurOn_def (Ω : Set ℂ) (f : ℂ → ℂ) :
 112    SchurOn Ω f = (∀ z ∈ Ω, ‖f z‖ ≤ 1) := rfl
 113
 114@[rsa_simp] theorem Problem_XiFromSensor_def (𝓙 : ℂ → ℂ) :
 115    Problem.XiFromSensor 𝓙 = fun z => theta (𝓙 z) := rfl
 116
 117@[rsa_simp] theorem SensorBlowsUpAt_def (𝓙 : ℂ → ℂ) (z0 : ℂ) :
 118    SensorBlowsUpAt 𝓙 z0 = Tendsto (fun z => ‖𝓙 z‖) (𝓝[({z0} : Set ℂ)ᶜ] z0) atTop := rfl
 119
 120@[rsa_simp] theorem sensorOfObstruction_def (G : ℂ → ℂ) :
 121    sensorOfObstruction G = fun z => (G z)⁻¹ := rfl
 122
 123-- Milestones (apply targets)
 124attribute [rsa_milestone]
 125  -- Cayley plumbing (explicit step, avoids rewriting away useful structure too early)
 126  theta_eq_div
 127  invTheta_theta
 128  theta_invTheta
 129  correctness
 130  frontEnd_of_obstruction
 131  backEnd_of_schur_holomorphic_nontrivial
 132  boundaryHit_theta_of_sensorBlowsUp
 133  sensorBlowsUpAt_of_tendsto_zero
 134  no_boundaryHit_of_schur_holomorphic_nontrivial
 135  boundaryHit_implies_value_eq_one
 136  eq_const_one_of_boundaryHit
 137
 138/-! ## Canonical training goals (all proved, no `sorry`) -/
 139
 140namespace RLGoals
 141
 142open scoped Real Topology
 143open Filter
 144
 145/-- A tiny `rsa_simp` sanity check (uses only whitelisted lemmas). -/
 146theorem goal_theta_eq_div (J : ℂ) : theta J = (2 * J - 1) / (2 * J + 1) := by
 147  rsa_step
 148
 149/-- Cayley inverse micro-goal: `theta (invTheta ξ) = ξ`. -/
 150theorem goal_theta_invTheta (ξ : ℂ) (h : ξ ≠ 1) : theta (invTheta ξ) = ξ := by
 151  rsa_step
 152
 153/-- Cayley inverse micro-goal: `invTheta (theta J) = J`. -/
 154theorem goal_invTheta_theta (J : ℂ) (h : (2 * J + 1) ≠ 0) : invTheta (theta J) = J := by
 155  rsa_step
 156
 157/-- Front-end micro-goal: sensor blow-up implies the compiled boundary hit. -/
 158theorem goal_pole_implies_boundaryHit (𝓙 : ℂ → ℂ) (z0 : ℂ)
 159    (h : SensorBlowsUpAt 𝓙 z0) :
 160    BoundaryHitAt (fun z => theta (𝓙 z)) z0 := by
 161  rsa_step
 162
 163/-- Front-end micro-goal: obstruction tends to `0` + stays nonzero ⇒ sensor blows up. -/
 164theorem goal_obstruction_to_sensor_blowup (G : ℂ → ℂ) (z0 : ℂ)
 165    (h0 : Tendsto G (𝓝[({z0} : Set ℂ)ᶜ] z0) (𝓝 (0 : ℂ)))
 166    (hne : ∀ᶠ z in (𝓝[({z0} : Set ℂ)ᶜ] z0), G z ≠ 0) :
 167    SensorBlowsUpAt (sensorOfObstruction G) z0 := by
 168  rsa_step
 169
 170/-- A canonical FrontEnd goal: the candidate *provides* the two analytic obligations
 171(`G → 0` and eventual `G ≠ 0` on the punctured neighborhood), and `FrontEnd` compiles it
 172into a boundary-hit. -/
 173theorem goal_frontEnd_from_candidate_obligations
 174    (Ω : Set ℂ) (G : ℂ → ℂ) :
 175    let Candidate : ℂ → Prop :=
 176      fun z0 =>
 177        Tendsto G (𝓝[({z0} : Set ℂ)ᶜ] z0) (𝓝 (0 : ℂ))
 178          ∧ ∀ᶠ z in (𝓝[({z0} : Set ℂ)ᶜ] z0), G z ≠ 0
 179    FrontEnd
 180      { Ω := Ω
 181        Candidate := Candidate
 182        Xi := fun z => theta ((G z)⁻¹) } := by
 183  intro Candidate
 184  -- Build via the FrontEnd constructor.
 185  refine frontEnd_of_obstruction (Ω := Ω) (Candidate := Candidate) (G := G) ?_ ?_
 186  · intro z0 _hz0 hC
 187    exact hC.1
 188  · intro z0 _hz0 hC
 189    exact hC.2
 190
 191/-- Back-end micro-goal: boundary hit + continuity forces the value `Ξ z0 = 1`. -/
 192theorem goal_boundaryHit_value (Ξ : ℂ → ℂ) (z0 : ℂ)
 193    (hCont : ContinuousAt Ξ z0)
 194    (hHit : BoundaryHitAt Ξ z0) :
 195    Ξ z0 = (1 : ℂ) := by
 196  rsa_step
 197
 198/-- Back-end micro-goal: boundary hit forces constancy `Ξ ≡ 1` under holomorphic + Schur. -/
 199theorem goal_boundaryHit_forces_const_one
 200    (Ω : Set ℂ) (Ξ : ℂ → ℂ)
 201    (hΩo : IsOpen Ω) (hΩc : IsPreconnected Ω)
 202    (hHol : DifferentiableOn ℂ Ξ Ω)
 203    (hSchur : SchurOn Ω Ξ)
 204    (z0 : ℂ) (hz0 : z0 ∈ Ω)
 205    (hHit : BoundaryHitAt Ξ z0) :
 206    Set.EqOn Ξ (fun _ => (1 : ℂ)) Ω := by
 207  rsa_step
 208
 209/-- A canonical BackEnd goal: constant `Ξ ≡ 0` on `Ω = univ` is holomorphic, Schur-bounded,
 210and nontrivial (≠ 1), hence admits a `BackEnd` certificate. -/
 211theorem goal_backEnd_const_zero :
 212    BackEnd
 213      { Ω := (Set.univ : Set ℂ)
 214        Candidate := fun _ => False
 215        Xi := fun _ => (0 : ℂ) } := by
 216  -- Use the generic back-end constructor.
 217  refine backEnd_of_schur_holomorphic_nontrivial
 218    (P := { Ω := (Set.univ : Set ℂ), Candidate := fun _ => False, Xi := fun _ => (0 : ℂ) })
 219    (hΩ_open := isOpen_univ) (hΩ_conn := isPreconnected_univ) ?_ ?_ ?_
 220  · simp
 221  · intro _z _hz
 222    simp
 223  · refine ⟨0, by simp, ?_⟩
 224    norm_num
 225
 226/-- End-to-end micro-goal: with `Ω = univ`, the candidate `False` is ruled out immediately. -/
 227theorem goal_correctness_trivial_univ :
 228    ∀ {z0 : ℂ}, z0 ∈ (Set.univ : Set ℂ) → ¬ (False) := by
 229  intro z0 hz0 hFalse
 230  exact hFalse
 231
 232/-- End-to-end RSA goal (compiler correctness): if you supply
 233
 234- a FrontEnd compilation of a candidate into a boundary-hit, and
 235- a BackEnd certificate forbidding boundary hits,
 236
 237then the candidate is impossible in the audited region. -/
 238theorem goal_correctness_usage
 239    (P : Problem) (FE : FrontEnd P) (BE : BackEnd P) :
 240    ∀ {z0 : ℂ}, z0 ∈ P.Ω → ¬ P.Candidate z0 := by
 241  intro z0 hz0
 242  exact correctness (P := P) FE BE hz0
 243
 244end RLGoals
 245
 246/-! ## RS → RL Bridge Training Goals
 247
 248These goals exercise the machinery from `RStoRL.lean`:
 249- Virtue-based action space (14 virtues as generators)
 250- Gibbs/thermodynamic policy
 251- Lexicographic multi-objective selection
 252- Eight-tick cadence evaluation
 253-/
 254
 255namespace RStoRLGoals
 256
 257open RStoRL
 258
 259/-- VirtueAction: zero action has zero norm. -/
 260theorem goal_virtueAction_zero_norm : VirtueAction.zero.norm = 0 :=
 261  virtueAction_zero_norm
 262
 263/-- VirtueAction: norm is non-negative. -/
 264theorem goal_virtueAction_norm_nonneg (a : VirtueAction) : 0 ≤ a.norm :=
 265  virtueAction_norm_nonneg a
 266
 267/-- VirtueAction: scaling by positive factor scales norm. -/
 268theorem goal_virtueAction_scale_norm (a : VirtueAction) (c : ℝ) (hc : 0 ≤ c) :
 269    (a.scale c).norm = c * a.norm :=
 270  virtueAction_scale_norm a c hc
 271
 272/-- Lexicographic: comparison is irreflexive (no action is strictly better than itself). -/
 273theorem goal_lexBetter_irrefl (r : AuditResult) : ¬lexBetter r r :=
 274  lexBetter_irrefl r
 275
 276/-- Gibbs: weights are always positive (ensures exploration). -/
 277theorem goal_gibbs_weight_pos (g : GibbsPolicy) (s : MoralState) (a : VirtueAction) :
 278    0 < g.weight s a :=
 279  gibbs_weight_pos g s a
 280
 281/-- Gibbs: partition function is positive for non-empty action sets. -/
 282theorem goal_gibbs_partitionFn_pos (g : GibbsPolicy) (s : MoralState)
 283    (actions : List VirtueAction) (h : actions ≠ []) :
 284    0 < g.partitionFn s actions :=
 285  gibbs_partitionFn_pos g s actions h
 286
 287/-- Eight-tick: total value over cadence is well-defined. -/
 288theorem goal_eightTick_value_finite (c : EightTickCadence)
 289    (valueAt : MoralState → ℝ) : ∃ v : ℝ, v = c.totalValue valueAt :=
 290  eightTick_value_finite c valueAt
 291
 292/-- Feasibility: σ=0 is the hard constraint for admissibility. -/
 293theorem goal_sigma_feasibility (s : MoralState) :
 294    SigmaFeasible s ↔ s.skew = 0 := by
 295  rfl
 296
 297/-- Harm bound: ΔS ≤ 0 means no externalized harm. -/
 298theorem goal_harm_bound_zero (deltaS : ℝ) :
 299    HarmBound deltaS 0 ↔ deltaS ≤ 0 := by
 300  rfl
 301
 302/-- Consent: D_j V_i ≥ 0 is the consent condition. -/
 303theorem goal_consent_condition (dV : ℝ) :
 304    SatisfiesConsent dV ↔ 0 ≤ dV := by
 305  rfl
 306
 307/-- Parasitism threshold uses φ (golden ratio). -/
 308theorem goal_parasitism_threshold_phi :
 309    parasitismThreshold = 1 / φ := by
 310  rfl
 311
 312/-- LACompletion identity: identity projector preserves actions. -/
 313theorem goal_LACompletion_identity_project (a : VirtueAction) :
 314    LACompletion.identity.project a = a := by
 315  rfl
 316
 317/-- Temperance: energy budget constraint via φ. -/
 318theorem goal_temperance_check (a : VirtueAction) (budget : ℝ) :
 319    a.satisfiesTemperance budget ↔ a.energyCost ≤ budget / φ := by
 320  rfl
 321
 322end RStoRLGoals
 323
 324end RecognitionStabilityAudit
 325end Verification
 326end IndisputableMonolith
 327
 328end
 329