other

Deployment gate MB11_defeater_toy_scope_exceeded zero_regret_not_harm_bound

Lean spine source

formal/AlignmentProofSpine/Defeaters.lean

Declarations: MB11_defeater_toy_scope_exceeded, zero_regret_not_harm_bound, regret_evidence_not_deployment_safe

From the machine-checked spine in formal/ (core modules are Mathlib-free;Field/Finite/ may import Mathlib). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem MB11_defeater_toy_scope_exceeded :
    ∃ c : MB11DefeaterToyCase,
      MB11DefeaterToyAntecedent c ∧
        MB11DefeaterToyScopeExceeded c ∧
        ¬ MB11DefeaterToySafe c :=
  ⟨⟨true, true, true, false⟩, ⟨rfl, rfl⟩, rfl, by simp⟩

theorem zero_regret_not_harm_bound :
    ∃ (trace : List RegretStep) (comparator : RegretAction),
      cumulativeRegret trace comparator = 0 ∧
        (trace.map stepHarm).sum > 0 := by
  refine ⟨[{ env := .catastrophic, act := .a }], .b, ?_, ?_⟩
  · simp [cumulativeRegret, learningLoss]
  · simp [stepHarm, harmCost]

/-- Prefix catastrophe: a finite trace can have bounded cumulative regret
    (here zero) while containing an irreversible harm event. Average/regret
    performance does not imply prefix safety. -/

theorem regret_evidence_not_deployment_safe :
    ∃ t : RegretInterfaceToy,
      t.hasRegretEvidence = true ∧ t.safe = false :=
  ⟨⟨true, true, false⟩, rfl, rfl⟩

/-- Independence toy: regret evidence can hold while the capacity `RiskGap`
    leaf fails — different formal object. -/