ClosedUnderIteration
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.