ContinuousCombinerPsiAffineCompletion
plain-language theorem explainer
Researchers replacing the polynomial restriction in the Translation Theorem with continuity cite this definition as the ψ-affine completion step. It states that for any comparison operator obeying the continuous laws of logic, if the associated log-cost is smooth and satisfies the second-derivative identity, then the log-cost obeys the bilinear identity for some coefficient c. The definition simply packages the existence statement extracted from the Aczél equation under those hypotheses.
Claim. Let $C$ be a comparison operator satisfying the continuous laws of logic. Let $G(t)$ be the derived cost of $C$ evaluated at $e^t$. Assume $G$ is infinitely differentiable and satisfies the second-derivative identity: there exists a function $ψ$ such that $2G''(t) = ψ(G(t)) · G''(0)$ for all real $t$. Then there exists a real number $c$ such that $G(t+u) + G(t-u) = 2G(t) + 2G(u) + c · G(t) · G(u)$ for all real $t,u$.
background
The GeneralizedDAlembert module replaces the polynomial-degree restriction on route-independence with mere continuity by invoking the Aczél–Kannappan classification of continuous d'Alembert solutions. A continuous Law of Logic is the structure SatisfiesLawsOfLogicContinuous, which augments the standard axioms (identity, non-contradiction, excluded middle, scale invariance, non-triviality) with continuous route independence instead of the polynomial version. The derived cost is the function obtained by fixing one argument of the comparison operator at the multiplicative identity and passing to logarithmic coordinates.
proof idea
This definition is a one-line wrapper that directly states the existence of a real coefficient $c$ making the log-bilinear identity hold for the derived cost function, given the supplied smoothness and second-derivative hypotheses. No additional lemmas or tactics are invoked inside the definition; it serves purely as a named Prop packaging the algebraic target.
why it matters
This definition supplies the final analysis input that forces bilinearity from a continuous combiner, feeding directly into the structure ContinuousCombinerAnalysisInputs and the theorem continuous_combiner_psi_affine_forcing. It addresses the gap exposed by the quartic-log obstruction, confirming that the second-derivative identity cannot be derived from continuity alone. In the framework it supports the shift from polynomial to continuous route-independence in the Translation Theorem, consistent with the Aczél–Kannappan trichotomy that classifies solutions as constant, hyperbolic cosine, or trigonometric cosine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.