traceCost_diagSL
plain-language theorem explainer
On the split torus of SL(2,ℝ), the calibrated trace functional of a diagonal area-preserving event equals the canonical recognition cost J. Anyone citing the symplectic derivation of J needs this identification. The proof unfolds both sides and rewrites by the elementary trace of diag(x, x⁻¹).
Claim. For every real $x$, the calibrated trace cost of the diagonal area-preserving matrix $\mathrm{diag}(x,x^{-1})$ equals the recognition cost $J(x)=\tfrac12(x+x^{-1})-1$.
background
The module treats a double-entry ledger as a 2D phase space (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$, hence $\det M=1$, i.e. $M\in\mathrm{SL}(2,\mathbb{R})=\mathrm{Sp}(2,\mathbb{R})$.
The calibrated trace functional on such an event is $\mathrm{traceCost}(M)=\tfrac12\mathrm{tr}(M)-1$, normalized to vanish on the identity (balanced ledger). The split-torus element is the diagonal map $\mathrm{diag}(x,x^{-1})$, which lies in $\mathrm{Sp}(2,\mathbb{R})$ for $x\neq 0$. Its ordinary matrix trace is $x+x^{-1}$.
The canonical recognition cost is $J(x)=\tfrac12(x+x^{-1})-1$, forced uniquely by the Recognition Composition Law together with reciprocity, normalization, calibration, and continuity. This lemma is the direct comparison of the two functionals on the split torus.
proof idea
Term-mode one-liner after unfolding. Expand $\mathrm{traceCost}$ and $J$ by definition, then rewrite the matrix trace via the simp lemma that $\mathrm{tr},\mathrm{diag}(x,x^{-1})=x+x^{-1}$. Both sides become $\tfrac12(x+x^{-1})-1$.
why it matters
This is the bridge that equates the physical symplectic action cost with the RS-native $J$. Downstream, symplecticActionCert packages it as the field recognition_cost_is_half_trace, together with the $\sigma=0\Leftrightarrow$ area-preservation equivalence, the SL(2) trace identity, and the derivation of the RCL from that identity. That certificate discharges the documented bridge from the functional-equation forcing of $J$ (T5 / RCL uniqueness) to a ledger-forced variational principle.
It is also cited in the SevenGaps chart analysis, where dropping linearity produces a monotone area-preserving coordinate in which cost is not quadratic, showing the chart is not forced without that hypothesis. Framework landmarks: T5 $J$-uniqueness, the RCL, and the identification $J(e^t)=\cosh t-1$ (Hamiltonian action minimized at the balanced ledger $t=0$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.