Towards Superintelligence Alignment
other

Lean dependency spine

Selection / basin MB6b_defeater_toy_lock_in P31_safe_agent_selected_against

Lean spine source

formal/AlignmentProofSpine/Defeaters.lean

Declarations: MB6b_defeater_toy_lock_in, P31_safe_agent_selected_against

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 MB6b_defeater_toy_lock_in :
    ∃ b : MB6bDefeaterToyBasin,
      MB6bDefeaterToyBasinStable b ∧ ¬ MB6bDefeaterToyCorrectionIntegrityFromBasin b :=
  ⟨MB6bDefeaterToyBasin.lockedInBad, trivial, by simp⟩

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⟩