  64/-- A combining rule Φ is **closed under iteration** on a set `S ⊆ ℝ` if
  65applying Φ to two elements of S produces an element of S, and the result is
  66continuous in both inputs. -/
  67def ClosedUnderIteration (Phi : ℝ → ℝ → ℝ) (S : Set ℝ) : Prop :=
  68  ContinuousOn (Function.uncurry Phi) (S ×ˢ S) ∧
  69  ∀ u v : ℝ, u ∈ S → v ∈ S → Phi u v ∈ S
  70
  71/-- The structural closure property derived from the four Aristotelian
  72laws plus the route-independence equation: the combining rule on
  73`Range(F)` is closed under iteration in this technical sense. -/
  74def IteratedClosureOnRange (F : ℝ → ℝ) (Phi : ℝ → ℝ → ℝ) : Prop :=
  75  ClosedUnderIteration Phi (Set.image F (Set.Ioi 0))
  76
  77/-! ## Provable Consequences
  78
  79The next two lemmas extract regularity properties from closure-under-iteration
  80that are used in the conjecture's proof.  Both are fully proved here.
  81-/
  82
  83/-- **The diagonal of Φ on Range(F) is continuous.**  Pure consequence of
  84joint continuity of Φ on Range(F)². -/
  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
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.