iterate_defect_nonincreasing
Iterating any one-step dynamics whose defect is nonincreasing at each step keeps the defect nonincreasing after any finite number of iterations. Lattice modelers working on discrete Navier-Stokes or cellular automata would cite this to justify stability across repeated time windows. The proof is by induction on the iteration count, with the zero case immediate and the successor case chaining the single-step property through transitivity of the order.
claimLet dyn be a one-step dynamics on a type α, consisting of a step map step : α → α and a defect map defect : α → ℝ such that defect(step(s)) ≤ defect(s) for all s. Then for every natural number n and state s, defect((step^[n]) s) ≤ defect(s).
background
OneStepDynamics α is an abstract structure bundling a step function α → α, a defect functional α → ℝ, and the single-step axiom that each application of step does not increase defect. The module treats time as discrete, with the fundamental tick as the RS-native time quantum, so that an 8-tick window becomes the natural stability unit for the Navier-Stokes lattice program. The result depends on the transitivity theorem for the order relation supplied by the arithmetic foundations.
proof idea
Proof by induction on n. The zero case reduces immediately by simplification. In the successor case, rewrite the (n+1)-fold iterate as one additional step applied to the n-fold iterate, apply the single-step defect_nonincreasing property to the intermediate state, and chain the resulting inequality to the inductive hypothesis via le_trans.
why it matters in Recognition Science
This lemma supplies the iteration step that lets the single-step property lift to the 8-tick window operator and to arbitrary numbers of windows, as consumed by step8_defect_nonincreasing and window_certificate_extends. It thereby supports the eight-tick octave as the fundamental evolution period and the propagation of defect certificates in the D=3 spatial setting of the Recognition framework.
scope and limits
- Does not construct or prove existence of any concrete dynamics.
- Does not address convergence to a continuous-time limit.
- Does not bound defect from below or establish positivity.
- Does not incorporate spatial locality or cellular-automaton rules.
Lean usage
example {α : Type} (dyn : OneStepDynamics α) (n : ℕ) (s : α) : dyn.defect ((dyn.step^[n]) s) ≤ dyn.defect s := iterate_defect_nonincreasing dyn n sformal statement (Lean)
32theorem iterate_defect_nonincreasing {α : Type} (dyn : OneStepDynamics α) :
33 ∀ n s, dyn.defect ((dyn.step^[n]) s) ≤ dyn.defect s := by
proof body
Term-mode proof.
34 intro n
35 induction n with
36 | zero =>
37 intro s
38 simp
39 | succ n ihn =>
40 intro s
41 rw [Function.iterate_succ_apply']
42 exact le_trans (dyn.defect_nonincreasing ((dyn.step^[n]) s)) (ihn s)
43
44/-- A single 8-tick window is defect-nonincreasing. -/