Encyclopedia Foundation Foundation Polynomiality From Logic Closed Under Iteration

ARTICLE 4 claims 2 theorems 2 models

Foundation Polynomiality From Logic Closed Under Iteration

A precise condition on how comparisons of comparisons combine, and the two continuity facts it guarantees.

Verify this page

Closure under iteration

In mathematics, a set is closed under an operation when applying that operation to elements of the set always yields another element of the set. The positive integers are closed under addition, for instance, because adding two positive integers always gives a positive integer. The Recognition Science framework applies this classical idea to a combining rule, a function that takes two real numbers and produces a third. The declaration ClosedUnderIteration states that a combining rule Φ is closed under iteration on a set S when two conditions hold: applying Φ to any two elements of S produces an element of S, and Φ is continuous in both inputs on S.

The framework's interest lies in a specific set: the range of a function F on positive inputs. The definition IteratedClosureOnRange packages this as the claim that Φ is closed under iteration on the image of F over positive reals. The docstring frames this as the formal content of "comparisons of comparisons compose consistently": any finite iteration of the combining rule on elements of the range again lands in the range, and the iteration depends continuously on its starting inputs.

Two theorems are fully proved from this closure condition. The first, diagonal_continuous_on_range, shows that the diagonal of Φ, the map v ↦ Φ(v, v), is continuous on the range of F. This is a direct consequence of the joint continuity of Φ on the range squared. The second, iterate_continuous_on_range, shows that iterating Φ on a starting element produces continuous orbits: for any natural number n, there exists a continuous function φₙ on the range such that φₙ(v) lies in the range for every v in the range.

In Recognition Science, these two results are the structural consequences of closure under iteration that the framework's library actually proves. They establish that the combining rule behaves continuously under iteration on the range, a regularity property that the framework uses in further arguments.

What the declaration does not claim is as important as what it does. The framework's corrected status statement explicitly retracts an earlier, stronger claim: that closure under iteration on the range forces the combining rule to be real-analytic. A counterexample in the framework's own library, the quartic-log combiner Φ(a,b) = 2a + 2b + 12√(ab), is closed on [0,∞) but is not real-analytic at the origin. The polynomiality problem, proving that the combiner has degree at most two, is therefore moved to a planned module that assumes real-analyticity at the origin directly.

MODEL ClosedUnderIteration · IndisputableMonolith/Foundation/PolynomialityFromLogic.lean
ClosedUnderIteration · IndisputableMonolith/Foundation/PolynomialityFromLogic.lean:64 
/-- A combining rule Φ is **closed under iteration** on a set `S ⊆ ℝ` if
applying Φ to two elements of S produces an element of S, and the result is
continuous in both inputs. -/
def ClosedUnderIteration (Phi : ℝ → ℝ → ℝ) (S : Set ℝ) : Prop :=
  ContinuousOn (Function.uncurry Phi) (S ×ˢ S) ∧
  ∀ u v : ℝ, u ∈ S → v ∈ S → Phi u v ∈ S
THEOREM diagonal_continuous_on_range · IndisputableMonolith/Foundation/PolynomialityFromLogic.lean
diagonal_continuous_on_range · IndisputableMonolith/Foundation/PolynomialityFromLogic.lean:83 
/-- **The diagonal of Φ on Range(F) is continuous.**  Pure consequence of
joint continuity of Φ on Range(F)². -/
theorem diagonal_continuous_on_range
    (F : ℝ → ℝ) (Phi : ℝ → ℝ → ℝ)
    (hClosed : IteratedClosureOnRange F Phi) :
    ContinuousOn (fun v : ℝ => Phi v v) (Set.image F (Set.Ioi 0)) := by
  obtain ⟨hCont, _⟩ := hClosed
  -- The diagonal map v ↦ (v, v) is continuous everywhere; compose with Phi.
  have h_diag_on : ContinuousOn (fun w : ℝ => ((w, w) : ℝ × ℝ))
      (Set.image F (Set.Ioi 0)) :=
    (continuous_id.prodMk continuous_id).continuousOn
  have h_maps : Set.MapsTo (fun w : ℝ => ((w, w) : ℝ × ℝ))
      (Set.image F (Set.Ioi 0))
      ((Set.image F (Set.Ioi 0)) ×ˢ (Set.image F (Set.Ioi 0))) := by
    intro w hw
    exact ⟨hw, hw⟩
  -- Use ContinuousOn.comp on the explicit lambda form of uncurry.
  have h_phi_on : ContinuousOn (fun p : ℝ × ℝ => Phi p.1 p.2)
      ((Set.image F (Set.Ioi 0)) ×ˢ (Set.image F (Set.Ioi 0))) := hCont
  have h_comp : ContinuousOn
      ((fun p : ℝ × ℝ => Phi p.1 p.2) ∘ (fun w : ℝ => ((w, w) : ℝ × ℝ)))
      (Set.image F (Set.Ioi 0)) :=
    h_phi_on.comp h_diag_on h_maps
  -- Convert the composition into the simpler form.
  have h_eq : ((fun p : ℝ × ℝ => Phi p.1 p.2) ∘ (fun w : ℝ => ((w, w) : ℝ × ℝ)))
              = (fun v : ℝ => Phi v v) := by
    funext w
    rfl
  rw [h_eq] at h_comp
  exact h_comp
THEOREM iterate_continuous_on_range · IndisputableMonolith/Foundation/PolynomialityFromLogic.lean
iterate_continuous_on_range · IndisputableMonolith/Foundation/PolynomialityFromLogic.lean:114 
/-- **Iteration produces continuous orbits.**  If we iterate Φ on a starting
element v ∈ Range(F), the n-fold iterate is again in Range(F), and the map
v ↦ Φ^[n](v, v) is continuous on Range(F). -/
theorem iterate_continuous_on_range
    (F : ℝ → ℝ) (Phi : ℝ → ℝ → ℝ)
    (hClosed : IteratedClosureOnRange F Phi)
    (n : ℕ) :
    ∃ φₙ : ℝ → ℝ,
      ContinuousOn φₙ (Set.image F (Set.Ioi 0)) ∧
      (∀ v ∈ Set.image F (Set.Ioi 0), φₙ v ∈ Set.image F (Set.Ioi 0)) := by
  -- Define the iterate by recursion on n.  Inductively, each iterate is
  -- a continuous map from Range(F) into Range(F).
  induction n with
  | zero =>
    refine ⟨id, ?_, ?_⟩
    · exact continuousOn_id
    · intro v hv
      exact hv
  | succ k ih =>
    obtain ⟨φₖ, hCont_φₖ, hMap_φₖ⟩ := ih
    refine ⟨fun v => Phi (φₖ v) v, ?_, ?_⟩
    · -- Continuity of v ↦ Phi(φₖ v, v) via ContinuousOn.comp.
      obtain ⟨hCont_Phi, _⟩ := hClosed
      have h_pair_on : ContinuousOn (fun w : ℝ => ((φₖ w, w) : ℝ × ℝ))
          (Set.image F (Set.Ioi 0)) :=
        hCont_φₖ.prodMk continuousOn_id
      have h_maps : Set.MapsTo (fun w : ℝ => ((φₖ w, w) : ℝ × ℝ))
          (Set.image F (Set.Ioi 0))
          ((Set.image F (Set.Ioi 0)) ×ˢ (Set.image F (Set.Ioi 0))) := by
        intro w hw
        exact ⟨hMap_φₖ w hw, hw⟩
      have h_phi_on : ContinuousOn (fun p : ℝ × ℝ => Phi p.1 p.2)
          ((Set.image F (Set.Ioi 0)) ×ˢ (Set.image F (Set.Ioi 0))) := hCont_Phi
      have h_comp : ContinuousOn
          ((fun p : ℝ × ℝ => Phi p.1 p.2) ∘
            (fun w : ℝ => ((φₖ w, w) : ℝ × ℝ)))
          (Set.image F (Set.Ioi 0)) :=
        h_phi_on.comp h_pair_on h_maps
      have h_eq : ((fun p : ℝ × ℝ => Phi p.1 p.2) ∘
                    (fun w : ℝ => ((φₖ w, w) : ℝ × ℝ)))
                  = (fun v : ℝ => Phi (φₖ v) v) := by
        funext w
        rfl
      rw [h_eq] at h_comp
      exact h_comp
    · intro v hv
      obtain ⟨_, hClosure⟩ := hClosed
      exact hClosure (φₖ v) v (hMap_φₖ v hv) hv

What this page does not claim

Closure under iteration does not imply real-analyticity of the combining rule, as the quartic-log counterexample shows. The continuity results do not establish the full polynomiality conjecture, which remains a target for a future module.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PolynomialityFromLogic.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND