ContinuousCombinerAnalysisInputs
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.