IteratedClosureOnRange
plain-language theorem explainer
The definition asserts that the image of F over positive reals satisfies closure under iteration of the binary combining operation Phi. Workers on the polynomiality conjecture from logical axioms reference this property when extracting regularity for downstream continuity statements. It is realized as a direct abbreviation of the ClosedUnderIteration predicate applied to that image set.
Claim. For a map $F:ℝ→ℝ$ and binary operation $Φ:ℝ×ℝ→ℝ$, the iterated closure property on the range holds when the set $F((0,∞))$ is invariant under iterated applications of $Φ$.
background
This definition appears in the PolynomialityFromLogic module, which extracts polynomial features from the four Aristotelian laws together with the route-independence equation. ClosedUnderIteration Phi S requires that repeated applications of Phi to pairs drawn from S remain inside S, supplying the joint continuity data needed for diagonal and orbit maps. It rests on the J-cost structure from PhiForcingDerived and the positive-reals ledger from DAlembert.LedgerFactorization, both of which calibrate the domain and the operation Phi.
proof idea
The definition is a one-line wrapper that applies ClosedUnderIteration directly to Phi and the image of F on the positive reals.
why it matters
It supplies the hypothesis for the two immediate downstream theorems that prove continuity of the diagonal map and of n-fold iterates on the range. Those continuity statements are invoked in the module's main conjecture proof. In the Recognition framework the closure encodes the logical axioms into the regularity required for the phi-ladder and the T5–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.