diagSL_conservesSigma
plain-language theorem explainer
The diagonal ledger map with eigenvalues x and x⁻¹ preserves symplectic area whenever x ≠ 0, so it is a legitimate σ-conserving recognition event. Anyone working the split-torus reduction of the SL(2) trace identity cites this. The proof is a one-line appeal to the elementary determinant computation for that matrix.
Claim. For every real $x \neq 0$, the diagonal matrix $\mathrm{diag}(x, x^{-1})$ satisfies $\det = 1$, hence conserves ledger $\sigma$ (equivalently, preserves the area form on the debit-credit phase space).
background
In this module a double-entry ledger is a two-dimensional phase space with states (debit, credit). 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$. For $2\times 2$ maps that is exactly $\det M = 1$, written here as the predicate ConservesSigma.
The diagonal family diagSL $x$ is the split-torus element $\mathrm{diag}(x, x^{-1})$ inside $\mathrm{Sp}(2,\mathbb{R})$. It is the natural one-parameter subgroup on which the matrix SL(2) trace identity specialises to a scalar identity in the eigenvalues. The companion lemma diagSL_det already records $\det(\mathrm{diag}(x,x^{-1})) = x \cdot x^{-1} = 1$ for $x \neq 0$.
The broader setting identifies the calibrated trace functional $\tfrac12\mathrm{tr},M - 1$ with the recognition cost $J$, forced by the Recognition Composition Law together with reciprocity and normalisation.
proof idea
One-line term proof: ConservesSigma is definitionally $\det = 1$, so the claim is exactly the already-proved determinant identity for the diagonal matrix. Apply diagSL_det at the given $x \neq 0$; no further rewriting is required.
why it matters
This lemma licenses every later appeal to the split torus as a family of genuine $\sigma$-conserving events. Downstream, split_torus_trace_identity feeds diagSL $x$ and diagSL $y$ into the general SL(2) identity tr$(A B) + $tr$(A B^{-1}) = $tr$(A),$tr$(B)$ and obtains the scalar form
$(x y + x^{-1} y^{-1}) + (x y^{-1} + x^{-1} y) = (x + x^{-1})(y + y^{-1})$.
That scalar identity is the diagonal restriction of the ledger-forced trace law that underwrites the identification of $J$ with symplectic action. In the forcing chain it sits under the T5 uniqueness of $J(x) = \tfrac12(x + x^{-1}) - 1$ and the RCL, supplying the concrete geometric models on which the cost is evaluated. Without it the split-torus specialisation would be an extra hypothesis rather than a proved instance of $\sigma$-conservation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.