diagonal_continuous_on_range
plain-language theorem explainer
The diagonal restriction of the combining map Phi is continuous on the positive image of F under the iterated closure hypothesis. Researchers establishing regularity of iterated orbits in Recognition Science cite this result when building smoothness properties from logical closure. The proof extracts joint continuity of Phi from the closure predicate and composes it with the continuous diagonal embedding via ContinuousOn.comp.
Claim. Let $F : ℝ → ℝ$ and $Φ : ℝ → ℝ → ℝ$. If $Φ$ is closed under iteration on the image of $F$ over $(0, ∞)$, then the map $v ↦ Φ(v, v)$ is continuous on that image.
background
The PolynomialityFromLogic module extracts regularity from iteration closure derived from Aristotelian laws and route-independence. IteratedClosureOnRange F Phi is defined to be ClosedUnderIteration Phi (Set.image F (Set.Ioi 0)), which encodes that the combining rule on the range is closed under iteration and therefore jointly continuous on the product of the range with itself. Upstream results supply the algebraic composition of J-automorphisms and the compatibility definition of function iteration that underwrite this extraction.
proof idea
Obtain the joint continuity component hCont of Phi on the product set directly from the closure hypothesis. Verify that the diagonal map w ↦ (w, w) is continuous on the image and maps the image into the product set. Apply ContinuousOn.comp to compose Phi with the diagonal, then rewrite the resulting expression to the target diagonal lambda.
why it matters
This lemma supplies one of the two regularity properties extracted from closure-under-iteration and used in the module conjecture proof. It guarantees continuity of the diagonal of Phi, which supports claims that iteration produces continuous orbits on the range. In the Recognition Science framework the result aligns with the self-similar fixed point phi and the steps of the forcing chain that produce the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.