Foundation Generalized Dalembert Aczel Kannappan Continuous D Alembert

The d'Alembert equation

The d'Alembert functional equation, written H(x+y) + H(x-y) = 2 H(x) H(y), asks for functions H that turn addition into multiplication. It first appeared in 1747 when Jean le Rond d'Alembert studied vibrating strings, and it has since become a standard tool in analysis. The equation is so rigid that, with only two mild conditions, every solution is known. If H is continuous and H(0) = 1, then H must be the constant function 1, a hyperbolic cosine cosh(αx), or a trigonometric cosine cos(αx), for some real number α. This classification, named for János Aczél and Pl. Kannappan, is a classical result of functional equations.

The classification is not merely plausible; it is proved inside the Recognition Science framework's machine-checked library of formal theorems. The theorem, called aczel_kannappan_continuous_dAlembert, starts from continuity, H(0) = 1, and the d'Alembert equation, and derives the trichotomy. The proof works by first showing that continuity upgrades H to an infinitely smooth function, then differentiating the equation twice to obtain the ordinary differential equation H'' = c H with c = H''(0), and finally solving that ODE in each of the three cases determined by the sign of c. Each step is a formal proof checked by a computer, so the classification is a theorem, not a conjecture.

In Recognition Science, this theorem serves a specific purpose. The framework models reasoning as a ledger, a discrete record of recognition events, and assigns a cost to each comparison. A key step in deriving the unique cost function requires that a certain combining function be bilinear. Earlier work assumed this combiner was a polynomial of degree at most two. The d'Alembert classification replaces that assumption with a weaker one: mere continuity of the combiner is enough. The framework's library proves that a continuous combiner satisfying the laws of logic must still have the bilinear form P(u,v) = 2u + 2v + c u v, for some constant c. This is a genuine extension, because a counterexample shows that continuity alone does not force the second-derivative identity needed in an intermediate step; the polynomial assumption is not simply redundant.

What the declaration does not claim is equally important. It does not claim that every continuous function satisfying the equation is one of the three forms; that would be false, because the classification requires H(0) = 1. It does not claim that the d'Alembert classification itself is new; it is a classical result, here re-proved inside the framework. And it does not claim that the full cost function derivation works from continuity alone. The library states that finite pairwise polynomial closure remains the sharp hypothesis for the main result, and the quartic log-cost example shows why. The d'Alembert theorem is a powerful tool, but it is one step in a larger chain, not the whole story.

/-- **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

/-- **Continuous-combiner bilinear classification** (hypothesis-package form).

The final bilinear conclusion follows if the explicit analysis package is
provided. It is not automatic from `SatisfiesLawsOfLogicContinuous`; the
quartic log-cost refutes the proposed second-derivative input. -/
theorem continuous_combiner_bilinear_classification
    (C : ComparisonOperator)
    (h : SatisfiesLawsOfLogicContinuous C)
    (hInputs : ContinuousCombinerAnalysisInputs 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) := by
  have hSmooth := continuous_combiner_log_smoothness_bootstrap C h hInputs.finite_smoothness
  have hLog := continuous_combiner_psi_affine_forcing C h hSmooth
    hInputs.second_derivative hInputs.psi_affine
  exact log_bilinear_positive_cost_bilinear (derivedCost C) hLog

/-- 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

What this page does not claim

The d'Alembert classification is new; it is a classical result re-proved inside the framework. Continuity alone is enough to derive the full cost function; finite pairwise polynomial closure remains the sharp hypothesis. Every continuous solution of the d'Alembert equation is one of the three forms; the condition H(0) = 1 is required.

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: