IndisputableMonolith.Foundation.PolynomialityFromLogic
This module defines closed-under-iteration for combining rules on real subsets to support derivations of polynomiality from logical consistency in Recognition Science. Researchers tracing the J-cost functional back to multiplicative closure would cite it. The module imports d'Alembert inevitability and Aczel smoothness, then introduces the core definition plus auxiliary continuity statements on ranges and diagonals.
claimA combining rule $Φ$ is closed under iteration on a set $S ⊆ ℝ$ when $Φ(x,y) ∈ S$ for all $x,y ∈ S$ and $Φ$ is continuous in both arguments jointly.
background
The module sits in the Foundation layer and imports the d'Alembert inevitability result, which shows that any cost functional obeying multiplicative consistency must satisfy the equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ with $H(0)=1$. It further imports the Aczel theorem, which classifies all continuous solutions of that equation as the constant function 1 or $H(t) = cosh(λ t)$. The central definition supplied here is that of a combining rule being closed under iteration on a subset of the reals, requiring both set closure and joint continuity.
proof idea
This is a definition module. It imports the two upstream modules on d'Alembert inevitability and Aczel smoothness, then declares ClosedUnderIteration together with IteratedClosureOnRange and the two continuity lemmas diagonal_continuous_on_range and iterate_continuous_on_range.
why it matters in Recognition Science
The module supplies the closure and continuity notions required for later steps that extract polynomial structure from logical consistency. It therefore supports the forcing chain from T0 through the J-uniqueness step and the emergence of the phi-ladder. No downstream theorems are recorded yet, so the module currently functions as an interface definition awaiting use in polynomiality derivations.
scope and limits
- Does not classify combining rules outside the continuous d'Alembert solutions.
- Does not treat discontinuous or non-real-valued cases.
- Does not produce explicit polynomial expressions for the cost functional.
- Does not address vector-valued or higher-dimensional extensions.