diagSL
plain-language theorem explainer
Defines the diagonal split-torus element diag(x, x⁻¹) in Sp(2,ℝ): the canonical area-preserving recognition event with eigenvalue x. Anyone deriving the recognition cost J from the symplectic ledger cites this as the model event on which the calibrated trace equals J. The body is a one-line 2×2 matrix constructor.
Claim. For $x \in \mathbb{R}$, let $\mathrm{diag}_{\mathrm{SL}}(x) := \begin{pmatrix} x & 0 \\ 0 & x^{-1} \end{pmatrix}$. This is the diagonal element of the split torus in $\mathrm{Sp}(2,\mathbb{R}) = \mathrm{SL}(2,\mathbb{R})$, the area-preserving recognition event with eigenvalue $x$.
background
The module treats a double-entry ledger as a two-dimensional phase space: a state is a pair (debit, credit). A recognition event is a linear map $M:\mathbb{R}^2\to\mathbb{R}^2$. The $\sigma=0$ conservation law (no net imbalance) is area preservation for the symplectic form $\omega(v,w)=v_0 w_1-v_1 w_0$, which for $2\times 2$ maps is exactly $\det M=1$, i.e. $M\in\mathrm{SL}(2,\mathbb{R})=\mathrm{Sp}(2,\mathbb{R})$.
On that group, Cayley–Hamilton yields the SL(2) trace identity $\mathrm{tr}(AB)+\mathrm{tr}(AB^{-1})=\mathrm{tr}(A),\mathrm{tr}(B)$. The recognition cost of an event is the calibrated trace functional $\mathrm{traceCost},M=\tfrac12\mathrm{tr},M-1$, which vanishes on the identity (balanced ledger).
The diagonal matrices with reciprocal eigenvalues form the split torus inside $\mathrm{Sp}(2,\mathbb{R})$. They are the simplest nontrivial area-preserving events and the natural place to match the abstract cost $J$ to a physical action.
proof idea
Pure definition: the $2\times 2$ matrix with $x$ and $x^{-1}$ on the diagonal and zeros off-diagonal. No proof obligations. Downstream lemmas immediately compute its trace ($x+x^{-1}$), determinant ($1$ when $x\neq 0$), and membership in the $\sigma$-conserving class.
why it matters
This is the model recognition event on which the module identifies the symplectic action with the canonical cost $J$. Downstream, diagSL_trace and diagSL_det give $\mathrm{tr}=x+x^{-1}$ and $\det=1$; diagSL_conservesSigma places it in the area-preserving class; traceCost_diagSL proves $\mathrm{traceCost}(\mathrm{diag}_{\mathrm{SL}}(x))=J(x)$, so the calibrated trace on the split torus is exactly the RS cost forced by the Recognition Composition Law (T5 J-uniqueness).
The scalar restriction of the SL(2) trace identity becomes split_torus_trace_identity, recovering the RCL algebraically on eigenvalues. All of this is packaged in SymplecticActionCert, the certificate that $J$ is the symplectic action of the double-entry ledger. Without this diagonal generator, the bridge from ledger geometry to $J(x)=\tfrac12(x+x^{-1})-1$ (equivalently $\cosh(\log x)-1$) has no concrete carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.