Foundation Generalized Dalembert Continuous Combiner Psi Affine Forcing

The continuous combiner

The d'Alembert functional equation is a classical object of analysis. It asks for continuous functions H from the real line to itself, with H(0) = 1, that satisfy H(x+y) + H(x-y) = 2 H(x) H(y) for all real x and y. The Aczél–Kannappan classification, proved in full by J. Aczél and P. Kannappan in the 1960s, gives the complete answer: every continuous solution is the constant function 1, a hyperbolic cosine cosh(αx), or a trigonometric cosine cos(αx), for some real parameter α. The equation appears across mathematics, from harmonic analysis to the theory of group representations, wherever a function's value at a sum and difference is governed by its values at the parts.

In Recognition Science, the framework models comparison costs as functions on positive numbers, and route independence asks that combining two costs and then applying the derived cost give the same result regardless of the order of operations. The original route-independence condition required the combining rule P to be a polynomial of total degree at most two. The framework's library of machine-checked formal theorems proves that this polynomial restriction is stronger than needed. The key step is the Aczél–Kannappan classification itself, which the framework proves internally rather than assuming as an axiom. From continuity of the combiner, the framework derives that the cost function, after a logarithmic change of variables, must satisfy the d'Alembert equation, and the classification then forces the cost to be one of the three classical forms.

The declaration continuous_combiner_psi_affine_forcing packages one step of this argument. It states: if the route-independence combiner is continuous, if the cost function is smooth, and if a second-derivative identity and an affine-completion condition hold, then the logarithmically transformed cost satisfies a bilinear identity of the form G(t+u) + G(t-u) = 2 G(t) + 2 G(u) + c G(t) G(u) for some real constant c. The affine-completion condition says that a certain auxiliary function ψ, when evaluated at the cost values, takes the affine form ψ(G(t)) = 2 + c G(t). This is a theorem, not a definitional choice: the framework proves that these hypotheses force the bilinear identity.

What the declaration does not claim is just as important. It does not prove that the affine-completion condition follows from continuity alone. A later counterexample in the same module, the quartic log-cost, shows that continuity alone does not force the second-derivative identity that would make the affine condition automatic. The sharp hypothesis for the full uniqueness result remains finite pairwise polynomial closure of the combiner, as in the original Law-of-Logic paper. The continuous-combiner version is a generalization that drops the polynomial-degree-at-most-two assumption, but it requires the extra smoothness and affine conditions as explicit inputs. The framework's library also proves that the polynomial case is subsumed by the continuous case, so the older theorem becomes a particular instance of the newer one.

The practical consequence is a cleaner boundary for the framework's main cost theorem. A reader can now see that the polynomial restriction was an artifact of the proof technique, not a requirement of the underlying mathematics. The continuous-combiner route opens the door to cost functions that are not polynomials, as long as they satisfy the smoothness and affine conditions. The quartic log-cost counterexample shows exactly where the boundary lies: continuity is necessary but not sufficient. The framework's library keeps both versions, the polynomial and the continuous, so downstream results can choose the hypothesis that fits their application.

/-- **Aczél–Kannappan classification** (proved theorem, not axiom):
every continuous solution of the d'Alembert functional equation
`H(x+y) + H(x-y) = 2 H(x) H(y)` with `H(0) = 1` is either the
constant 1, a hyperbolic cosine, or a trigonometric cosine.

The proof reduces to
`IndisputableMonolith.Cost.FunctionalEquation.dAlembert_classification`,
which assembles the integration bootstrap, universal-coefficient ODE
derivation, and ODE uniqueness lemmas into the disjunction. -/
theorem aczel_kannappan_continuous_dAlembert
    (H : ℝ → ℝ) (hCont : Continuous H) (h_one : H 0 = 1)
    (hEq : ∀ x y : ℝ, H (x + y) + H (x - y) = 2 * H x * H y) :
    (∀ x, H x = 1) ∨
    (∃ α : ℝ, ∀ x, H x = Real.cosh (α * x)) ∨
    (∃ α : ℝ, ∀ x, H x = Real.cos (α * x)) :=
  IndisputableMonolith.Cost.FunctionalEquation.dAlembert_classification
    H h_one hCont hEq

/-- The continuous-combiner Law of Logic gives a continuous log-coordinate
Aczél equation. This is the formal input object for the smoothness bootstrap. -/
theorem log_aczel_data_of_laws
    (C : ComparisonOperator) (h : SatisfiesLawsOfLogicContinuous C) :
    ∃ P : ℝ → ℝ → ℝ,
      LogAczelData (fun t : ℝ => derivedCost C (Real.exp t)) P := by
  obtain ⟨P, hPcont, hPsym, hCons⟩ := h.route_independence
  refine ⟨P, ?_⟩
  have hFcont : ContinuousOn (derivedCost C) (Set.Ioi (0 : ℝ)) :=
    excluded_middle_implies_continuous C h.excluded_middle
  have hNorm : derivedCost C 1 = 0 :=
    identity_implies_normalized C h.identity
  have hSymm : IsSymmetric (derivedCost C) :=
    non_contradiction_and_scale_imply_reciprocal C h.non_contradiction h.scale_invariant
  refine
    { continuous_G := continuous_log_cost_of_continuousOn_positive (derivedCost C) hFcont
      zero_G := by simpa [derivedCost] using hNorm
      even_G := ?_
      continuous_P := hPcont
      symmetric_P := hPsym
      aczel_eq := ?_ }
  · exact IndisputableMonolith.Cost.FunctionalEquation.G_even_of_reciprocal_symmetry
      (derivedCost C) (by intro x hx; exact hSymm x hx)
  · intro t u
    have htu_pos : 0 < Real.exp t := Real.exp_pos t
    have huu_pos : 0 < Real.exp u := Real.exp_pos u
    have h := hCons (Real.exp t) (Real.exp u) htu_pos huu_pos
    simpa [Real.exp_add, Real.exp_sub] using h

/-- **Residual input 2 assembled:** smoothness plus the derivative identity
and ψ-affine completion give the required log-bilinear identity. -/
theorem continuous_combiner_psi_affine_forcing
    (C : ComparisonOperator)
    (h : SatisfiesLawsOfLogicContinuous C)
    (hSmooth : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
      (fun t : ℝ => derivedCost C (Real.exp t)))
    (hDeriv : ContinuousCombinerSecondDerivativeInput C h hSmooth)
    (hPsi : ContinuousCombinerPsiAffineCompletion C h hSmooth hDeriv) :
    ∃ c : ℝ, LogBilinearIdentity (fun t : ℝ => derivedCost C (Real.exp t)) c := by
  exact hPsi

/-- A classified positive-ratio cost admits a bilinear combiner on positive
ratios. This is Piece 5 of the axiom-2 attack: once the log-coordinate
classification is known, the bilinear witness is explicit. -/
theorem classified_positive_cost_bilinear
    (F : ℝ → ℝ)
    (hClass : ClassifiedLogCost (fun t : ℝ => F (Real.exp t))) :
    ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
      (∀ x y : ℝ, 0 < x → 0 < y →
        F (x * y) + F (x / y) = P (F x) (F y)) ∧
      (∀ u v, P u v = 2*u + 2*v + c*u*v) := by
  obtain ⟨c, hbil⟩ := classified_log_cost_bilinear (fun t : ℝ => F (Real.exp t)) hClass
  refine ⟨fun u v => 2*u + 2*v + c*u*v, c, ?_, ?_⟩
  · intro x y hx hy
    have hxne : x ≠ 0 := ne_of_gt hx
    have hyne : y ≠ 0 := ne_of_gt hy
    have hxy : 0 < x * y := mul_pos hx hy
    have hxdiv : 0 < x / y := div_pos hx hy
    have hlog_xy : Real.log (x * y) = Real.log x + Real.log y :=
      Real.log_mul hxne hyne
    have hlog_div : Real.log (x / y) = Real.log x - Real.log y :=
      Real.log_div hxne hyne
    have hx_exp : Real.exp (Real.log x) = x := Real.exp_log hx
    have hy_exp : Real.exp (Real.log y) = y := Real.exp_log hy
    have h := hbil (Real.log x) (Real.log y)
    dsimp only at h
    rw [← hx_exp, ← hy_exp]
    rw [← Real.exp_add, ← Real.exp_sub]
    exact h
  · intro u v
    rfl

/-- Every polynomial-LoL operator is a continuous-LoL operator. The bilinear
conclusion still requires the explicit analysis package at this level; the
ordinary polynomial theorem in `LogicAsFunctionalEquation` remains the
unconditional route. -/
theorem laws_continuous_subsumes_polynomial
    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C)
    (hInputs : ContinuousCombinerAnalysisInputs C
      (laws_polynomial_implies_continuous C h)) :
    ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
      (∀ x y : ℝ, 0 < x → 0 < y →
        derivedCost C (x * y) + derivedCost C (x / y)
          = P (derivedCost C x) (derivedCost C y)) ∧
      (∀ u v, P u v = 2*u + 2*v + c*u*v) :=
  RCL_is_unique_functional_form_of_logic_continuous C
    (laws_polynomial_implies_continuous C h) hInputs

What this page does not claim

The continuous-combiner theorem does not prove that the affine-completion condition follows from continuity alone. The framework does not claim that every continuous cost function satisfies the d'Alembert equation; the continuous route-independence predicate is a hypothesis, not a consequence. The declaration does not establish the full uniqueness of the cost function J(x) = (x + 1/x)/2 - 1; that remains the separate Law-of-Logic theorem with its polynomial hypothesis.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/GeneralizedDAlembert.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: