Foundation Dalembert Counterexamples Fquad Symm

A symmetry that does not force the structure

The declaration Fquad_symm establishes a narrow but important fact about a specific cost function. The function in question is the quadratic log-cost, defined as F(x) = (log x)² / 2 for positive x. The lemma proves that this function is symmetric under reciprocal arguments: F(x) = F(1/x) for all x > 0. In plain terms, the cost of recognizing a ratio x is exactly the same as recognizing its reciprocal 1/x. This is a property one would expect of a ledger that treats the two sides of a comparison symmetrically, and the proof is a direct consequence of the logarithm's sign change under inversion.

What makes this lemma significant is what it does not establish. The symmetry alone does not force the full d'Alembert structure that the Recognition Science framework derives for its canonical cost function. The quadratic log-cost does satisfy the weak consistency condition: there exists a combiner P such that F(xy) + F(x/y) = P(F(x), F(y)), with the additive combiner P(u,v) = 2u + 2v. It also satisfies the calibration condition on its log-lift. Yet the shifted log-lift H(t) = t²/2 + 1 fails the d'Alembert equation, which requires H(t+u) + H(t-u) = 2H(t)H(u). The theorem Hquad_not_dAlembert proves this failure directly.

This counterexample serves a precise structural role. It shows that the mere existence of some combiner P, satisfying the weak consistency hypothesis, is insufficient to derive the d'Alembert form. Any theorem claiming to force that form from the weak hypothesis must add at least one further nondegeneracy axiom. The quadratic log-cost is therefore not a competing model of the framework's canonical cost; it is a boundary marker showing where the weak hypotheses stop and the stronger forcing conditions must begin. The lemma Fquad_symm is a clean, machine-checked proof of one property, and the surrounding declarations map out exactly how far that property reaches and where it falls short.

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

This answer does not claim that the quadratic log-cost is a viable model for the canonical recognition cost. This answer does not claim that the reciprocal symmetry alone is sufficient to derive the d'Alembert equation. This answer does not claim that the counterexample invalidates the framework's main forcing theorem.

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: