Foundation Dalembert Unconditional Rcl Unconditional

The unconditional composition law

The d'Alembert equation, named for Jean le Rond d'Alembert's 1747 work on vibrating strings, is a functional equation that asks how a function behaves when its inputs are added or subtracted. In the Recognition Science framework, a parallel question arises for the cost function, which measures the price of recognizing one thing in terms of another. The framework's cost function J(x) = (x + 1/x)/2 - 1 assigns a nonnegative number to every positive ratio x, with J(1) = 0 meaning no cost when the two things are identical.

The declaration rcl_unconditional proves that if this cost function satisfies a multiplicative consistency condition, then the way two costs combine is forced to be exactly P(u, v) = 2uv + 2u + 2v. The condition states: J(xy) + J(x/y) = P(J(x), J(y)) for some function P. The theorem shows that P must be that specific polynomial, not merely for a few inputs but for all nonnegative values u and v. This is the strongest possible form of the result because it places no assumption on P whatsoever; P is computed from the known properties of J, not assumed in advance.

The proof relies on the fact that J is surjective onto the nonnegative reals: for every v ≥ 0 there is some x > 0 with J(x) = v. This lets the framework extend the identity from the range of J to the entire first quadrant. The key lemma, J_computes_P, shows that J itself satisfies the identity with P(u, v) = 2uv + 2u + 2v, and the surjectivity result then forces any candidate P to agree with this formula everywhere. The theorem P_uniqueness goes further: if two functions P and Q both satisfy the consistency equation with J, they must be identical on the nonnegative quadrant.

What this establishes in plain terms is that the composition law for recognition costs has no free parameters. Earlier versions of the framework assumed P was a polynomial, which invited the objection that the result only held within that restricted class. The unconditional version removes that assumption entirely. The framework's machine-checked library of formal theorems verifies that the only possible composition law is the one given, and that no irregular or exotic alternatives can slip through.

The consequence is that the entire forcing chain, from the cost function to the golden ratio and beyond, rests on a firmer foundation. The composition law is not a choice but a derived necessity, and this derivation is checked by the framework's library. What the declaration does not claim is that the cost function itself is derived here; that is established elsewhere. It also does not claim that the composition law applies to arbitrary functions, only to those satisfying the stated symmetry, normalization, calibration, and smoothness conditions that define the cost function.

/-- **THEOREM (Unconditional RCL Inevitability)**

If F : ℝ₊ → ℝ satisfies:
1. F = J (forced by symmetry + normalization + calibration + smoothness + ODE uniqueness)
2. F(xy) + F(x/y) = P(F(x), F(y)) for some function P

Then P(u, v) = 2uv + 2u + 2v on the entire first quadrant [0, ∞)².

**NO ASSUMPTION ON P IS MADE.** P is computed, not assumed.

This completely addresses the mathematician's concern about "irregular solutions":
there are none, because P is determined by F.
-/
theorem rcl_unconditional (P : ℝ → ℝ → ℝ)
    (hCons : ∀ x y : ℝ, 0 < x → 0 < y →
      Cost.Jcost (x * y) + Cost.Jcost (x / y) = P (Cost.Jcost x) (Cost.Jcost y)) :
    ∀ u v : ℝ, 0 ≤ u → 0 ≤ v → P u v = 2*u*v + 2*u + 2*v :=
  P_determined_nonneg P hCons

/-- J : (0, ∞) → [0, ∞) is surjective onto [0, ∞). -/
theorem J_surjective_nonneg :
    ∀ v : ℝ, 0 ≤ v → ∃ x : ℝ, 0 < x ∧ Cost.Jcost x = v := by
  intro v hv
  -- J(x) = (x + 1/x)/2 - 1
  -- J(1) = 0
  -- J(x) → ∞ as x → ∞ or x → 0⁺
  -- J is continuous on (0, ∞)
  -- By IVT, J takes all values in [0, ∞)
  -- For v = 0, take x = 1
  -- For v > 0, solve (x + 1/x)/2 - 1 = v
  --   => x + 1/x = 2v + 2
  --   => x² - (2v + 2)x + 1 = 0
  --   => x = (2v + 2 + √((2v+2)² - 4)) / 2 = v + 1 + √(v² + 2v)
  by_cases hv0 : v = 0
  · use 1
    constructor
    · exact one_pos
    · simp [Cost.Jcost, hv0]
  · -- v > 0 case
    have hv_pos : 0 < v := lt_of_le_of_ne hv (Ne.symm hv0)
    let discriminant := (2*v + 2)^2 - 4
    have h_disc_pos : 0 < discriminant := by
      simp only [discriminant]
      have h1 : (2*v + 2)^2 = 4*v^2 + 8*v + 4 := by ring
      rw [h1]
      have h2 : 4*v^2 + 8*v + 4 - 4 = 4*v^2 + 8*v := by ring
      rw [h2]
      have h3 : 4*v^2 + 8*v = 4*v*(v + 2) := by ring
      rw [h3]
      apply mul_pos
      · linarith
      · linarith
    let x := (2*v + 2 + Real.sqrt discriminant) / 2
    have hx_pos : 0 < x := by
      simp only [x]
      apply div_pos
      · have h1 : 0 < 2*v + 2 := by linarith
        have h2 : 0 ≤ Real.sqrt discriminant := Real.sqrt_nonneg _
        linarith
      · linarith
    use x
    constructor
    · exact hx_pos
    · -- Prove J(x) = v
      simp only [Cost.Jcost, x]
      -- Need to show: ((2v+2+√disc)/2 + 2/(2v+2+√disc))/2 - 1 = v
      -- This is algebraic manipulation
      have hx_ne : x ≠ 0 := hx_pos.ne'
      have h_quad : x^2 - (2*v + 2)*x + 1 = 0 := by
        simp only [x]
        have h_sqrt_sq : Real.sqrt discriminant ^ 2 = discriminant :=
          Real.sq_sqrt (le_of_lt h_disc_pos)
        field_simp
        simp only [discriminant] at h_sqrt_sq ⊢
        ring_nf
        ring_nf at h_sqrt_sq
        linarith
      -- From quadratic: x + 1/x = 2v + 2
      have h_sum : x + x⁻¹ = 2*v + 2 := by
        have h1 : x^2 + 1 = (2*v + 2)*x := by linarith [h_quad]
        field_simp at h1 ⊢
        linarith
      calc (x + x⁻¹) / 2 - 1 = (2*v + 2) / 2 - 1 := by rw [h_sum]
        _ = v + 1 - 1 := by ring
        _ = v := by ring

/-- If any P satisfies the consistency equation with J, it must be the RCL.
    This rules out ALL alternatives, polynomial or not. -/
theorem P_uniqueness (P Q : ℝ → ℝ → ℝ)
    (hP : ∀ x y : ℝ, 0 < x → 0 < y →
      Cost.Jcost (x * y) + Cost.Jcost (x / y) = P (Cost.Jcost x) (Cost.Jcost y))
    (hQ : ∀ x y : ℝ, 0 < x → 0 < y →
      Cost.Jcost (x * y) + Cost.Jcost (x / y) = Q (Cost.Jcost x) (Cost.Jcost y)) :
    ∀ u v : ℝ, 0 ≤ u → 0 ≤ v → P u v = Q u v := by
  intro u v hu hv
  have hP' := rcl_unconditional P hP u v hu hv
  have hQ' := rcl_unconditional Q hQ u v hu hv
  rw [hP', hQ']

What this page does not claim

The declaration does not derive the cost function J itself; that is established in separate modules. The composition law applies only to functions satisfying the stated conditions, not to arbitrary functions. The theorem does not claim that the consistency equation holds for all real inputs, only for positive x and y.

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/Unconditional.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: