Towards Superintelligence Alignment
proof

Lean dependency spine

P43 Small-step drift

Lean spine source

formal/AlignmentProofSpine/Capability.lean

Declarations: P43_small_step_drift_can_accumulate

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 P43_small_step_drift_can_accumulate :
    ∀ K : Int, K > 0 → ∃ x0 xN : Int, xN - x0 > K := by
  intro K hK
  exact ⟨0, K + 1, by omega⟩

/-- Slow plotting: any positive hidden production rate eventually crosses any
    finite threshold if accumulation is not bounded by decay, reset, or ledgers. -/