Foundation Dalembert Counterexamples

The quadratic counterexample

The d'Alembert equation, named for Jean le Rond d'Alembert's 1747 work on vibrating strings, is the functional equation H(t+u) + H(t-u) = 2 H(t) H(u). Its continuous solutions are the hyperbolic cosine and its relatives, and it appears across analysis whenever a function is determined by its values on sums and differences. In the Recognition Science framework, the equation is a target: the framework's forcing chain aims to show that the cost function's structure leads to this d'Alembert form for a related function called the log-lift.

The module Counterexamples establishes a boundary on that ambition. It defines a quadratic log-cost F(x) = (log x)² / 2 and shows that this function satisfies the weak consistency condition: there exists some combiner P such that F(xy) + F(x/y) = P(F(x), F(y)). Here the combiner is simply P(u,v) = 2u + 2v, an additive rule. The quadratic log-cost also passes two other checks: it vanishes at x = 1, and its second derivative at 1 equals 1, matching the calibration condition used in the framework.

Yet the shifted log-lift H(t) = F(exp t) + 1 = t²/2 + 1 fails the d'Alembert equation. The theorem Hquad_not_dAlembert states this failure directly. The quadratic function satisfies the weak hypothesis but not the strong conclusion. This is a structural obstruction: any theorem claiming to force the d'Alembert form from the mere existence of a combiner P must add at least one further nondegeneracy axiom. The quadratic example is not a defect in the framework; it is a precise statement of what the weak hypothesis alone cannot deliver.

In Recognition Science, the consequence is a sharper research target. The framework's library proves that the full cost function J(x) = (x + 1/x)/2 - 1 satisfies the d'Alembert structure under five plain conditions. The counterexample shows why those conditions, including the forced composition law and continuity, are not optional decoration. Each axiom earns its place by excluding a case like the quadratic one. The module thus clarifies the logical territory: the path from weak consistency to the d'Alembert form runs through additional structure, not through the bare existence of a combiner.

lemma Fquad_consistency :
    ∀ x y : ℝ, 0 < x → 0 < y →
      Fquad (x * y) + Fquad (x / y) = Padd (Fquad x) (Fquad y) := by
  intro x y hx hy
  -- Work in log-coordinates: let t = log x, u = log y
  have hx0 : x ≠ 0 := hx.ne'
  have hy0 : y ≠ 0 := hy.ne'
  have hlog_mul : Real.log (x * y) = Real.log x + Real.log y := by
    simpa using Real.log_mul hx.ne' hy.ne'
  have hlog_div : Real.log (x / y) = Real.log x - Real.log y := by
    simpa [div_eq_mul_inv, Real.log_mul, Real.log_inv, hy0] using Real.log_div hx.ne' hy.ne'
  -- Now compute
  simp [Fquad, Cost.F_ofLog, Gquad, Padd, hlog_mul, hlog_div]
  ring

theorem Hquad_not_dAlembert :
    ¬ (Hquad 0 = 1 ∧ ∀ t u : ℝ, Hquad (t + u) + Hquad (t - u) = 2 * Hquad t * Hquad u) := by
  intro h
  have h0 : Hquad 0 = 1 := h.1
  have hdA := h.2
  -- Evaluate the d'Alembert identity at t = 1, u = 1.
  have h11 := hdA 1 1
  -- Compute both sides explicitly; they disagree (4 ≠ 9/2).
  have hL : Hquad (1 + 1) + Hquad (1 - 1) = 4 := by
    calc
      Hquad (1 + 1) + Hquad (1 - 1)
          = ((1 + 1) ^ 2 / 2 + 1) + ((1 - 1) ^ 2 / 2 + 1) := by
              simp [Hquad_simp]
      _ = 4 := by
            norm_num
  have hR : 2 * Hquad 1 * Hquad 1 = (9 : ℝ) / 2 := by
    simp [Hquad_simp]
    ring
  -- Contradiction
  have : (4 : ℝ) = (9 : ℝ) / 2 := by
    calc (4 : ℝ) = Hquad (1 + 1) + Hquad (1 - 1) := by simpa using hL.symm
      _ = 2 * Hquad 1 * Hquad 1 := h11
      _ = (9 : ℝ) / 2 := hR
  norm_num at this

lemma Fquad_unit0 : Fquad 1 = 0 := by
  simp [Fquad, Cost.F_ofLog, Gquad]

lemma calib_Fquad : deriv (deriv (fun t : ℝ => Fquad (Real.exp t))) 0 = 1 := by
  -- Fquad(exp t) = t^2/2
  have hfun : (fun t : ℝ => Fquad (Real.exp t)) = fun t => t ^ 2 / 2 := by
    funext t
    simp [Fquad_on_exp, Gquad]
  -- Differentiate twice
  rw [hfun]
  -- First derivative: d/dt (t^2/2) = t
  have hderiv_eq : deriv (fun t : ℝ => t ^ 2 / 2) = fun t => t := by
    funext t
    have hpow : HasDerivAt (fun s : ℝ => s ^ 2) (2 * t) t := by
      simpa using (HasDerivAt.fun_pow (hasDerivAt_id t) 2)
    have hdiv : HasDerivAt (fun s : ℝ => s ^ 2 / 2) ((2 * t) / 2) t :=
      hpow.div_const 2
    have hcoef : ((2 * t) / 2 : ℝ) = t := by ring
    simpa [hcoef] using hdiv.deriv
  -- Second derivative at 0: d/dt (t) at 0 = 1
  simpa [hderiv_eq] using (hasDerivAt_id (0 : ℝ)).deriv

What this page does not claim

The module does not prove that the full cost function J(x) fails the d'Alembert equation; J satisfies it under the five conditions. The counterexample does not show that the framework's forcing chain is invalid, only that the weak hypothesis alone is insufficient. The quadratic log-cost is not claimed to be a physically realized cost function in the framework.

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/DAlembert/Counterexamples.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: