sigmaAreaDefect
plain-language theorem explainer
The σ area defect of a 2×2 real matrix is its determinant minus one. It quantifies how far a ledger event map fails area preservation (equivalently, σ = 0 balance). Anyone citing the symplectic-ledger bridge or ConservesSigma equivalences needs this scalar. The body is a one-line arithmetic definition on det.
Claim. For a real $2\times 2$ matrix $M$, the $\sigma$ area defect is $\det M - 1$.
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$. A recognition event is a linear map $M:\mathbb{R}^2\to\mathbb{R}^2$. The $\sigma=0$ conservation law (no net imbalance) is geometrically area preservation for the symplectic 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. $M\in\mathrm{SL}(2,\mathbb{R})=\mathrm{Sp}(2,\mathbb{R})$.
The module's aim is to identify the recognition cost $J(x)=\tfrac12(x+x^{-1})-1$ with a calibrated trace functional on this area-preserving group, discharging the bridge from the Recognition Composition Law to a physical variational principle. The scalar defined here is the elementary obstruction to that group membership: how far $\det M$ sits from $1$.
proof idea
Pure definition: evaluate the determinant of the $2\times 2$ real matrix and subtract one. No lemmas, no tactics.
why it matters
This defect is the quantitative face of $\sigma$ imbalance. The immediate parent is conservesSigma_iff_defect_zero, which states that a ledger event conserves $\sigma$ if and only if the defect vanishes, and the module doc ties that equivalence to area preservation (conservesSigma_iff_preservesArea): $\sigma=0$ iff area-preserving iff $\det=1$.
That identification is the geometric half of the module's bridge: once events live in $\mathrm{SL}(2,\mathbb{R})$, Cayley–Hamilton yields the SL(2) trace identity, and the calibrated trace cost $\tfrac12\mathrm{tr},M-1$ recovers $J$. The defect is therefore the gatekeeper scalar between raw ledger maps and the forced cost that matches T5 J-uniqueness and the RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.