proof

P13 Risk = Control − CCI

Lean spine source

Declarations: P13_risk_gap_bounded_by_cci_slack

From the machine-checked spine in formal/ (Mathlib + spine imports). 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