trace_diagSL_mul
plain-language theorem explainer
The product of two split-torus diagonal SL(2) matrices has trace equal to the sum of the products of their eigenvalues and reciprocal eigenvalues. Anyone deriving the Recognition Composition Law as an SL(2) trace identity on the diagonal torus cites this evaluation. The proof is a one-line simplification of the explicit 2×2 matrix product.
Claim. For all real $x,y$, writing $D(x)=\mathrm{diag}(x,x^{-1})$ for the diagonal area-preserving matrix, $\mathrm{tr}\bigl(D(x)\,D(y)\bigr)=xy+x^{-1}y^{-1}$.
background
In the symplectic ledger picture, a recognition event is a linear map of the debit-credit phase space $\mathbb{R}^2$. Area preservation (the $\sigma=0$ law) forces $\det M=1$, i.e. $M\in\mathrm{SL}(2,\mathbb{R})=\mathrm{Sp}(2,\mathbb{R})$. The split-torus elements are the diagonal matrices $D(x)=\mathrm{diag}(x,x^{-1})$, the canonical area-preserving maps with eigenvalue pair $(x,x^{-1})$.
The module identifies the canonical cost $J(x)=\tfrac12(x+x^{-1})-1$ with a calibrated trace functional on these maps. The Recognition Composition Law then appears as the SL(2) trace identity restricted to the split torus. Evaluating the trace of a product of two diagonal elements is the elementary algebraic step that makes that restriction explicit.
Upstream, $D(x)$ is defined as the $2\times 2$ matrix with diagonal $(x,x^{-1})$; the ambient trace is the ordinary matrix trace (here on $\mathrm{Fin},2$).
proof idea
One-line wrapper: unfold the definition of the diagonal matrix $D(x)$ and apply the standard two-by-two matrix-trace formula. The product is again diagonal with entries $xy$ and $x^{-1}y^{-1}$, so the trace identity is immediate by simplification.
why it matters
This lemma is the first rewrite step inside the scalar split-torus trace identity, the diagonal restriction of the SL(2) matrix identity $\mathrm{tr}(AB)+\mathrm{tr}(AB^{-1})=\mathrm{tr}(A),\mathrm{tr}(B)$. That scalar form is how the module discharges the bridge from the Recognition Composition Law (a stated primitive in the functional-equation derivation) to a ledger-forced variational principle.
Together with the companion evaluation for the product against the inverse, it converts the matrix identity into $(xy+x^{-1}y^{-1})+(xy^{-1}+x^{-1}y)=(x+x^{-1})(y+y^{-1})$, which is RCL after the usual $J$-normalization $J(x)=\tfrac12(x+x^{-1})-1$. It therefore sits on the Cost side of the forcing chain that underwrites T5 $J$-uniqueness, where $J(x)=\cosh(\log x)-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.