IteratedClosureOnRange
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not specify the algebraic form of the operation Phi.
- Does not itself prove continuity or any metric properties.
- Does not extend the domain beyond the positive reals.
- Does not address physical calibration or numerical constants.
formal statement (Lean)
74def IteratedClosureOnRange (F : ℝ → ℝ) (Phi : ℝ → ℝ → ℝ) : Prop :=
proof body
Definition body.
75 ClosedUnderIteration Phi (Set.image F (Set.Ioi 0))
76
77/-! ## Provable Consequences
78
79The next two lemmas extract regularity properties from closure-under-iteration
80that are used in the conjecture's proof. Both are fully proved here.
81-/
82
83/-- **The diagonal of Φ on Range(F) is continuous.** Pure consequence of
84joint continuity of Φ on Range(F)². -/