ContinuousCombinerAnalysisInputs
ContinuousCombinerAnalysisInputs packages the finite-order mollifier smoothness, bootstrapped second-derivative identity, and psi-affine completion needed to derive bilinearity from a continuous Law of Logic. Researchers generalizing the Translation Theorem beyond polynomial route-independence cite this hypothesis package when applying Aczél-Kannappan classification inside Recognition Science. The declaration is a structure definition that simply records the three named inputs without any proof steps.
claimLet $C$ be a comparison operator and let $h$ witness that $C$ satisfies the continuous laws of logic (identity, non-contradiction, excluded middle, scale invariance, continuous route independence, and non-triviality). Then ContinuousCombinerAnalysisInputs$(C,h)$ holds precisely when the derived cost $G(t)=F(e^t)$ admits $C^n$ regularity for every finite $n$ via the mollifier route, the second-derivative identity $2G''(t)=ψ(G(t))G''(0)$ holds after the smoothness bootstrap, and the psi-affine completion produces a constant $c$ such that the log-bilinear identity is satisfied.
background
The GeneralizedDAlembert module carries out Move 3 of the Recognition Science program: replace the polynomial-degree-≤2 restriction on the route-independence combiner with mere continuity, using the classical Aczél–Kannappan trichotomy for continuous solutions of the d'Alembert equation. SatisfiesLawsOfLogicContinuous is the continuous analogue of the original Law of Logic structure; it keeps the four Aristotelian conditions plus scale invariance but substitutes ContinuousRouteIndependence for the polynomial version. ContinuousCombinerMollifierFiniteSmoothness asserts that the log-coordinate derived cost $G(t)=F(e^t)$ is $C^n$ for every natural number $n$. The upstream bootstrap theorem upgrades any such finite-order control to full $C^∞$ smoothness on the log-cost.
proof idea
The declaration is a structure definition with an empty proof body. It assembles the three inputs by direct field references: the mollifier finite-smoothness predicate, the continuous_combiner_log_smoothness_bootstrap theorem applied to that predicate, and the two named predicates ContinuousCombinerSecondDerivativeInput and ContinuousCombinerPsiAffineCompletion that encode the Stetkær/Aczél derivative extraction and log-bilinear conclusion.
why it matters in Recognition Science
The structure is the explicit hypothesis package required by the downstream theorems continuous_combiner_bilinear, continuous_combiner_bilinear_classification, laws_continuous_subsumes_polynomial, and RCL_is_unique_functional_form_of_logic_continuous. It marks the precise point at which the quartic-log obstruction prevents continuity alone from discharging the Translation Theorem, thereby keeping finite pairwise polynomial closure as the sharp hypothesis for the Law-of-Logic paper. The package therefore sits between the polynomial Translation Theorem in LogicAsFunctionalEquation and any future result that might close the gap.
scope and limits
- Does not prove that the three analysis inputs follow automatically from SatisfiesLawsOfLogicContinuous.
- Does not apply when the combiner fails to be continuous.
- Does not discharge the second-derivative identity; the quartic-log counterexample remains in force.
- Does not replace the classical Aczél–Kannappan classification theorem.
- Does not supply a concrete counterexample to the package itself.
formal statement (Lean)
569structure ContinuousCombinerAnalysisInputs
570 (C : ComparisonOperator)
571 (h : SatisfiesLawsOfLogicContinuous C) : Prop where
572 finite_smoothness : ContinuousCombinerMollifierFiniteSmoothness C h
573 second_derivative :
574 ContinuousCombinerSecondDerivativeInput C h
575 (continuous_combiner_log_smoothness_bootstrap C h finite_smoothness)
576 psi_affine :
577 ContinuousCombinerPsiAffineCompletion C h
578 (continuous_combiner_log_smoothness_bootstrap C h finite_smoothness)
579 second_derivative
580
581/-- **Residual input 2 assembled:** smoothness plus the derivative identity
582and ψ-affine completion give the required log-bilinear identity. -/