ContinuousCombinerPsiAffineCompletion
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the second-derivative identity from continuity of the combiner alone.
- Does not exclude the quartic-log counterexample without the extra hypotheses.
- Does not treat non-smooth or non-differentiable combiners.
- Does not compute the explicit numerical value of the coefficient $c$.
Lean usage
theorem use_psi_affine (C : ComparisonOperator) (h : SatisfiesLawsOfLogicContinuous C) (hSmooth : ContDiff ℝ ⊤ (fun t => derivedCost C (Real.exp t))) (hDeriv : AczelSecondDerivativeIdentity (fun t => derivedCost C (Real.exp t))) : ContinuousCombinerPsiAffineCompletion C h hSmooth hDeriv := by sorryformal statement (Lean)
557def ContinuousCombinerPsiAffineCompletion
558 (C : ComparisonOperator)
559 (_h : SatisfiesLawsOfLogicContinuous C)
560 (_hSmooth : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
561 (fun t : ℝ => derivedCost C (Real.exp t)))
562 (_hDeriv : AczelSecondDerivativeIdentity (fun t : ℝ => derivedCost C (Real.exp t))) : Prop :=
proof body
Definition body.
563 ∃ c : ℝ, LogBilinearIdentity (fun t : ℝ => derivedCost C (Real.exp t)) c
564
565/-- Explicit package of the extra analysis needed to force bilinearity from
566an arbitrary continuous combiner. This is deliberately a hypothesis package,
567not an axiom. The quartic-log obstruction shows the package is not automatic
568from `SatisfiesLawsOfLogicContinuous`. -/