iterate_continuous_on_range
plain-language theorem explainer
Iteration of the combining rule Φ on the positive range of F produces a continuous self-map of that range for any finite number of steps. Workers on the Recognition Science foundation would reference this when deriving regularity from the closure property that follows from the Aristotelian laws and route-independence. The proof is by induction on the iteration depth: the zero case is the identity, and each successor step composes the prior continuous iterate with Φ using product continuity and the given closure to preserve the range.
Claim. Let $F : ℝ → ℝ$ and $Φ : ℝ → ℝ → ℝ$. Suppose $Φ$ satisfies the iterated closure property on the image $R = F((0,∞))$, meaning repeated application of $Φ$ to pairs from $R$ remains in $R$. Then for every natural number $n$ there exists a function $φ_n : R → R$ that is continuous on $R$ and represents the $n$-fold iteration of $Φ$ starting from elements of $R$.
background
The declaration lives in the PolynomialityFromLogic module, which extracts structural consequences of closure under iteration on the range of F. The key hypothesis is IteratedClosureOnRange F Phi, defined as ClosedUnderIteration Phi (Set.image F (Set.Ioi 0)), which encodes that the combining rule on Range(F) is closed under iteration. This follows from the four Aristotelian laws plus the route-independence equation in the broader foundation. The module corrects an earlier claim by dropping analyticity and retaining only continuity of iterates and the diagonal.
proof idea
The proof proceeds by induction on n. For n = 0, the identity map is continuous on the image and maps it to itself. For the successor case, given a continuous φ_k that maps the image to itself, the next map is defined as v ↦ Phi(φ_k v, v). Continuity follows from the continuity of Phi on the product of the image with itself (from the closure hypothesis), the product of the continuous φ_k with the identity, and composition of continuous maps on the appropriate sets. The range preservation uses the closure property directly on the pair (φ_k v, v).
why it matters
This result supplies the continuous iterates needed for further analysis of the functional equation in the Recognition framework, particularly in establishing regularity properties that precede polynomiality considerations. It forms part of the corrected module that retains only the provable structural consequences after the quartic-log counterexample ruled out general analyticity. While not directly tied to the T0-T8 chain, it supports the derivation of continuous orbits from the J-uniqueness and self-similar fixed point in the foundation. The module comment indicates the polynomiality problem is deferred to a future module assuming analyticity at the origin.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.