IndisputableMonolith.Compat.FunctionIterate
This module supplies a compatibility definition for iterating a function f exactly n steps from initial value a. It is imported by the central Compat module so that downstream code can rely on a uniform iteration primitive. The module contains only the definition and imports Mathlib; no proofs are present.
claimThe principal object is the function $\mathrm{iterate}(f,n,a)$ that returns the result of applying $f$ exactly $n$ times to $a$.
background
The module sits in the Compat domain and imports only Mathlib. Its single definition, iterate, encodes the standard n-fold composition of a map on a type. This shim ensures that repeated function application is available uniformly when other modules construct objects such as forcing chains or phi-ladder steps.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module is imported by IndisputableMonolith.Compat, described as the central compatibility layer that downstream modules use to obtain shims and project-wide constants. It therefore supplies the iterate primitive required by any construction that needs controlled iteration.
scope and limits
- Does not contain any theorems or proofs.
- Does not introduce Recognition Science constants or J-cost definitions.
- Does not depend on any sibling modules inside the project.