diagonal_continuous_on_range
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove joint continuity of Phi without the closure hypothesis.
- Does not extend continuity to the full real line or negative values.
- Does not imply differentiability of the diagonal map.
- Does not depend on any specific functional form of F beyond the image.
formal statement (Lean)
85theorem diagonal_continuous_on_range
86 (F : ℝ → ℝ) (Phi : ℝ → ℝ → ℝ)
87 (hClosed : IteratedClosureOnRange F Phi) :
88 ContinuousOn (fun v : ℝ => Phi v v) (Set.image F (Set.Ioi 0)) := by
proof body
Tactic-mode proof.
89 obtain ⟨hCont, _⟩ := hClosed
90 -- The diagonal map v ↦ (v, v) is continuous everywhere; compose with Phi.
91 have h_diag_on : ContinuousOn (fun w : ℝ => ((w, w) : ℝ × ℝ))
92 (Set.image F (Set.Ioi 0)) :=
93 (continuous_id.prodMk continuous_id).continuousOn
94 have h_maps : Set.MapsTo (fun w : ℝ => ((w, w) : ℝ × ℝ))
95 (Set.image F (Set.Ioi 0))
96 ((Set.image F (Set.Ioi 0)) ×ˢ (Set.image F (Set.Ioi 0))) := by
97 intro w hw
98 exact ⟨hw, hw⟩
99 -- Use ContinuousOn.comp on the explicit lambda form of uncurry.
100 have h_phi_on : ContinuousOn (fun p : ℝ × ℝ => Phi p.1 p.2)
101 ((Set.image F (Set.Ioi 0)) ×ˢ (Set.image F (Set.Ioi 0))) := hCont
102 have h_comp : ContinuousOn
103 ((fun p : ℝ × ℝ => Phi p.1 p.2) ∘ (fun w : ℝ => ((w, w) : ℝ × ℝ)))
104 (Set.image F (Set.Ioi 0)) :=
105 h_phi_on.comp h_diag_on h_maps
106 -- Convert the composition into the simpler form.
107 have h_eq : ((fun p : ℝ × ℝ => Phi p.1 p.2) ∘ (fun w : ℝ => ((w, w) : ℝ × ℝ)))
108 = (fun v : ℝ => Phi v v) := by
109 funext w
110 rfl
111 rw [h_eq] at h_comp
112 exact h_comp
113
114/-- **Iteration produces continuous orbits.** If we iterate Φ on a starting
115element v ∈ Range(F), the n-fold iterate is again in Range(F), and the map
116v ↦ Φ^[n](v, v) is continuous on Range(F). -/