trace_diagSL_mul_inv
plain-language theorem explainer
On the split torus of SL(2,ℝ), the trace of diag(x,x⁻¹) times the inverse of diag(y,y⁻¹) equals x/y + y/x whenever y ≠ 0. Specialists reducing the Fricke/SL(2) identity to diagonal ledger events cite this evaluation. The proof rewrites the inverse as the adjugate (det = 1) and expands the 2×2 matrices.
Claim. For all real $x$ and $y \neq 0$, writing $D(t) = \mathrm{diag}(t, t^{-1})$ for the diagonal area-preserving matrix, one has $\mathrm{tr}\bigl(D(x)\, D(y)^{-1}\bigr) = x y^{-1} + x^{-1} y$.
background
This module treats recognition events as linear maps of the double-entry ledger phase space ℝ². The σ = 0 law (no net imbalance) is area preservation for the form ω(v,w) = v₀w₁ − v₁w₀, hence det = 1: events live in SL(2,ℝ) = Sp(2,ℝ).
The diagonal (split-torus) element is D(t) = diag(t, t⁻¹). Whenever t ≠ 0 it has determinant 1, so it is area-preserving. The upstream SL(2) trace identity states that for any matrix A and any area-preserving B, tr(A B) + tr(A B⁻¹) = tr(A) tr(B) (the Fricke identity). Restricting both arguments to the split torus needs explicit scalar evaluations of those two traces.
The companion product-trace evaluation and the present inverse-trace evaluation are the two ingredients of that restriction.
proof idea
First apply the determinant lemma for the diagonal embedding: det D(y) = 1. On SL(2), the inverse equals the adjugate, so rewrite D(y)⁻¹ as adj D(y) via the matrix inverse definition. Then unfold the diagonal embedding, the 2×2 adjugate formula, and the 2×2 trace: the product is diagonal with entries x y⁻¹ and x⁻¹ y, and the trace is their sum. Pure algebraic expansion; no induction or analysis.
why it matters
This is the inverse half of the diagonal specialization of the Fricke/SL(2) identity. The sole downstream consumer is the scalar split-torus trace identity, which combines the product-trace and inverse-trace evaluations to obtain (x y + x⁻¹ y⁻¹) + (x y⁻¹ + x⁻¹ y) = (x + x⁻¹)(y + y⁻¹).
That algebraic skeleton is the Recognition Composition Law restricted to the split torus, and is the bridge from the symplectic ledger principle to the calibrated cost J(x) = ½(x + x⁻¹) − 1. In the forcing chain this feeds T5 (J-uniqueness). Without the inverse-trace evaluation, the diagonal restriction of the SL(2) identity cannot close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.