continuous_combiner_bilinear_classification
plain-language theorem explainer
A continuous comparison operator C obeying the four Aristotelian laws plus scale invariance and continuous route independence yields a bilinear combiner P(u,v) = 2u + 2v + c uv on derived costs, provided an explicit analysis package supplies finite mollifier smoothness, a second-derivative identity, and psi-affine completion. Recognition Science authors extending the Translation Theorem to the continuous setting cite this result when the polynomial-degree hypothesis is replaced by continuity. The proof is a three-step term chain that bootstraps
Claim. Let $C$ be a comparison operator satisfying the continuous laws of logic (identity, non-contradiction, excluded middle, scale invariance, and continuous route independence). Suppose the analysis inputs package is given, consisting of finite-order mollifier derivative control, a second-derivative identity on the log-cost, and psi-affine completion. Then there exist a function $P:ℝ→ℝ→ℝ$ and a constant $c$ such that for all positive $x,y$, $F(xy)+F(x/y)=P(F(x),F(y))$ where $F$ is the derived cost of $C$, and moreover $P(u,v)=2u+2v+cuv$.
background
SatisfiesLawsOfLogicContinuous is the structure that replaces the polynomial route-independence hypothesis of the original SatisfiesLawsOfLogic with ContinuousRouteIndependence while retaining the four Aristotelian conditions and scale invariance. ContinuousCombinerAnalysisInputs is an explicit hypothesis package containing three items: finite smoothness via mollifiers, a second-derivative identity, and psi-affine completion; the module doc notes that the quartic-log counterexample shows this package is not automatic from continuity alone. The local setting is the GeneralizedDAlembert module, whose goal is to discharge the polynomial-degree-≤2 restriction on the combiner by invoking the Aczél–Kannappan classification of continuous solutions to the d'Alembert equation. Upstream lemmas include continuous_combiner_log_smoothness_bootstrap, which upgrades finite mollifier control to $C^∞$ smoothness of the log-cost, and continuous_combiner_psi_affine_forcing, which assembles the log-bilinear identity from smoothness plus the derivative and affine inputs.
proof idea
The term proof first invokes continuous_combiner_log_smoothness_bootstrap on the finite-smoothness field of hInputs to obtain $C^∞$ smoothness of the log-cost. It then feeds that smoothness together with the second-derivative and psi-affine fields into continuous_combiner_psi_affine_forcing to produce the log-bilinear identity. Finally it applies log_bilinear_positive_cost_bilinear to lift the log identity back to the required bilinear combiner on positive ratios.
why it matters
This theorem supplies the final algebraic step that converts the continuous-combiner hypothesis package into the bilinear conclusion; it is invoked by the main continuous_combiner_bilinear theorem and by laws_continuous_subsumes_polynomial. The module doc positions it inside Move 3 of the Recognition framework, where continuity plus the Aczél–Kannappan trichotomy (constant, cosh, cos) replaces the earlier polynomial restriction on the route-independence combiner. It touches the open question whether the analysis package can be derived from continuity alone; the quartic-log obstruction shows it cannot, so finite pairwise polynomial closure remains the sharp unconditional route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.