traceCost
plain-language theorem explainer
Defines the calibrated trace functional on a 2×2 real matrix as half the trace minus one. It is the recognition action cost of a ledger event and vanishes at the identity (balanced σ = 0 ground state). Downstream work cites it to identify this functional with the canonical J-cost on the split torus. The body is a one-line arithmetic definition.
Claim. For a real $2\times 2$ matrix $M$, the calibrated recognition action cost is $\mathrm{traceCost}(M) := \tfrac{1}{2}\operatorname{tr}(M) - 1$. It vanishes when $M = I$ (the balanced ledger ground state).
background
In this module a double-entry ledger is 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 σ = 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})$.
The canonical recognition cost is $J(x)=\tfrac12(x+x^{-1})-1$, forced by the Recognition Composition Law together with reciprocity, normalization, calibration, and continuity. The module's bridge is to realize $J$ as a physical variational cost on the area-preserving group via the calibrated trace functional on ledger events.
On $\mathrm{SL}(2)$, Cayley–Hamilton yields the trace identity $\operatorname{tr}(AB)+\operatorname{tr}(AB^{-1})=\operatorname{tr}(A)\operatorname{tr}(B)$. The present definition supplies the cost side of that story: half-trace shifted so the identity has cost zero.
proof idea
Pure definition: evaluate half the matrix trace and subtract one. No lemmas, no tactics. Downstream traceCost_diagSL unfolds this definition against Cost.Jcost and rewrites via diagSL_trace to obtain equality on the split-torus diagonal embedding.
why it matters
This is the cost object in the symplectic-action bridge that discharges the documented identification of $J$ with a physical ledger cost. It is a field ingredient of SymplecticActionCert, whose doc states that the recognition cost $J$ is the symplectic action of the double-entry ledger: σ = 0 is area preservation, the area-preserving group satisfies the trace identity, the calibrated trace on the split torus is $J$, and the RCL is that identity.
The companion theorem traceCost_diagSL proves that on diagonal $\mathrm{SL}(2)$ matrices the functional equals $J(x)$, and thence $J(e^t)=\cosh t-1$ (cost as cosh of the generator's Hamiltonian action). That pins T5-style J-uniqueness to an independently physical variational principle rather than treating RCL as a bare primitive. Framework landmarks: RCL, $J(x)=\cosh(\log x)-1$, and the σ = 0 ground state.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.