IndisputableMonolith.Compat.FunctionIterate
The module supplies a compatibility definition for iterating a function f exactly n times starting from a. It is imported by the central Compat module to standardize shims across the Recognition Science project. The file contains only this definition and no theorems.
claimFor a map $f : X → X$ and point $a ∈ X$, the n-fold iterate is the result of applying $f$ to $a$ exactly n times.
background
This module belongs to the Compat domain and imports only Mathlib. It introduces the iterate definition to handle repeated function application uniformly. The local setting is a thin compatibility layer whose sole purpose is to expose this operation to the rest of the project.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The iterate definition is consumed by the central compatibility imports in IndisputableMonolith.Compat. It therefore supplies the function-iteration shim required by any downstream module that needs consistent n-step iteration.
scope and limits
- Does not contain theorems or proofs.
- Does not depend on any Recognition Science modules.
- Does not introduce constants or additional shims.