mulDAlembert_diff_sq
plain-language theorem explainer
Under the multiplicative d'Alembert sum law g(xy)+g(x/y)=2g(x)g(y) with g(1)=1, the squared difference (g(xy)-g(x/y))² equals 4(g(x)²-1)(g(y)²-1) for nonzero x,y. Cost and real-trace-root arguments cite this to turn sum data into a product of defect factors. The proof expands the square, substitutes the sum law and product identity, then reduces via duplication on each argument.
Claim. Let $g:\mathbb{R}\to\mathbb{R}$ satisfy $g(xy)+g(x/y)=2\,g(x)\,g(y)$ whenever $x,y\neq 0$, and $g(1)=1$. Then for all $x,y\neq 0$, $(g(xy)-g(x/y))^2=4\bigl((g x)^2-1\bigr)\bigl((g y)^2-1\bigr)$.
background
The module develops real-valued solutions of the multiplicative d'Alembert equation, the two-variable sum law that characterises (under mild regularity) the normalised multiplicative trace $g(x)=(x+x^{-1})/2$. In Recognition Science this is the unshifted form of the J-cost: $J(x)=g(x)-1=\cosh(\log x)-1$, forced unique at T5 of the unified forcing chain and tied to the Recognition Composition Law.
Standing hypotheses are the pointwise sum law $g(xy)+g(x/y)=2g(x)g(y)$ on nonzero reals and the normalisation $g(1)=1$. Two prior lemmas in the same module supply the algebra: multiplicative duplication yields $g(x^2)=2g(x)^2-1$ from the product law at $(x,x)$, and the product identity, obtained by feeding $(xy,x/y)$ into the sum law, yields $g(x^2)+g(y^2)=2,g(xy),g(x/y)$.
proof idea
Fix nonzero $x,y$. Record the sum law at $(x,y)$, the product identity at $(x,y)$, and duplication at both $x$ and $y$. Rewrite the product identity by substituting the two duplication formulae, so its left-hand side becomes $(2g(x)^2-1)+(2g(y)^2-1)$.
Expand the target square as $(a-b)^2=(a+b)^2-4ab$ with $a=g(xy)$, $b=g(x/y)$. Replace $a+b$ by the sum-law value $2g(x)g(y)$, and replace $2ab$ via the rewritten product identity. A final ring closes the identity to $4(g(x)^2-1)(g(y)^2-1)$.
why it matters
Feeds directly into the doubled-trace restatement: with $T=2g$ and $T(1)=2$, one obtains $(T(xy)-T(x/y))^2=(T(x)^2-4)(T(y)^2-4)$. That form matches the larger-trace and defect-factor bookkeeping used for realTraceRoot and the nonnegativity of $g^2-1$.
In the framework this is pure cost algebra under the multiplicative skeleton of the Recognition Composition Law. The same d'Alembert structure underlies J-uniqueness (T5) and the self-similar fixed point $\varphi$ (T6). The factors $g^2-1$ are the natural defect measures on the $\varphi$-ladder (squared hyperbolic sines of the log-coordinates).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.