mulDAlembert_diff_sq_trace
plain-language theorem explainer
Any real map T obeying the multiplicative d'Alembert law T(xy)+T(x/y)=T(x)T(y) with T(1)=2 satisfies (T(xy)-T(x/y))²=(T(x)²-4)(T(y)²-4) for nonzero x,y. Cost and recognition-trace workers cite it when staying in doubled-trace units instead of the unit-normalized generator. The proof rescales to g=T/2, applies the unit difference-square lemma, and clears the factor of four by ring algebra.
Claim. Let $T:\mathbb{R}\to\mathbb{R}$ satisfy $T(xy)+T(x/y)=T(x)\,T(y)$ whenever $x,y\neq 0$, and $T(1)=2$. Then for all $x,y\neq 0$, $(T(xy)-T(x/y))^2=(T(x)^2-4)(T(y)^2-4)$.
background
The module develops real-trace roots and multiplicative d'Alembert identities for cost and recognition traces. Doubled-trace normalization $T(1)=2$ is the natural scale for hyperbolic traces: the model solution $T(x)=x+x^{-1}$ (equivalently $2\cosh\log x$ on positives) has $T(1)=2$. The companion unit-normalized generator is $g=T/2$, so $g(1)=1$ and the sum law becomes $g(xy)+g(x/y)=2,g(x)g(y)$.
Upstream, the unit-normalized difference-square lemma states that under that law and $g(1)=1$, $(g(xy)-g(x/y))^2=4((g x)^2-1)((g y)^2-1)$. Related lemmas give multiplicative duplication $g(x^2)=2(gx)^2-1$ and a product identity obtained by feeding $(xy,x/y)$ into the sum law. The real-trace-root map extracts the principal branch $t\mapsto(t+\sqrt{t^2-4})/2$ for $t\ge 2$, with multiplication and add-inverse identities tying traces back to roots.
proof idea
Set $g:=T/2$. From $T(xy)+T(x/y)=T(x)T(y)$ and $T(1)=2$, field simplification plus linear arithmetic yields the unit d'Alembert law for $g$ with $g(1)=1$. Apply the upstream unit difference-square theorem to get $(g(xy)-g(x/y))^2=4((gx)^2-1)((gy)^2-1)$. Two ring identities rewrite the left side as $(T(xy)-T(x/y))^2/4$ and the right side as $(T(x)^2-4)(T(y)^2-4)/4$. Substitute those into the $g$-identity, cancel the nonzero factor $4$ by field simplification, and conclude.
why it matters
In Recognition Science the cost is forced to the J-cost $J(x)=(x+x^{-1})/2-1$ (forcing step T5), a shifted cosh-log. Doubled traces $T=x+x^{-1}$ (so $T=2(J+1)$) are the additive characters of the multiplicative group, and the d'Alembert sum law is the functional skeleton behind the Recognition Composition Law. This lemma supplies the squared-difference form directly in $T$-units, which is the shape needed for larger-trace reconstruction (the cosh-addition formula for the bigger of $T(xy)$ and $T(x/y)$) and for multiplying principal real-trace roots. No downstream uses are recorded yet in the graph; it closes the local suite of multiplicative d'Alembert identities in Cost.RealTraceRoot and stands ready for cost-composition and ladder arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.