continuous_combiner_bilinear_classification
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
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the analysis inputs package from SatisfiesLawsOfLogicContinuous alone.
- Does not apply to operators lacking continuous route independence.
- Does not remove the need for the explicit second-derivative and psi-affine hypotheses.
- Does not address the quartic-log counterexample that blocks automatic bilinearity.
formal statement (Lean)
598theorem continuous_combiner_bilinear_classification
599 (C : ComparisonOperator)
600 (h : SatisfiesLawsOfLogicContinuous C)
601 (hInputs : ContinuousCombinerAnalysisInputs C h) :
602 ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
603 (∀ x y : ℝ, 0 < x → 0 < y →
604 derivedCost C (x * y) + derivedCost C (x / y)
605 = P (derivedCost C x) (derivedCost C y)) ∧
606 (∀ u v, P u v = 2*u + 2*v + c*u*v) := by
proof body
Term-mode proof.
607 have hSmooth := continuous_combiner_log_smoothness_bootstrap C h hInputs.finite_smoothness
608 have hLog := continuous_combiner_psi_affine_forcing C h hSmooth
609 hInputs.second_derivative hInputs.psi_affine
610 exact log_bilinear_positive_cost_bilinear (derivedCost C) hLog
611
612/-- **Continuous-combiner Translation Theorem, hypothesis-package form**: a continuous comparison
613operator satisfying the four Aristotelian conditions plus scale
614invariance and continuous route independence admits a *bilinear*
615combiner `P(u,v) = 2u + 2v + c·u·v` if the explicit analysis package is
616also supplied. Polynomial-degree-≤-2 is not dropped by continuity alone. -/