mulDAlembert_prod
plain-language theorem explainer
If a real function obeys the multiplicative d'Alembert law g(xy)+g(x/y)=2 g(x) g(y) off zero, then g(x²)+g(y²)=2 g(xy) g(x/y). Cost and functional-equation workers cite it when building difference-square identities for real trace roots of the Recognition cost. The proof is a direct substitution of the pair (xy, x/y) into the law, followed by field simplification.
Claim. Let $g:\mathbb{R}\to\mathbb{R}$ satisfy $g(xy)+g(x/y)=2\,g(x)\,g(y)$ for all $x,y\neq 0$. Then for all $x,y\neq 0$, $g(x^{2})+g(y^{2})=2\,g(xy)\,g(x/y)$.
background
The module develops real-valued roots of the Recognition cost trace. The pure multiplicative d'Alembert equation
$$g(xy)+g(x/y)=2,g(x),g(y)\qquad(x,y\neq 0)$$
is the composition law satisfied by $g=T/2$, where $T(x)=x+x^{-1}$ (equivalently $g(x)=\cosh(\log x)$ on positives). This is the linearised form of the Recognition Composition Law after the shift that removes the additive $2J$ terms: if $J(x)=(x+x^{-1})/2-1$, then $T=2(J+1)$ obeys $T(xy)+T(x/y)=T(x)T(y)$ with $T(1)=2$.
The present lemma is the product dual of the usual sum law: evaluate the same identity on the composite arguments $xy$ and $x/y$. Non-vanishing of products and quotients is the only arithmetic prerequisite (standard field facts on $\mathbb{R}$).
proof idea
Fix nonzero $x,y$. The products $xy$ and $x/y$ are nonzero. Instantiate the hypothesis at the pair $(xy,,x/y)$:
$$g\bigl((xy)\cdot(x/y)\bigr)+g\bigl((xy)/(x/y)\bigr)=2,g(xy),g(x/y).$$
Field simplification yields $(xy)\cdot(x/y)=x^{2}$ and $(xy)/(x/y)=y^{2}$. Rewrite and rearrange by linear arithmetic to obtain $g(x^{2})+g(y^{2})=2,g(xy),g(x/y)$.
why it matters
This product identity is the middle algebraic step between the raw d'Alembert law and the difference-square formulae that control real trace roots. Downstream, mulDAlembert_diff_sq combines the sum law, this product identity, and duplication (with $g(1)=1$) to obtain
$$\bigl(g(xy)-g(x/y)\bigr)^{2}=4\bigl(g(x)^{2}-1\bigr)\bigl(g(y)^{2}-1\bigr).$$
The companion mulDAlembert_diff_sq_trace restates the same identity in doubled-trace units $T=2g$ with $T(1)=2$. Those identities certify non-negativity and ordering properties of the real square-root branch of the cost trace, tying the local Cost algebra back to T5 J-uniqueness and the RCL in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.