proof

P35 Basin stability

Lean spine source

Declarations: P35_basin_stability_induction

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 P35_basin_stability_induction
    (step : State → State)
    (B : State → Prop)
    (x0 : State)
    (hstable : BasinStable step B)
    (h0 : B x0) :
    ∀ n : Nat, B (iterateN step n x0) := by
  have aux : ∀ n x, B x → B (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) (hstable x hx)
  intro n; exact aux n x0 h0