iterate
plain-language theorem explainer
The definition supplies a compatibility shim that reexports the n-fold iteration of a map f on an element a via Mathlib's Nat.iterate. It is cited by successor constructions on LogicNat, continuity proofs for iterated orbits on ranges, and tick equivalences realizing time as an orbit. The implementation is a direct one-line alias to the canonical primitive.
Claim. For a map $f: X → X$, natural number $n$, and point $a ∈ X$, the n-fold iterate is $f^{[n]}(a)$ where $f^{[n]}$ denotes n-fold composition.
background
The module supplies a thin compatibility shim. Mathlib now exposes iteration via Nat.iterate (notation f^[n]), while older code in the repository expected Function.iterate. The shim lets the rest of the library compile unchanged without altering any downstream proofs.
proof idea
One-line wrapper that applies Nat.iterate.
why it matters
It underpins the successor definition in ArithmeticFromLogic and the iteration theorems in PolynomialityFromLogic and TimeAsOrbit. These feed the tick equivalence that realizes time as an orbit under the successor map, supporting the eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.