ContinuousCombinerAnalysisInputs
plain-language theorem explainer
ContinuousCombinerAnalysisInputs packages the finite-order mollifier smoothness on the derived cost, the second-derivative identity, and the ψ-affine completion needed to obtain the log-bilinear form from a continuous Law of Logic. Analysts extending the Translation Theorem beyond the polynomial case cite the structure when they must state the extra regularity hypotheses explicitly. The declaration is a structure definition with no proof body.
Claim. Let $C$ be a comparison operator and $h$ a witness that $C$ satisfies the continuous laws of logic. The structure asserts that the derived cost $G(t)=F(e^t)$ admits finite-order mollifier smoothness, that the second derivative satisfies the identity $2G''(t)=ψ(G(t))G''(0)$, and that the derivative identity plus symmetry yields a log-bilinear identity for some constant $c$.
background
The module GeneralizedDAlembert carries out Move 3: discharge polynomial regularity using continuity. It first proves the Aczél–Kannappan classification of continuous solutions to the d'Alembert equation inside the framework, reducing to the existing integration-bootstrap and ODE-uniqueness results. SatisfiesLawsOfLogicContinuous is the structure that replaces polynomial route-independence by continuous route-independence while retaining the four Aristotelian conditions, scale invariance, and non-triviality.
proof idea
The declaration is a structure definition that assembles three named analysis inputs; it contains no proof steps or tactics.
why it matters
It supplies the explicit hypothesis package required by continuous_combiner_bilinear, continuous_combiner_bilinear_classification, laws_continuous_subsumes_polynomial, and RCL_is_unique_functional_form_of_logic_continuous. These theorems recover the bilinear combiner and the RCL under the continuous laws once the package is supplied. The module doc-comment notes that the quartic-log obstruction shows the package is not automatic from continuity alone, so finite pairwise polynomial closure remains the sharp hypothesis for the unconditional Law-of-Logic paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.