Foundation Dalembert Counterexamples Fquad Consistency

A warning about weak premises

The d'Alembert equation is a classical functional equation from 1747, used by Jean le Rond d'Alembert to study vibrating strings. In modern form it asks for functions H satisfying H(t+u) + H(t−u) = 2H(t)H(u), a relation that forces cosine and hyperbolic cosine as its smooth solutions. The Recognition Science framework encounters this equation when it tries to derive its central cost function from weak premises about how a ledger (a discrete record of events) combines costs.

The declaration Fquad_consistency, proved in the framework's machine-checked library of formal theorems, establishes a warning. It shows that the quadratic log-cost F(x) := (log x)²/2 satisfies a weak consistency condition: for positive x and y, F(xy) + F(x/y) = P(F(x), F(y)) for some combiner P. Specifically, P(u,v) := 2u + 2v works. This looks like progress toward the framework's goal, but the declaration then proves the hope fails. The shifted log-lift H(t) := t²/2 + 1 does not satisfy the d'Alembert equation at all.

The point is structural. The mere existence of some combiner P is too weak a hypothesis. Any theorem that claims to force the d'Alembert form from this premise alone must add at least one further nondegeneracy axiom. The quadratic example satisfies the weak consistency, satisfies symmetry F(x) = F(1/x), and even satisfies a calibration condition on its second derivative at 1, yet it still escapes the d'Alembert structure. This is not a failure of the framework's main theorem; it is a precise boundary on what that theorem needs as input.

What Fquad_consistency does not claim is equally important. It does not show that the framework's five conditions are insufficient; those conditions include a forced composition law and continuity, which the quadratic example does not satisfy. It does not disprove the d'Alembert equation or suggest the framework's central result is wrong. It only closes one tempting shortcut: you cannot replace the full composition law with the bare existence of some combiner and still expect the golden-ratio forcing chain to follow.

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

What this page does not claim

This does not claim the framework's five conditions are insufficient; the quadratic example fails the forced composition law and continuity conditions. This does not claim the d'Alembert equation is false or that the framework's central uniqueness theorem is wrong. This does not claim the weak consistency condition alone is enough to derive any cost structure.

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: