conservesSigma_iff_preservesArea
plain-language theorem explainer
A real 2×2 matrix conserves ledger σ (determinant one) exactly when it preserves the debit-credit area form on every pair of vectors. Anyone identifying σ = 0 with the symplectic group SL(2,ℝ) cites this equivalence. The proof is a short two-direction argument: one side multiplies area by det via the scaling lemma; the converse evaluates on the standard basis pair.
Claim. For every real $2\times 2$ matrix $M$, $\det M = 1$ if and only if $M$ preserves the ledger area form: $\omega(Mv, Mw) = \omega(v,w)$ for all $v,w \in \mathbb{R}^2$, where $\omega(v,w) = v_0 w_1 - v_1 w_0$.
background
In this module a double-entry ledger is a two-dimensional phase space: a state is a pair (debit, credit) in $\mathbb{R}^2$, and a recognition event is a linear map $M$ of that space. The ledger symplectic area form is $\omega(v,w) = v_0 w_1 - v_1 w_0$.
σ-conservation of an event is defined as $\det M = 1$. The module's aim is to discharge the bridge from the Recognition Composition Law (which forces the cost $J$) to a physical variational principle: on area-preserving maps, Cayley–Hamilton yields the SL(2) trace identity, and the calibrated half-trace is $J$.
The decisive upstream fact is the scaling law: a linear ledger map multiplies the area form by its determinant, $\omega(Mv, Mw) = (\det M),\omega(v,w)$.
proof idea
Unfold σ-conservation to $\det M = 1$ and split both ways. Forward: rewrite the transformed area via the scaling identity $\omega(Mv,Mw) = (\det M),\omega(v,w)$ and cancel with $\det M = 1$. Backward: feed the standard basis pair $e_0 = (1,0)$, $e_1 = (0,1)$ into the assumed area-preservation identity; the base area $\omega(e_0,e_1) = 1$ together with the scaling identity forces $\det M = 1$.
why it matters
This is the geometric content of σ = 0: no net imbalance is exactly area preservation, hence membership in $\mathrm{SL}(2,\mathbb{R}) = \mathrm{Sp}(2,\mathbb{R})$. The module doc lists it as the first step that makes the symplectic ledger the content of σ = 0 rather than an extra assumption.
It is wired into the symplectic-action certificate as the field sigma_zero_iff_area_preserving, which packages the full derivation of $J$ from the ledger variational principle (trace identity, half-trace cost, and RCL recovered as the SL(2) identity). It is also cited by the Gap-5 chart verdict that links ledger momentum to gravity chart structure. Together with the later Cayley–Hamilton and trace-identity lemmas it underwrites the physical identification of the RCL-forced cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.