split_torus_trace_identity
plain-language theorem explainer
For real x and nonzero y, the scalar identity (xy + x⁻¹y⁻¹) + (xy⁻¹ + x⁻¹y) = (x + x⁻¹)(y + y⁻¹) holds. It is the split-torus (diagonal) restriction of the SL(2) Fricke trace identity on area-preserving ledger maps. Anyone deriving the Recognition Composition Law from symplectic action cites this bridge. The proof instantiates the matrix trace identity on diag(x,x⁻¹) and diag(y,y⁻¹), then simplifies the traces.
Claim. For all real $x$ and all $y \neq 0$, $$(xy + x^{-1}y^{-1}) + (xy^{-1} + x^{-1}y) = (x + x^{-1})(y + y^{-1}).$$
background
In this module the double-entry ledger is a two-dimensional phase space. A recognition event is a linear map $M:\mathbb{R}^2\to\mathbb{R}^2$. The $\sigma=0$ law (no net imbalance) is area preservation for the form $\omega(v,w)=v_0 w_1-v_1 w_0$, hence $\det M=1$, i.e. $M\in\mathrm{SL}(2,\mathbb{R})$. The calibrated cost of an event is the trace functional $\tfrac12\mathrm{tr},M-1$, which vanishes on the identity.
Cayley–Hamilton in two dimensions yields the SL(2) trace identity: when $B$ conserves $\sigma$ (so $B^{-1}$ exists and equals the adjugate), $\mathrm{tr}(AB)+\mathrm{tr}(AB^{-1})=\mathrm{tr} A\cdot\mathrm{tr} B$. The split-torus elements are the diagonal area-preserving maps $\mathrm{diag}(x,x^{-1})$ with $x\neq 0$; their traces are simply $x+x^{-1}$.
The present identity is that matrix identity restricted to a pair of such diagonal events. Upstream, the general matrix form is already proved, and the diagonal multiplication and inverse-trace formulas are available as simplifications.
proof idea
Term-mode proof. Instantiate the general SL(2) trace identity on the two diagonal matrices $\mathrm{diag}(x,x^{-1})$ and $\mathrm{diag}(y,y^{-1})$, using that the second conserves $\sigma$ whenever $y\neq 0$. Rewrite the two product traces via the diagonal multiplication and inverse-trace lemmas, which expand them to $xy+x^{-1}y^{-1}$ and $xy^{-1}+x^{-1}y$. Simplify the remaining traces with the one-line diagonal-trace formula $x+x^{-1}$. The resulting scalar equality is exactly the claim.
why it matters
This is the algebraic hinge between the symplectic ledger and the Recognition Composition Law. Downstream, rcl_from_symplectic_action quotes the identity as its key step and rewrites both sides in terms of the calibrated cost $J(z)=\tfrac12(z+z^{-1})-1$, obtaining
$J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$.
In the broader framework the RCL was previously a stated primitive that, with reciprocity and continuity, forces $J(x)=\cosh(\log x)-1$ (T5 J-uniqueness). Here the RCL itself is discharged as the Fricke/SL(2) trace identity specialized to the split torus of area-preserving ledger maps. That closes the bridge from the $\sigma=0$ variational principle to the cost functional used throughout the forcing chain, without treating composition as an extra axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.