trace_identity_of_conservesSigma
plain-language theorem explainer
When a 2×2 ledger map B preserves area (det B = 1), the Fricke/SL(2) identity holds: tr(AB) + tr(A B⁻¹) = tr(A)·tr(B). Anyone deriving the Recognition Composition Law from symplectic ledger geometry cites this. The proof rewrites the inverse as the adjugate under det = 1 and applies the unrestricted Cayley–Hamilton trace identity.
Claim. For real $2\times 2$ matrices $A,B$, if $B$ is $\sigma$-conserving (equivalently $\det B = 1$, so $B$ is area-preserving), then $\operatorname{tr}(AB) + \operatorname{tr}(A B^{-1}) = \operatorname{tr}(A)\,\operatorname{tr}(B)$.
background
In the symplectic-ledger picture, a recognition event is a linear map $M:\mathbb{R}^2\to\mathbb{R}^2$ on the double-entry phase space (debit, credit). The $\sigma=0$ law (no net imbalance) is area preservation for the 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})=\mathrm{Sp}(2,\mathbb{R})$. The predicate ConservesSigma packages that equality.
Cayley–Hamilton in two dimensions gives $B+\operatorname{adj} B=(\operatorname{tr} B),I$ for every $2\times 2$ matrix, and therefore the unrestricted identity $\operatorname{tr}(AB)+\operatorname{tr}(A,\operatorname{adj} B)=\operatorname{tr} A,\operatorname{tr} B$ (trace_mul_add_trace_mul_adjugate). When $\det B=1$, the inverse coincides with the adjugate, so the same identity becomes a statement about $B^{-1}$.
The module’s aim is to derive the recognition cost $J(x)=\tfrac12(x+x^{-1})-1$ and the Recognition Composition Law from this variational geometry rather than postulating RCL as a primitive.
proof idea
Tactic proof in three short steps. From ConservesSigma B read off $\det B=1$. Under that hypothesis, Matrix.inv_def plus simplification yields $B^{-1}=B.\mathrm{adjugate}$. Rewrite the goal with that equality, then apply the upstream lemma trace_mul_add_trace_mul_adjugate A B, which already proves $\operatorname{tr}(AB)+\operatorname{tr}(A,\operatorname{adj} B)=\operatorname{tr} A,\operatorname{tr} B$ for arbitrary $2\times 2$ real matrices via the ledger adjugate sum (Cayley–Hamilton).
why it matters
This is the SL(2) trace identity named in the module doc as the bridge from area-preserving ledger maps to the composition law for $J$. Downstream, split_torus_trace_identity restricts it to diagonal (split-torus) elements and obtains the scalar form $(xy+x^{-1}y^{-1})+(xy^{-1}+x^{-1}y)=(x+x^{-1})(y+y^{-1})$, which is the algebraic skeleton of RCL. The certificate symplecticActionCert records this theorem as its trace_identity field, tying $\sigma=0\Leftrightarrow$ area preservation, the calibrated half-trace cost, and the claim that RCL is the symplectic trace identity.
In the broader forcing chain this discharges the “documented bridge” that identifies $J$ with a physical cost: reciprocity $J(x)=J(1/x)$ becomes a theorem about symplectic spectra (eigenvalues in reciprocal pairs) rather than an assumption. It sits under T5 J-uniqueness and the RCL landmark, supplying the geometric reason those algebraic constraints appear.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.