ConservesSigma

In this module a double-entry ledger is treated as a two-dimensional phase space: a state is a debit–credit pair in $\mathbb{R}^2$, and a recognition event is a linear map $M:\mathbb{R}^2\to\mathbb{R}^2$. The $\sigma=0$ law (no net imbalance created) is identified with preservation of the ledger symplectic area form $\omega(v,w)=v_0 w_1-v_1 w_0$. For $2\times 2$ maps, area preservation is exactly $\det M=1$, i.e. membership in $\mathrm{SL}(2,\mathbb{R})=\mathrm{Sp}(2,\mathbb{R})$.

The module’s larger goal is to discharge the bridge that identifies the forced cost $J(x)=\tfrac12(x+x^{-1})-1$ with a physical variational principle on this area-preserving group. Upstream, the defect functional equals $J$ on positive reals; the present predicate simply names the geometric side of $\sigma=0$ so later lemmas can equate it with vanishing area defect and with the Fricke/SL(2) trace identity.

Definitional abbreviation: the predicate unfolds directly to the matrix determinant equaling one. No tactics or lemmas are applied.

This predicate is the common interface for the symplectic-action story. Downstream, conservesSigma_iff_defect_zero and conservesSigma_iff_preservesArea prove $\sigma=0$ iff the area defect vanishes iff the area form is preserved; trace_identity_of_conservesSigma obtains the SL(2) identity $\mathrm{tr}(AB)+\mathrm{tr}(AB^{-1})=\mathrm{tr}A,\mathrm{tr}B$ under the hypothesis, which specializes to the Recognition Composition Law; diagonal split-torus maps are shown to satisfy it; and SymplecticActionCert packages the whole chain that $J$ is the calibrated trace cost of the ledger. Gravity’s Gap-5 chart verdict also imports the same $\sigma\Leftrightarrow$ symplectic equivalence. Framework landmark: this is the geometric content of $\sigma=0$ that turns the RCL-forced $J$ into a ledger symplectic action (T5 J-uniqueness sits upstream of the cost side).