continuous_combiner_psi_affine_forcing
plain-language theorem explainer
Assembling smoothness of the derived cost, the named second-derivative identity, and the ψ-affine completion hypothesis for a continuous Law of Logic yields existence of a coefficient c such that the log-bilinear identity holds. Researchers classifying continuous solutions to the d'Alembert equation inside the Recognition Science pipeline cite this step when packaging analysis inputs. The proof is a direct invocation of the ψ-affine completion hypothesis.
Claim. Let $C$ be a comparison operator satisfying the continuous laws of logic. Let $G(t) = C(e^t,1)$ be the derived cost function, assumed smooth of class $C^∞$. If the second-derivative identity $2G''(t) = ψ(G(t))G''(0)$ holds and the ψ-affine completion condition is satisfied, then there exists a real number $c$ such that $G(t+u)+G(t-u)=2G(t)+2G(u)+cG(t)G(u)$ for all real $t,u$.
background
The module develops the continuous version of the d'Alembert functional equation to relax the polynomial route-independence hypothesis in the Translation Theorem. A continuous Law of Logic is a comparison operator satisfying identity, non-contradiction, excluded middle, scale invariance, continuous route independence, and non-triviality. The derived cost is the function $G(t)=C(e^t,1)$ obtained by fixing the second argument at the multiplicative identity. The target algebraic object is the log-bilinear identity $G(t+u)+G(t-u)=2G(t)+2G(u)+cG(t)G(u)$. Upstream, the Aczél–Kannappan classification states that a continuous solution $H$ to the d'Alembert equation with $H(0)=1$ is constant 1, a hyperbolic cosine, or a trigonometric cosine.
proof idea
This is a one-line wrapper that applies the ContinuousCombinerPsiAffineCompletion hypothesis directly; the hypothesis is defined to assert precisely the existence of the required coefficient $c$ for the log-bilinear identity.
why it matters
The declaration completes the explicit analysis package that turns smoothness plus derivative identity plus ψ-affine completion into bilinearity. It feeds the continuous-combiner bilinear classification theorem, which is the hypothesis-package form of the final bilinear conclusion. The step supports the module goal of replacing the polynomial-degree-≤-2 restriction with continuity via the Aczél–Kannappan trichotomy, while recording that the second-derivative input is not automatic from continuity alone (quartic log-cost obstruction). It touches the open question whether continuity alone closes the full Law of Logic pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.