conservesSigma_iff_defect_zero
plain-language theorem explainer
For a real 2×2 ledger map M, σ-conservation is exactly vanishing of the area defect det M − 1. Anyone citing the symplectic-ledger bridge (σ = 0 as area preservation) uses this equivalence. The proof unfolds the two definitions and closes both directions by linear arithmetic.
Claim. For every real $2\times 2$ matrix $M$, $M$ is $\sigma$-conserving (equivalently $\det M = 1$) if and only if its $\sigma$ area defect vanishes: $\det M - 1 = 0$.
background
In this module a double-entry ledger is 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) is identified with preservation of the ledger area form $\omega(v,w)=v_0 w_1-v_1 w_0$. For $2\times 2$ maps that is exactly $\det M=1$, i.e. membership in $\mathrm{SL}(2,\mathbb{R})=\mathrm{Sp}(2,\mathbb{R})$.
Two local definitions package that geometry. $\sigma$-conservation is the proposition $\det M=1$. The $\sigma$ area defect is the real number $\det M-1$. The module’s larger program then lifts area preservation to the SL(2) trace identity and the calibrated trace cost that recovers the forced $J$-cost from the Recognition Composition Law.
proof idea
One short tactic proof. Unfold both sides of the biconditional to $\det M=1$ and $\det M-1=0$. Split into the two directions; each direction is a single linarith step on the unfolded equalities. No external lemmas are required beyond the definitions.
why it matters
This is the first link in the module’s chain that turns $\sigma=0$ into symplectic geometry: $\sigma$-conservation $\Leftrightarrow$ area defect zero, and (by the sibling) $\Leftrightarrow$ area-form preservation $\Leftrightarrow$ $\det=1$. The module doc states the physical principle explicitly: “the symplectic ledger is not an extra assumption; it is the content of $\sigma=0$.”
Downstream the same chain yields the SL(2) trace identity $\mathrm{tr}(AB)+\mathrm{tr}(AB^{-1})=\mathrm{tr}(A),\mathrm{tr}(B)$ and the calibrated trace cost $\tfrac12\mathrm{tr} M-1$, which matches the uniquely forced $J(x)=\tfrac12(x+x^{-1})-1$ from RCL (T5). That discharges the documented bridge from the functional equation to a physical variational principle. No used_by edges are recorded yet; the immediate consumers are the sibling equivalences and the trace-identity lemmas in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.