trace_inv_eq_of_det_one
plain-language theorem explainer
For any 2×2 real matrix W with determinant 1 and two-sided inverse V, the traces agree: Tr(V) = Tr(W). This is the matrix form of reciprocal symmetry for balanced seam transfers: the unoriented scalar cannot tell over-posting by x from under-posting by x⁻¹. Cited in the SeamTransferCore certificate chain toward forcing the character anomaly to equal J. Proof identifies V with the adjugate and expands the Fin-2 formulas.
Claim. Let $W,V$ be $2\times 2$ real matrices. If $\det W = 1$ and $WV = I$, then $\operatorname{Tr}(V) = \operatorname{Tr}(W)$.
background
SeamTransferCore implements LEG-B Phase B of the Scale-Holonomy Trace Core: the per-closure recognition cost of a seam crossing is the character anomaly $C = \operatorname{Tr}(W)/2 - 1$ of the transfer $W$ induced on the seam's double-entry pair fiber. Balance means unit determinant (double-entry conservation); the delivered leg carries a real eigenvalue (the mismatch ratio); the trace is the conjugation-invariant scalar read off that transfer.
The module's circularity fence forbids positing $W = \operatorname{diag}(x,x^{-1})$ up front. Instead one assumes only a delivered-leg eigenvalue $x \neq 0$ and $\det W = 1$; the conjugate eigenvalue $x^{-1}$ and the identity $\operatorname{Tr} W = x + x^{-1}$ are derived, so the anomaly equals the T5 cost $J(x) = (x+x^{-1})/2 - 1$ with $J$ nowhere in the inputs.
This lemma isolates the orientation-blind half of that story: once $V = W^{-1}$ and $\det W = 1$, the traces coincide. That is the ledger's column-swap symmetry written as a matrix identity, before eigenvalues enter.
proof idea
From $\det W = 1$, the identity $W \cdot \operatorname{adj}(W) = (\det W),I$ collapses to $W \cdot \operatorname{adj}(W) = I$. Commutativity of two-sided inverses gives $VW = I$. A short calc then shows $V = \operatorname{adj}(W)$: insert the adjugate factorization, reassociate, and cancel $VW$. Rewrite the goal under that equality, expand the explicit Fin-2 adjugate and both Fin-2 traces, and finish by ring arithmetic on the four entries.
why it matters
Doc-comment frames the result as "Reciprocity is orientation-blindness": the unoriented invariant of one closure cannot distinguish over-posting by $x$ from under-posting by $x^{-1}$. That is exactly the T5 reciprocal-symmetry hypothesis, supplied here by ledger column-swap rather than by an ansatz on $J$.
Downstream it is consumed by seamTransferCoreCert, the module certificate that packages conjugate forcing, anomaly-is-$J$, the CensusPricing reduction, and the elliptic retrodiction. Without trace reciprocity, the character anomaly would still depend on orientation of the transfer leg; with it, the scalar is forced to be the symmetric combination that becomes $J$ after balanced_trace and charAnomaly_eq_J.
In the broader RS chain this is a local algebraic step on the path from structural seam facts (2d fiber, unit det, delivered eigenvalue, trace reading) to the Recognition Composition Law cost, without naming $J$ in the premises.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.