The Dynamical Guarantee
Alignment is not a snapshot property; it is a claim that a system stays inside an acceptable region across capability growth, feedback, and transformation.
What decision changes?
Ask whether a proposed safety property is stated as a fact about one moment, or as a probabilistic guarantee over a whole trajectory, within a certified class of systems and environments.
A static alignment claim has the form “at time t, system A has property P.” That is useful for ordinary software — does a program pass a test suite, respect an access policy, return a correct output — but it breaks for superintelligence, where the system learns, acquires tools, persuades users, and eventually produces successors. The same snapshot picture already strains for general intelligence once the system is embedded in learning, tools, institutions, and feedback loops.
This project’s replacement is a dynamical guarantee: a probabilistic claim that the system remains in, or returns to, an acceptable region of state space over a time horizon, conditional on starting inside a safety basin, the environment staying in a specified class, and the system belonging to a certified class of allowed transformations.
The distinction between a safe set, a bad set, and a basin matters here. A system can be safe right now while sitting outside the basin — a lab that behaves responsibly today while funding and competitive pressure push it toward dangerous deployment. A system can also enter a locally risky state while remaining inside a basin that reliably corrects it. The dynamical guarantee tracks the basin, not the snapshot.
The safety-case loop is closed by bridge MB11 (Deployment Safety) — see that card for the field crux, Lean bridge, and agree/differ notes.
Lean snippet
formal/playgrounds/P01-basin-invariant.lean/-!
Basin invariance (P01) — playground for `AlignmentProofSpine.P01_basin_invariant`.
Spine location: `formal/AlignmentProofSpine/Certification.lean`
Axiom footprint: `State`, `SafeState` (see `formal/axiom-ledger.json`).
Claim: if a safety predicate holds at the initial state and every transition
preserves it, it holds after any finite number of steps.
This file is self-contained for Lean 4 Web:
- `Safe` stands in for spine `SafeState`
- `iterateN` matches `AlignmentProofSpine.Core.iterateN`
- No Mathlib or spine imports
-/
namespace Playground
/-- Finite iteration of a step function (spine: `AlignmentProofSpine.iterateN`). -/
def iterateN {α : Type} (f : α → α) : Nat → α → α
| 0, x => x
| n + 1, x => iterateN f n (f x)
/-- Basin invariance: initial safety + step preservation ⇒ safety after n steps. -/
theorem basin_invariant {α : Type} (step : α → α) (Safe : α → Prop)
(x0 : α) (h0 : Safe x0) (hstep : ∀ x, Safe x → Safe (step x)) :
∀ n, Safe (iterateN step n x0) := by
have aux : ∀ n x, Safe x → Safe (iterateN step n x) := by
intro n
induction n with
| zero => intro x hx; exact hx
| succ k ih => intro x hx; exact ih (step x) (hstep x hx)
intro n
exact aux n x0 h0
/-- Spine names this `BasinStable`; same one-step preservation hypothesis. -/
def BasinStable {α : Type} (step : α → α) (B : α → Prop) : Prop :=
∀ x, B x → B (step x)
example : BasinStable id (fun (_ : Nat) => True) := by
intro _ _
trivial
example : ∀ n, (2 * n) % 2 = 0 := by
intro n
induction n with
| zero => rfl
| succ k ih => simp [Nat.mul_succ, ih]
#check basin_invariant
#check BasinStableTry this out
Open a self-contained snippet in theLean 4 Web editor with the infoview. The link preloads the full playground (inline compressed code, or GitHub raw when the snippet exceeds share-link size limits).