Foundation Dalembert Counterexamples Hquad Not D Alembert

A counterexample that guards the theory

The d'Alembert equation, named for Jean le Rond d'Alembert's 1747 work on vibrating strings, is a functional equation of the form H(t+u) + H(t-u) = 2H(t)H(u). Functions that satisfy it, such as cosine and hyperbolic cosine, have a rigid structure tied to exponential and trigonometric families. In the Recognition Science framework, a shifted version of the core cost function's logarithm is expected to satisfy this equation, and that expectation is part of what forces the golden ratio and the eight-tick cycle.

The declaration Hquad_not_dAlembert establishes a boundary on that expectation. It shows a specific function, H(t) = t²/2 + 1, which is the shifted log-lift of the quadratic log-cost F(x) = (log x)²/2, does not satisfy the d'Alembert equation. The proof in the machine-checked library of formal theorems verifies that the conjunction fails: either H(0) is not 1, or the equation does not hold for all real t and u. In fact H(0) = 1, so it is the equation that fails.

The deeper point is structural. The quadratic log-cost admits a combiner P(u,v) = 2u + 2v such that F(xy) + F(x/y) = P(F(x), F(y)) for all positive x and y. It also satisfies the symmetry condition F(x) = F(1/x) and the calibration condition on its log-lift. Yet the d'Alembert structure still fails. This means the mere existence of some combiner, the weak hypothesis that a function pairs with any binary operation, is not enough to force the rigid structure the framework needs.

In Recognition Science, this counterexample is a guard. It shows the framework's central theorem, which derives the unique cost function J(x) = (x + 1/x)/2 - 1, cannot rest on the weak consistency condition alone. At least one further nondegeneracy axiom is required. The framework models the cost as a discrete record of recognition events, and this example clarifies which properties of that record are load-bearing and which are incidental.

The declaration does not claim the quadratic log-cost is a valid cost function in the framework, nor that it refutes the framework's theorems. It claims only that a specific hypothesis is insufficient. The quadratic example satisfies the weak consistency, symmetry, and calibration conditions, but it fails the d'Alembert equation, so any theorem that claims to force the d'Alembert form from the weak hypothesis must add at least one further axiom. This is a precise, negative result that sharpens the positive theorem.

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

lemma Fquad_symm {x : ℝ} (hx : 0 < x) : Fquad x = Fquad x⁻¹ := by
  -- log(x⁻¹) = -log x for x>0
  simp [Fquad, Cost.F_ofLog, Gquad, Real.log_inv, hx.ne']

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

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

What this page does not claim

The quadratic log-cost is a valid cost function in the framework. The counterexample refutes the framework's central theorems about the cost function. The d'Alembert equation is the only structural condition the framework's cost function must satisfy.

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: