Cost Real Trace Root Mul Dalembert Diff Sq

The difference-square identity

The d'Alembert equation, named for Jean le Rond d'Alembert's 1747 work on vibrating strings, is a functional equation that constrains how a function behaves under the product and quotient of its arguments. The classical form, g(x·y) + g(x/y) = 2·g(x)·g(y), appears across mathematics and physics, from harmonic analysis to special relativity. The declaration mulDAlembert_diff_sq in the framework's machine-checked library of formal theorems proves a sharp consequence of this law: for any function g satisfying the equation and normalized so that g(1) = 1, the square of the difference between g(x·y) and g(x/y) equals 4·(g(x)² − 1)·(g(y)² − 1), for all nonzero x and y.

The identity is a pure algebraic derivation. It follows from three earlier results in the same library: the product law applied to the pair (x·y, x/y), the duplication formula g(x²) = 2·g(x)² − 1, and the sum of the two equations. The proof uses only the defining law, the normalization at 1, and standard field arithmetic. It does not require continuity, differentiability, or any regularity assumption on g. The theorem is stated for real-valued functions on the real numbers, and the proof is checked by the machine, so the derivation is exact within the framework's axioms.

In the framework's recognition account, which models physical structure from a discrete record of events, this identity supports a later step: it connects the difference-square of the trace function to the product of two factors, each of the form (g(x)² − 1). That form is what allows the real trace root, the principal root of X² − tX + 1 = 0 for t ≥ 2, to be introduced as a solution. The declaration itself does not introduce that root, nor does it state the uniqueness theorem for the cost function. It is one lemma in a longer chain, not the chain's conclusion.

What the declaration does not claim is as important as what it proves. It does not assert that any function satisfying the d'Alembert equation must be continuous or of a specific form; the theorem holds for all functions, including pathological ones, as long as the algebraic law and normalization hold. It does not claim that the equation has a unique solution, and it does not identify g with any particular physical quantity. The identity is a conditional statement: if a function obeys the law and the normalization, then the difference-square relation follows. The framework's later results, which do impose additional conditions, are separate declarations with their own proofs.

/-- **Difference square.** Sum law, product identity, and duplication on `x`, `y`. -/
theorem mulDAlembert_diff_sq {g : ℝ → ℝ}
    (hd : ∀ x y, x ≠ 0 → y ≠ 0 → g (x * y) + g (x / y) = 2 * g x * g y)
    (h1 : g 1 = 1) :
    ∀ x y, x ≠ 0 → y ≠ 0 →
      (g (x * y) - g (x / y)) ^ 2
        = 4 * ((g x) ^ 2 - 1) * ((g y) ^ 2 - 1) := by
  intro x y hx hy
  have hsum := hd x y hx hy
  have hprod := mulDAlembert_prod hd x y hx hy
  have hdx := mulDAlembert_duplication hd h1 x hx
  have hdy := mulDAlembert_duplication hd h1 y hy
  rw [hdx, hdy] at hprod
  have expand : (g (x * y) - g (x / y)) ^ 2
      = (g (x * y) + g (x / y)) ^ 2 - 2 * (2 * g (x * y) * g (x / y)) := by ring
  rw [expand, hsum, ← hprod]
  ring

/-- **Difference square.** Sum law, product identity, and duplication on `x`, `y`. -/
theorem mulDAlembert_diff_sq {g : ℝ → ℝ}
    (hd : ∀ x y, x ≠ 0 → y ≠ 0 → g (x * y) + g (x / y) = 2 * g x * g y)
    (h1 : g 1 = 1) :
    ∀ x y, x ≠ 0 → y ≠ 0 →
      (g (x * y) - g (x / y)) ^ 2
        = 4 * ((g x) ^ 2 - 1) * ((g y) ^ 2 - 1) := by
  intro x y hx hy
  have hsum := hd x y hx hy
  have hprod := mulDAlembert_prod hd x y hx hy
  have hdx := mulDAlembert_duplication hd h1 x hx
  have hdy := mulDAlembert_duplication hd h1 y hy
  rw [hdx, hdy] at hprod
  have expand : (g (x * y) - g (x / y)) ^ 2
      = (g (x * y) + g (x / y)) ^ 2 - 2 * (2 * g (x * y) * g (x / y)) := by ring
  rw [expand, hsum, ← hprod]
  ring

What this page does not claim

The declaration does not claim that the d'Alembert equation has a unique solution. It does not assert continuity or any regularity property of g. It does not identify g with a physical quantity or introduce the real trace root.

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: