Foundation Dalembert Counterexamples Fquad

The quadratic counterexample

The quadratic function F(x) = (log x)² / 2 is the simplest smooth cost function that satisfies a weak bookkeeping consistency yet escapes the full d'Alembert structure. In plain terms: if you keep a ledger, a discrete record of events, and ask that the cost of combining two ratios depend only on the individual costs, this quadratic function obeys that rule with a simple additive combiner P(u, v) = 2u + 2v. It also meets the other basic conditions: it costs zero at unity, it is symmetric under reciprocal arguments, and its log-lift has the correct calibration at zero.

Yet the shifted log-lift H(t) = t²/2 + 1 fails the d'Alembert equation, the functional equation that would force the unique cost structure. The theorem Hquad_not_dAlembert proves this failure formally. The obstruction is structural: any theorem claiming to force the full structure from the weak hypothesis must add at least one further nondegeneracy axiom. The quadratic function is not a counterexample to the full forcing theorem, which includes that extra axiom; it is a counterexample to a weaker claim that would omit it.

This matters because it draws a precise boundary. The weak consistency condition alone does not single out the cost function J(x) = (x + 1/x)/2 - 1. The quadratic function satisfies the weak condition but not the full structure. The full theorem needs the additional axiom, and the counterexample shows why that axiom is not redundant. The framework's library of machine-checked formal theorems records this boundary exactly, so that no later theorem can silently rely on the weak condition alone.

The practical consequence is a sharper understanding of what the framework does and does not prove. The quadratic function is not a path to the golden ratio or to the forcing chain; it is a road sign that says the weak condition stops here. The full structure requires the stronger axiom, and the counterexample makes that requirement visible and checkable.

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 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 answer does not claim that the quadratic function is a valid cost function in the full Recognition Science framework, only that it satisfies the weak consistency condition. This answer does not claim that the full forcing theorem is false; the counterexample targets only the weaker hypothesis that omits the nondegeneracy axiom. This answer does not claim that the quadratic function is the only counterexample of its kind.

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: