Foundation Generalized Dalembert Continuous Combiner Finite Smoothness To Top

From finite to full smoothness

The d'Alembert functional equation, H(x+y) + H(x-y) = 2 H(x) H(y), is a classical object of analysis. Its continuous solutions, with H(0) = 1, were classified by János Aczél and Pl. Kannappan: every such solution is either the constant 1, a hyperbolic cosine cosh(αx), or a trigonometric cosine cos(αx). This classification, proved in the framework's machine-checked library of formal theorems, is the engine that lets the Recognition Science framework replace a polynomial regularity assumption with a much weaker continuity assumption.

In Recognition Science, the framework models a ledger, a discrete record of recognition events, and a cost, the forced price of each recognition. The framework's central theorem, the Law of Logic, states that any cost function satisfying five plain conditions must equal J(x) = (x + 1/x)/2 - 1. A key step in the proof requires a route-independence combiner, a function that combines two costs, to be a polynomial of total degree at most two. A counterexample, the quartic-log cost, shows that some regularity is needed, but polynomial degree at most two is stronger than necessary.

The declaration continuous_combiner_finite_smoothness_to_top establishes the bridge: if a cost function, after a logarithmic change of variables, is smooth at every finite order n, then it is smooth at every order, including infinite order. In symbols, if for all natural numbers n, the function t ↦ derivedCost C (exp t) is n-times continuously differentiable, then it is infinitely differentiable. This is a purely analytic fact, proved by a standard bootstrap argument, and it is what lets the framework's continuous-combiner version of the Laws of Logic drop the polynomial-degree-≤2 hypothesis.

The theorem does not claim that continuity alone is enough. A later counterexample, the quartic log-cost, blocks the proposed second-derivative identity, showing that finite pairwise polynomial closure remains the sharp hypothesis for the Law-of-Logic paper. The theorem also does not claim that the Aczél–Kannappan classification applies to all continuous functions; it applies to continuous solutions of the d'Alembert equation. The classification itself, proved as aczel_kannappan_continuous_dAlembert, is a separate theorem, and the framework's full classification of continuous combiners requires additional second-derivative and affine-completion inputs, packaged in ContinuousCombinerAnalysisInputs.

What the theorem changes is the framework's reach. With finite smoothness bootstrapped to full smoothness, the framework can classify continuous combiners, not just polynomial ones, and the polynomial case becomes a particular instance. The continuous-combiner version of SatisfiesLawsOfLogic is intended for downstream code, and the polynomial-case Translation Theorem becomes a special case. The framework's account of logic now rests on continuity, a much weaker and more natural regularity condition, and the quartic-log counterexample marks exactly where the boundary lies.

/-- **Residual input 1b: finite-order smoothness promotes to full top-level
smoothness for this log-cost.**

Lean's `ContDiff` index used by Mathlib distinguishes the imported `⊤ : ℕ∞`
from the outer `⊤ : WithTop ℕ∞` expected by downstream APIs. This input is the
formal promotion step from the finite-order certificates produced by the
mollifier route to the top-level smoothness statement consumed below. -/
theorem continuous_combiner_finite_smoothness_to_top
    (C : ComparisonOperator)
    (_h : SatisfiesLawsOfLogicContinuous C)
    (hFinite : ∀ n : ℕ, ContDiff ℝ n (fun t : ℝ => derivedCost C (Real.exp t))) :
    ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
      (fun t : ℝ => derivedCost C (Real.exp t)) := by
  exact SmoothnessTop.contDiff_top_of_contDiff_nat hFinite

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

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

/-- Classified log-costs always give a bilinear identity. -/
theorem classified_log_cost_bilinear
    (G : ℝ → ℝ) (hG : ClassifiedLogCost G) :
    ∃ c : ℝ, LogBilinearIdentity G c := by
  rcases hG with h0 | ⟨α, hpar⟩ | ⟨α, hcosh⟩ | ⟨α, hcos⟩
  · refine ⟨0, ?_⟩
    intro t u
    rw [h0 (t + u), h0 (t - u), h0 t, h0 u]
    ring
  · refine ⟨0, ?_⟩
    intro t u
    rw [hpar (t + u), hpar (t - u), hpar t, hpar u]
    exact log_parabolic_bilinear_identity α t u
  · refine ⟨2, ?_⟩
    intro t u
    rw [hcosh (t + u), hcosh (t - u), hcosh t, hcosh u]
    exact log_cosh_sub_one_bilinear_identity α t u
  · refine ⟨-2, ?_⟩
    intro t u
    rw [hcos (t + u), hcos (t - u), hcos t, hcos u]
    exact log_one_sub_cos_bilinear_identity α t u

What this page does not claim

Continuity alone is sufficient for the full classification of logic; the quartic-log counterexample shows it is not. The Aczél–Kannappan classification applies to all continuous functions; it applies only to continuous solutions of the d'Alembert equation. The framework derives the fine-structure constant alpha; its expression lands within about 5.6 parts per million of the measured value but its seed is an identification, not a derived coupling.

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: