IndisputableMonolith.Compat.FunctionIterate
Compatibility shim defining n-fold iteration of a function f starting from a value a. Downstream RS modules import it via the central Compat barrel rather than depending on a particular Mathlib iterate API. The module is pure definitional packaging with no theorems.
claimFor a type $\alpha$, a map $f : \alpha \to \alpha$, a start value $a \in \alpha$, and $n \in \mathbb{N}$, the iterate $f^{[n]}(a)$ is the value obtained by applying $f$ exactly $n$ times to $a$ (with $f^{[0]}(a) = a$).
background
Recognition Science Lean code sits on Mathlib but pins a few names so that physics modules do not break when Mathlib moves iterate helpers. This file is one such pin: a single compatibility definition of function iteration.
Iteration appears wherever discrete dynamics or rung-stepping on the $\varphi$-ladder is written as repeated application of a self-map. The module itself does not encode RS physics; it only standardizes the notation $f$ applied $n$ times from $a$.
The parent barrel IndisputableMonolith.Compat re-exports this shim so that "import Compat" pulls project-wide constants and compatibility definitions in one place.
proof idea
This is a definition module, no proofs. It exposes a named iterate binding (compatibility wrapper around the Mathlib-style n-fold application of f to a) and stops there.
why it matters in Recognition Science
Feeds the central Compat import surface used across the monolith. Any later lemma that steps a discrete dynamical system, an eight-tick schedule, or a ladder map by repeated application can cite this name without forking Mathlib APIs. It is infrastructure, not a forcing-chain step (T0–T8); its value is stable naming for downstream physics modules that import Compat.
scope and limits
- Does not prove uniqueness or equational laws for iteration.
- Does not define continuous flows or real-time dynamics.
- Does not encode RS mass, J-cost, or forcing-chain content.
- Does not fix a particular Mathlib version beyond the local shim.