other

forgeability_gap all-seven-green + Risk≤δ ⇏ TrueHarm≤δ

Lean spine source

formal/AlignmentProofSpine/Forgeability.lean

Declarations: forgeability_gap

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 forgeability_gap (δ : Int) :
    ∃ s : ForgeabilityToySuccessor,
      ForgeabilityToyAllSevenGreen s ∧
      ForgeabilityToyRiskBounded s δ ∧
      ¬ ForgeabilityToyTrueHarmBounded s δ :=
  ⟨⟨δ, δ + 1⟩, trivial, le_refl δ, by show ¬ δ + 1 ≤ δ; omega⟩