P13 Risk = Control − CCI

Declarations: P13_risk_gap_bounded_by_cci_slack

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 P13_risk_gap_bounded_by_cci_slack
    {A : System} {δ : Int}
    (h : Control A ≤ CCI A + δ) :
    RiskGap A ≤ δ := by
  unfold RiskGap; omega