Encyclopedia Foundation Foundation Polynomiality From Logic Iterated Closure On Range

ARTICLE 4 claims 2 theorems 2 models

Foundation Polynomiality From Logic Iterated Closure On Range

A technical condition called closure under iteration guarantees that repeatedly combining values never leaves the original set, and that the process behaves continuously.

Verify this page

Closure under iteration

In mathematics, a set is closed under an operation if applying that operation to members of the set always produces another member of the set. For example, the natural numbers are closed under addition because adding two natural numbers always gives a natural number. The Recognition Science framework applies this idea to a function F that maps positive real numbers to real numbers. The set of interest is the range of F, meaning all values F actually produces. The combining rule Phi takes two such values and produces a new one. The declaration IteratedClosureOnRange states that Phi is closed under iteration on this range: applying Phi to any two values in the range always yields another value in the range, and Phi is continuous in both inputs.

This closure condition has two proved consequences. First, the diagonal of Phi on the range is continuous: the function that sends v to Phi(v, v) is continuous on the range of F. Second, iteration produces continuous orbits: for any natural number n, the n-fold iterate of Phi on a starting value v in the range is again in the range, and the map v to that iterate is continuous on the range. Both results are fully proved in the machine-checked library of formal theorems. They form the structural content of the idea that comparisons of comparisons compose consistently.

The declaration does not claim that closure under iteration forces the combining rule Phi to be real-analytic. An earlier version of the module carried that assumption, but a counterexample showed it false in general. The quartic-log combiner Phi(a,b) = 2a + 2b + 12 sqrt(a*b) is closed on [0, infinity) but is not real-analytic at the origin. The corrected module keeps only the structural consequences that are actually proved: diagonal continuity and continuous iterates on the range.

In Recognition Science, this closure property is a bridge from logical consistency to mathematical regularity. The framework models comparisons as a ledger of recognition events, where each comparison combines two prior comparisons. Closure under iteration guarantees that this process never escapes the set of possible comparison values, and that small changes in inputs produce small changes in outputs. The proved consequences give the framework a foothold for further analysis, while the counterexample marks a clear boundary: closure alone does not imply analyticity.

MODEL IteratedClosureOnRange · IndisputableMonolith/Foundation/PolynomialityFromLogic.lean
IteratedClosureOnRange · IndisputableMonolith/Foundation/PolynomialityFromLogic.lean:71 
/-- The structural closure property derived from the four Aristotelian
laws plus the route-independence equation: the combining rule on
`Range(F)` is closed under iteration in this technical sense. -/
def IteratedClosureOnRange (F : ℝ → ℝ) (Phi : ℝ → ℝ → ℝ) : Prop :=
  ClosedUnderIteration Phi (Set.image F (Set.Ioi 0))
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 force the combining rule Phi to be real-analytic, as the quartic-log counterexample shows. The declaration does not establish that F itself is continuous or analytic; it only concerns the range of F and the combining rule Phi. The two proved consequences do not imply that the combining rule is polynomial or has any specific algebraic form.

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