iterate
The iterate definition supplies a compatibility shim that computes the n-fold application of a map f to a starting point a. Downstream modules for arithmetic, continuous orbits, and time ticks rely on it to avoid Mathlib version conflicts. It is implemented as a direct alias to Nat.iterate.
claimThe n-fold iteration of a function $f : α → α$ applied to an initial value $a ∈ α$, denoted $f^{[n]}(a)$.
background
This module addresses version differences in Mathlib regarding function iteration. Older code expected Function.iterate while current Mathlib supplies Nat.iterate and the notation f^[n]. The definition ensures seamless compatibility for the rest of the library.
proof idea
One-line wrapper that applies Nat.iterate f n a.
why it matters in Recognition Science
It underpins succ in ArithmeticFromLogic, the continuous-orbit theorems in PolynomialityFromLogic, and the tick equivalences in TimeAsOrbit. The shim preserves the iteration machinery used throughout the Recognition Science forcing chain, including the eight-tick octave.
scope and limits
- Does not introduce new iteration semantics beyond the Mathlib standard.
- Does not handle non-natural iteration counts.
- Does not prove any continuity or algebraic properties; those live in the using modules.
Lean usage
iterate Nat.succ 3 0formal statement (Lean)
19def iterate (f : α → α) (n : Nat) (a : α) : α :=
proof body
Definition body.
20 Nat.iterate f n a
21
22end Function