iterate
plain-language theorem explainer
The iterate definition supplies a compatibility shim that applies a function f repeatedly n times to an initial value a. It is cited by constructions of successor functions on LogicNat, continuous iteration orbits on ranges, and tick equivalences to natural numbers in the Recognition Science monolith. The implementation is a direct one-line alias to the Mathlib primitive Nat.iterate.
Claim. Define the n-fold iteration of a map $f : α → α$ applied to a starting point $a$ by iterate$(f, n, a) :=$ Nat.iterate$(f, n, a)$.
background
This module supplies a compatibility layer because Mathlib versions differ on whether Function.iterate exists; older code in the monolith historically used that name. The local setting is therefore a thin shim that delegates to the current canonical API Nat.iterate (or the notation $f^[n]$) so that downstream files continue to compile unchanged. No upstream lemmas are required; the definition stands alone as a compatibility bridge.
proof idea
The definition is a one-line wrapper that directly invokes Nat.iterate f n a.
why it matters
This definition supports the successor operation on LogicNat, the Tick ≃ LogicNat equivalence, and theorems establishing continuity of n-fold iterates on Range(F). It underpins the inductive structure that turns Peano axioms into theorems and enables the time-as-orbit construction used for the eight-tick octave. It touches the maintenance question of keeping the monolith stable across Mathlib updates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.