diagSL_trace
plain-language theorem explainer
The trace of the diagonal area-preserving matrix with eigenvalues x and x inverse equals x plus x inverse. Anyone reducing the calibrated symplectic cost on the split torus to the canonical recognition cost J cites this identity, as does the scalar restriction of the SL(2) trace identity. The proof is a one-line simplification that unfolds the matrix definition and the two-by-two trace formula.
Claim. For every real number $x$, the matrix $\mathrm{diag}(x, x^{-1})$ has trace $x + x^{-1}$.
background
In the symplectic-ledger picture, a recognition event is a linear map of the two-dimensional debit-credit phase space. Area preservation (equivalently $\sigma = 0$) forces the map into $\mathrm{SL}(2,\mathbb{R}) = \mathrm{Sp}(2,\mathbb{R})$. The diagonal family $\mathrm{diag}(x, x^{-1})$ is the split-torus subgroup of that group: each element is area-preserving with reciprocal eigenvalues.
The module identifies the recognition cost of an event with the calibrated trace functional $\tfrac12,\mathrm{tr},M - 1$. Evaluating that functional on the split torus requires the ordinary matrix trace of $\mathrm{diag}(x, x^{-1})$, which is exactly this lemma.
The ambient derivation of $J$ from the Recognition Composition Law is already complete elsewhere; this module supplies an independent variational reading of the same $J$ as symplectic action on the ledger.
proof idea
One-line wrapper: simp unfolds the definition of the diagonal matrix $\mathrm{diag}(x, x^{-1})$ and applies the standard two-by-two matrix-trace identity (sum of the diagonal entries). No further algebraic work is required.
why it matters
This identity is the computational hinge that turns the abstract calibrated-trace cost into the canonical recognition cost $J$ on the split torus: the downstream result traceCost_diagSL rewrites the symplectic action cost as $J$ by invoking this trace evaluation. It is also the rewrite step inside split_torus_trace_identity, the scalar form of the SL(2) trace identity on diagonal elements, obtained by restricting $\mathrm{tr}(AB)+\mathrm{tr}(AB^{-1})=\mathrm{tr}(A),\mathrm{tr}(B)$ to the split torus.
Together these steps discharge the documented bridge that identifies $J(x)=\tfrac12(x+x^{-1})-1$ with a physical action, connecting T5 J-uniqueness and the RCL to a ledger-forced variational principle. The lemma itself is local to the cost-as-action bridge; the eight-tick and $D=3$ forcing sit further upstream in the chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.