ClosedUnderIteration
A combining rule on the reals is closed under iteration on a subset S when the rule is continuous on the product S times S and returns an element of S for every pair from S. Researchers deriving polynomial behavior from logical axioms cite this definition to encode the structural closure that follows from the four Aristotelian laws and route-independence. The definition is introduced directly as the conjunction of the continuity requirement and the algebraic closure condition.
claimLet $Phi : mathbb{R} to mathbb{R} to mathbb{R}$ be a combining rule and let $S subseteq mathbb{R}$ be a set. Then $Phi$ is closed under iteration on $S$ if $Phi$ is continuous on $S times S$ and $Phi(u,v) in S$ whenever $u,v in S$.
background
This definition appears in the PolynomialityFromLogic module, which extracts polynomial-like regularity from the logical foundations built in DAlembert.Inevitability and the Aczel theorem. The combining rule Phi is the integral operator introduced in AczelProof and AczelTheorem, where Phi(H,t) equals the integral from 0 to t of H(s) ds. The local theoretical setting is the reduction of seven independent axioms to four substantive structural conditions plus three definitional facts, as stated in the upstream PrimitiveDistinction.from theorem.
proof idea
As a definition the declaration is the direct conjunction of two properties: continuity of the uncurried Phi on the product set S times S, together with the requirement that Phi maps every pair from S back into S.
why it matters in Recognition Science
The definition supplies the closure property used by the downstream IteratedClosureOnRange declaration, which applies the same condition to the image of F on the positive reals. It records the structural consequence of the four Aristotelian laws plus route-independence and thereby prepares the regularity needed for the subsequent lemmas on continuous iteration in this module. In the broader Recognition Science development it supports the passage from logical axioms toward the phi-ladder and the eight-tick octave.
scope and limits
- Does not assert existence of any Phi satisfying the property.
- Does not derive continuity from more primitive axioms.
- Does not restrict the explicit algebraic form of Phi.
- Does not connect the set S to specific physical constants such as phi.
Lean usage
def example (F : ℝ → ℝ) (Phi : ℝ → ℝ → ℝ) : Prop := ClosedUnderIteration Phi (Set.image F (Set.Ioi 0))formal statement (Lean)
67def ClosedUnderIteration (Phi : ℝ → ℝ → ℝ) (S : Set ℝ) : Prop :=
proof body
Definition body.
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. -/