proof

P31 Safe agent selected against

Lean spine source

Declarations: P31_safe_agent_selected_against

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 P31_safe_agent_selected_against :
    ∃ safe risky : Bool,
      ToySafe safe ∧ ¬ ToySafe risky ∧
        ToyDeploymentMass defaultEnvironment risky >
          ToyDeploymentMass defaultEnvironment safe :=
  ⟨true, false, rfl, by decide, by decide⟩