proof

P43 Small-step drift

Lean spine source

Declarations: P43_small_step_drift_can_accumulate

From the machine-checked spine in formal/ (Mathlib + spine imports). 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. -/