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 book’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.
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).