Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PolynomialityFromLogic

show as:
view Lean formalization →

Sets up closure-under-iteration for a binary combining rule on a real set, with joint continuity of the result. Bridges the d'Alembert inevitability of the cost functional to Aczél smoothness, so iterated combinations stay inside a continuous family. Analysts tracking how logical consistency forces polynomial (or hyperbolic) cost structure would cite it. The module is definitional scaffolding plus continuity lemmas on ranges, not a single end theorem.

claimA combining rule $\Phi:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ is closed under iteration on $S\subseteq\mathbb{R}$ when $x,y\in S$ implies $\Phi(x,y)\in S$ and $(x,y)\mapsto\Phi(x,y)$ is continuous on $S\times S$. The module records iterated closure on the range, and continuity of the diagonal and of iterates, as the bridge from multiplicative cost consistency to smooth d'Alembert solutions.

background

Recognition Science forces the cost functional from multiplicative consistency rather than by ansatz. The upstream d'Alembert inevitability module shows that any cost $F:\mathbb{R}_+\to\mathbb{R}$ with the right composition law must satisfy a d'Alembert equation: the unique form compatible with multiplicative consistency of the cost.

Aczél's classical classification then applies: every continuous solution of $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ is $C^\infty$, and is either $H\equiv 1$ or $H(t)=\cosh(\lambda t)$. That smoothness is what upgrades algebraic consistency to a polynomial (or hyperbolic) cost shape on the recognition ladder.

This module sits between those two layers. It isolates the set-theoretic and topological bookkeeping: a combining rule must map a working set into itself and stay continuous under iteration, so the range remains a legitimate domain for the Aczél argument.

proof idea

Definition module with supporting continuity lemmas, not a single monolithic proof. It introduces closed-under-iteration for a combining rule $\Phi$ on $S$, then packages iterated closure on the range and continuity of the diagonal map and of iterates. Those facts are the hypotheses one feeds into the Aczél smoothness pipeline once d'Alembert form is already forced. No deep new analysis lives here; the work is interface hygiene between inevitability and smoothness.

why it matters in Recognition Science

Without iterated closure and continuity on the range, the jump from "d'Alembert is inevitable" to "solutions are $C^\infty$ and classified" is formally incomplete: one must know that repeated combinations stay inside a set where continuity hypotheses apply. The module therefore glues Foundation.DAlembert.Inevitability to Cost.AczelTheorem.

In the broader forcing chain this supports the path to the unique J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) and the Recognition Composition Law, which sit at T5 of the unified forcing chain. No downstream consumers are wired in the graph yet; the module is infrastructure for that classification step rather than a leaf theorem.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (4)