Field projection — Deployment Safety / Safety Case

Deployment gates and safety cases ask whether evidence supports scaling compute or release. Episode-battery pass and regret bounds are projections of deployment safety — case-green plus tolerance does not imply Safe without scope discipline and MB11 bridge assumptions.

What decision changes?

Before treating a safety-case pass or low regret as deployment authorization, check scope boundaries and whether harm bounds transfer to the true deployment envelope.

Deployment safety and safety-case agendas ask whether evidence supports scaling compute, release, or pivotal deployment. This project treats episode-battery pass, regret bounds, and case-green status as projections of deployment-level Safe — not as substitutes for scope discipline.

Lean proves finite defeaters: MB11_defeater_toy_scope_exceeded when case reads green but scope is exceeded, and zero_regret_not_harm_bound showing regret alone does not discharge harm bounds. MB11 forward assembly remains an explicit bridge; the separations calibrate what case-green actually certifies.

What safety-case engineering keeps that this crosswalk does not replace: concrete hazard analysis templates, organizational sign-off workflows, and empirical validation batteries. The projection records logical dependencies; it does not replace a safety case document.

Formulas

SafetyCasePass  WithinDeploymentRiskTolerance ⇏ Safe\text{SafetyCasePass}\ \wedge\ \text{WithinDeploymentRiskTolerance}\ \not\Rightarrow\ \text{Safe}
Non-converse separation: case-green within stated tolerance does not imply Safe without scope discipline (MB11 defeater). (ch42)
ZeroRegretBound ⇏ HarmBound\text{ZeroRegretBound}\ \not\Rightarrow\ \text{HarmBound}
Regret separation: zero or bounded regret does not discharge harm bounds on finite interface. (ch44)
SafetyCaseAdequacy  Safe\text{SafetyCaseAdequacy}\ \Rightarrow\ \text{Safe}
Forward bridge: MB11 safety-case adequacy supports Safe when bridge assumptions hold. (ch42)

Lean source

Machine-checked declarations on the shared finite domain — each links to the theorem in the repo.

  • MB11_defeater_toy_scope_exceeded (counterexample) — MB11 toy defeater: safety case scope exceeded while case reads green within tolerance.
  • zero_regret_not_harm_bound (counterexample) — Finite separation: zero regret does not imply harm bound (RegretSafety toy).
  • regret_evidence_not_deployment_safe (counterexample) — Interface separation: regret evidence alone does not imply deployment safe.
  • MB11_safety_case_adequacy (bridge) — Bridge MB11: safety-case adequacy supports deployment-level Safe.