conserving_trace_eq
plain-language theorem explainer
A 2×2 real transfer that preserves the double-entry pairing and carries a positive real eigenvalue x must have trace exactly x + 1/x. Holography and seam-cost arguments cite this as the audit identity that turns ledger conservation plus a delivered leg into a scalar invariant. The proof is a one-line term: convert pairing preservation to det = 1, then apply the Cayley–Hamilton balanced-trace lemma.
Claim. Let $W$ be a $2\times 2$ real matrix and $x>0$. If $W$ preserves the double-entry pairing form (i.e. $\mathrm{pairForm}(Wu,Wv)=\mathrm{pairForm}(u,v)$ for all vectors $u,v$) and $x$ is a real eigenvalue of $W$, then $\mathrm{Tr}\,W = x + x^{-1}$.
background
This module types the R1–R4 residue of ConservingSeamPricing in weakest honest form and shows that the B2 uniqueness claim (deficit-free period $\beta=2\pi/\kappa$ is the unique zero of per-cycle seam cost) survives without loading the exact character-anomaly reading $\mathrm{Tr}(W)/2-1$.
The pairing form is the ledger double-entry bilinear form on $\mathbb{R}^2$. Conservation of that form under $W$ is the R2 sentence; by preserves_pairForm_iff_det_one it is exactly unimodularity $\det W=1$. R3 supplies a positive real eigenvalue $x$ (the delivered leg). The reciprocal $x^{-1}$ is not an extra hypothesis: it is forced by $\det=1$ and Cayley–Hamilton.
The identity $\mathrm{Tr},W=x+x^{-1}$ is the scalar audit invariant used throughout the discharge. Downstream bounds and zero-set arguments never reopen the matrix algebra; they only manipulate this trace.
proof idea
One-line term proof. Apply preserves_pairForm_iff_det_one (forward direction) to the pairing-conservation hypothesis, obtaining $\det W=1$. Pass $x\neq 0$ via ne_of_gt from $x>0$. Feed both facts plus the real-eigenvalue witness into balanced_trace, which is the Cayley–Hamilton identity for unimodular $2\times 2$ matrices: the second eigenvalue is forced to be $x^{-1}$, so the trace is $x+x^{-1}$.
why it matters
This is the R2+R3 force-the-trace step named in the module doc: the reciprocal leg is derived, never posited (the circularity fence). It is the algebraic engine under the key bundled lemma conserving_trace_bound ($\mathrm{Tr},W=x+x^{-1}\ge 2$, equality iff $x=1$), and under the siblings conserving_trace_ge_two and conserving_trace_eq_two_iff.
Those feed b2_unique_zero_of_ledgerClosure: for any calibrated faithful trace reading, off-period turn ratio gives trace strictly above 2, so faithfulness forbids a zero; at the period the trace is exactly 2 and calibration fires. Non-vacuity via ledgerClosurePricing_readingCost also rewrites costs through this identity on the hyperbolic witness family.
Framework role: the seam transfer is the holographic ledger map; the identity $x+x^{-1}$ is the same balanced combination that appears in the J-cost fixed-point structure (T5), though B2 discharge itself deliberately avoids naming $J$ or $\cosh$. Open elsewhere: B3 ($\kappa$ as horizon clock rate) and physical instantiation of LedgerClosurePricing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.