Cost Real Trace Root Mul Dalembert Prod

The product identity

The classical d'Alembert equation, named for Jean le Rond d'Alembert's 1747 work on vibrating strings, asks for functions that turn multiplication into addition. In its multiplicative form, a function g satisfies g(x·y) + g(x/y) = 2·g(x)·g(y) for all nonzero x and y. This is a standard object in functional equations, and without extra regularity assumptions it admits many wild solutions. The identity at hand, called the product identity, is a pure algebraic consequence of that law alone.

Take the law and apply it to the pair (x·y, x/y). The product of those two arguments is x², and their quotient is y². Substituting and simplifying gives g(x²) + g(y²) = 2·g(x·y)·g(x/y). This is the theorem mulDAlembert_prod: a relation that holds for every function g satisfying the multiplicative d'Alembert law, with no further conditions. It does not require g(1) = 1, nor continuity, nor any regularity class. The proof is a short algebraic manipulation using only the law itself and the field axioms for real numbers.

In the Recognition Science framework, this identity is part of a chain that leads to the cost function J(x) = (x + 1/x)/2 − 1. The framework models recognition events as entries in a ledger, a discrete record of events, and derives the cost of recognition from five forced conditions. The product identity is one algebraic step in that derivation, connecting the d'Alembert law to the duplication formula g(x²) = 2·g(x)² − 1 and the difference-square identity (g(x·y) − g(x/y))² = 4·(g(x)² − 1)·(g(y)² − 1). These are proved in the framework's machine-checked library of formal theorems, but the product identity itself is a standalone algebraic fact.

What the declaration does not claim is equally precise. It does not assert that any particular function satisfies the d'Alembert law, nor that the law has a unique solution. It does not establish the cost function J, nor any physical consequence such as the golden ratio or the number of spatial dimensions. Those results require additional premises, including the normalization g(1) = 1 and the full forcing chain. The product identity is one link in a longer argument, not the argument itself.

The practical upshot is a reusable algebraic tool. Any function that obeys the multiplicative d'Alembert law, whether it is the classical cosine in disguise or a pathological non-measurable solution, must also obey the product identity. This makes the identity a reliable stepping stone for later steps in the framework's derivation, and a standalone fact a reader can verify by hand in a few lines.

/-- **Product identity.** Apply the law to arguments `(x*y)` and `(x/y)`. -/
theorem mulDAlembert_prod {g : ℝ → ℝ}
    (hd : ∀ x y, x ≠ 0 → y ≠ 0 → g (x * y) + g (x / y) = 2 * g x * g y) :
    ∀ x y, x ≠ 0 → y ≠ 0 →
      g (x * x) + g (y * y) = 2 * g (x * y) * g (x / y) := by
  intro x y hx hy
  have hxy : x * y ≠ 0 := mul_ne_zero hx hy
  have hxdy : x / y ≠ 0 := div_ne_zero hx hy
  have h := hd (x * y) (x / y) hxy hxdy
  have hprod : (x * y) * (x / y) = x * x := by field_simp [hy]
  have hquot : (x * y) / (x / y) = y * y := by field_simp [hy]
  rw [hprod, hquot] at h
  linarith

What this page does not claim

The product identity does not assert existence or uniqueness of any solution to the d'Alembert law. The declaration does not establish the cost function J, the golden ratio, or any physical dimension. The identity holds without the normalization g(1) = 1, but that normalization is needed for later steps in the framework.

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/Cost/RealTraceRoot.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: