mulDAlembert_duplication
plain-language theorem explainer
Multiplicative duplication for real functions obeying the d'Alembert product law: if g(xy)+g(x/y)=2 g(x)g(y) and g(1)=1, then g(x^{2})=2 g(x)^{2}-1 for x≠0. Cited by anyone reducing cost or real-trace identities on the phi-ladder. Proof specializes the product law at equal arguments, rewrites x/x=1, and finishes by linear arithmetic.
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 suppose $g(1)=1$. Then for every $x\neq 0$, $g(x^{2})=2\,g(x)^{2}-1$.
background
The module develops real-trace and cost identities under a multiplicative d'Alembert law. The product hypothesis is the pure form $g(xy)+g(x/y)=2 g(x)g(y)$ on nonzero reals, normalized by $g(1)=1$. This is the same algebraic skeleton as the doubled-trace law $T(xy)+T(x/y)=T(x)T(y)$ with $T(1)=2$ after the rescaling $g=T/2$, and it matches the Chebyshev/cosh duplication pattern.
In Recognition Science the related cost is the J-functional $J(x)=(x+x^{-1})/2-1$ (T5 uniqueness; also $\cosh(\log x)-1$), whose composition law is the Recognition Composition Law. The present $g$-law is the homogeneous product piece used when working with traces or roots rather than the shifted cost $J$. Sibling facts in the module fix positivity and the square-root branch of the real trace (realTraceRoot, realTraceRoot_ge_one, realTraceRoot_mul).
proof idea
Term-mode specialization, not a wrapper. Introduce $x\neq 0$, instantiate the product law at the pair $(x,x)$, rewrite $x/x=1$ via div_self, substitute $g(1)=1$, and close with linarith to rearrange $g(x^{2})+1=2 g(x)^{2}$ into the stated duplication formula. No external lemmas beyond field arithmetic.
why it matters
Supplies the duplication step needed for the difference-square identities that follow in the same module. Downstream, mulDAlembert_diff_sq combines the sum/product law with this duplication on $x$ and $y$ to obtain $(g(xy)-g(x/y))^{2}=4(g(x)^{2}-1)(g(y)^{2}-1)$; mulDAlembert_diff_sq_trace is the same statement in doubled-trace units $T$ with $T(1)=2$. Those identities control how real-trace roots separate under multiplication and division, which is the algebraic engine behind cost comparisons on the phi-ladder.
Framework link: the product law is the homogeneous core of the Recognition Composition Law and of T5 J-uniqueness. Duplication is the discrete double-angle step that lets rung arithmetic close without analytic continuation. No open scaffold: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.