laws_continuous_subsumes_polynomial
plain-language theorem explainer
Any comparison operator obeying the laws of logic under a polynomial combiner also obeys the continuous version of those laws. Under the explicit continuous-combiner analysis package the recognition composition law forces the combiner to take the bilinear form 2u + 2v + c uv. Recognition Science researchers cite the result when relaxing the polynomial-degree hypothesis to mere continuity while retaining the analysis package. The proof is a one-line application of the uniqueness theorem for continuous logic operators.
Claim. Let $C$ be a comparison operator satisfying the laws of logic. Assume the continuous-combiner analysis inputs hold for the continuous version implied by the polynomial laws. Then there exist a function $P : ℝ → ℝ → ℝ$ and constant $c$ such that for all positive $x,y$ the derived cost satisfies derived cost of $C$ at $xy$ plus derived cost of $C$ at $x/y$ equals $P$ of the two derived costs, and $P(u,v) = 2u + 2v + c uv$.
background
The module discharges polynomial regularity via continuity. It proves the Aczél–Kannappan classification of continuous solutions to the d'Alembert equation as a theorem inside the framework, reducing to the integration bootstrap and ODE uniqueness lemmas already present in Cost.FunctionalEquation. The shifted cost $H(x) = J(x) + 1$ converts the recognition composition law into the standard d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$. ContinuousCombinerAnalysisInputs is an explicit hypothesis package containing finite smoothness, second-derivative input, and psi-affine completion; the quartic-log counterexample shows these are not automatic from continuity alone.
proof idea
The proof is a one-line wrapper that applies RCL_is_unique_functional_form_of_logic_continuous to the continuous version of the laws implied by the polynomial case together with the supplied analysis inputs.
why it matters
The result shows that the polynomial case of the Translation Theorem is subsumed by the continuous version, yet the bilinear conclusion still requires the analysis package. It feeds the continuous-combiner version of SatisfiesLawsOfLogic and keeps the unconditional polynomial route in LogicAsFunctionalEquation as the sharp statement. The construction sits inside the move that replaces the polynomial-degree hypothesis with continuity while preserving the recognition composition law and the J-uniqueness fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.