ledger_adjugate_sum
plain-language theorem explainer
For every real 2×2 matrix B, B plus its classical adjugate equals (tr B) times the identity. This is the ledger form of 2D Cayley–Hamilton and is the algebraic step that turns area-preserving ledger maps into a trace identity. Anyone deriving the recognition cost as a calibrated symplectic action on SL(2,ℝ) cites it. The proof is entrywise: expand the Fin-2 adjugate and trace formulas, then clear the four matrix entries by ring.
Claim. For every real $2\times 2$ matrix $B$, $$B + \operatorname{adj}(B) = (\operatorname{tr} B)\, I_2.$$ Equivalently, writing $B=\begin{pmatrix}a&b\\c&d\end{pmatrix}$, one has $B+\begin{pmatrix}d&-b\\-c&a\end{pmatrix}=(a+d)I_2$. No determinant hypothesis is required.
background
In this module a double-entry ledger is a two-dimensional phase space with states (debit, credit) ∈ ℝ². A recognition event is a linear map M: ℝ² → ℝ². The σ = 0 conservation law (no net imbalance) is geometrically area preservation for the symplectic form ω(v,w) = v₀w₁ − v₁w₀, which for 2×2 maps is exactly det M = 1, i.e. M ∈ SL(2,ℝ) = Sp(2,ℝ).
The classical adjugate of a 2×2 matrix is the cofactor transpose; for B = ((a,b),(c,d)) one has adj B = ((d,−b),(−c,a)), and B · adj B = (det B) I. Cayley–Hamilton in dimension two rearranges to the identity proved here: B + adj B = (tr B) I, with no invertibility assumption.
The module’s goal is to identify the recognition cost J(x) = ½(x + x⁻¹) − 1 with a calibrated trace functional on area-preserving ledger maps, discharging the bridge from the Recognition Composition Law to a physical variational principle.
proof idea
Term-mode proof by direct expansion. Rewrite with the Mathlib Fin-2 formulas for adjugate and trace, then use matrix extensionality. Case-split on the two row and column indices (four entries). On each entry, simp unfolds addition, scalar multiplication by the trace, the identity matrix, and the concrete adjugate components; ring finishes the arithmetic identity a + d = tr B on the diagonal and the off-diagonal cancellations.
why it matters
This is the first algebraic lemma in the symplectic-action derivation of J-cost. The immediate parent is trace_mul_add_trace_mul_adjugate: tr(A·B) + tr(A·adj B) = tr A · tr B for all 2×2 maps (pure Cayley–Hamilton, no det hypothesis). Specializing to det B = 1 replaces adj B by B⁻¹ and yields the SL(2) trace identity tr(A·B) + tr(A·B⁻¹) = tr A · tr B, from which the calibrated cost ½ tr M − 1 is forced on area-preserving events.
That cost is exactly the unique J forced by the Recognition Composition Law (T5 J-uniqueness: J(x) = (x + x⁻¹)/2 − 1). The module therefore closes the documented bridge from ledger σ = 0 geometry to the RCL cost, rather than treating J as a primitive number-system axiom alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.