Foundation Dalembert Counterexamples Hquad Simp

What Hquad_simp shows

The d'Alembert equation, named for Jean le Rond d'Alembert's 1747 work on vibrating strings, is a functional equation that characterizes functions whose value at a sum and difference combine in a fixed way. In one variable it reads H(t+u) + H(t−u) = 2H(t)H(u), and its continuous solutions are the hyperbolic cosine and its relatives. The equation appears throughout physics because it encodes linear superposition.

The Recognition Science library, a machine-checked collection of formal theorems, examines whether a weak hypothesis forces this structure. The hypothesis is that some combiner P exists with F(xy) + F(x/y) = P(F(x), F(y)). The declaration Hquad_simp establishes a concrete counterexample: for the quadratic log-cost F(x) = (log x)²/2, the shifted log-lift H(t) = F(exp t) + 1 simplifies to t²/2 + 1. This H is the function whose d'Alembert property is at stake.

The library proves that this H fails the d'Alembert equation, while the underlying F satisfies the weak consistency condition with the additive combiner P(u,v) = 2u + 2v. That means the mere existence of some combiner does not force the d'Alembert form. Any theorem claiming to derive the full structure from the weak hypothesis must add at least one further nondegeneracy axiom.

In Recognition Science, the d'Alembert form is a step toward the forced cost function J(x) = (x + 1/x)/2 − 1. This counterexample shows why the forcing chain needs its full five conditions: reciprocal symmetry alone, or even with a combiner, leaves room for quadratic costs that do not lead to J.

lemma Hquad_simp (t : ℝ) : Hquad t = t ^ 2 / 2 + 1 := by
  simp [Hquad, Fquad_on_exp, Gquad]

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

What this page does not claim

Hquad_simp does not claim that the quadratic log-cost satisfies the full Recognition Science cost theorem. Hquad_simp does not claim that no combiner can force d'Alembert; it only shows that one weak combiner does not. Hquad_simp does not claim that the d'Alembert equation is the only route to the forced cost function.

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: