balanced_trace
plain-language theorem explainer
A balanced 2×2 real transfer with determinant 1 and a nonzero real eigenvalue x has trace exactly x + x^{-1}. Seam-ledger and holography arguments cite this to read the character anomaly off a delivered mismatch without positing a diagonal form. The proof is a short Cayley–Hamilton reduction: the 2×2 characteristic identity, det = 1, and field clearing force the trace by linear arithmetic.
Claim. Let $W$ be a $2\times 2$ real matrix with $\det W = 1$. If $x \neq 0$ is a real eigenvalue of $W$ (there exists a nonzero vector $v$ with $Wv = xv$), then $\operatorname{tr} W = x + x^{-1}$.
background
SeamTransferCore studies the transfer $W$ that one seam closure induces on the double-entry pair fiber (a $2\times 2$ real matrix). Balance means double-entry conservation, written here as $\det W = 1$. The delivered leg is the real-eigenvalue hypothesis: some nonzero fiber vector scales by the mismatch ratio $x\neq 0$ under one closure. No assumption is made about the other leg.
The character anomaly of a transfer is $\operatorname{Tr}(W)/2 - 1$, the conjugation-invariant scalar of the closure holonomy, normalized to vanish at the identity. The module program (panel Scale-Holonomy Trace Core, Phase B) is to force this anomaly to equal the T5 cost $J(x)=(x+x^{-1})/2-1$ without ever taking $W=\operatorname{diag}(x,x^{-1})$ as an input. The reciprocal must be derived from conservation, not posited.
proof idea
From the real-eigenvalue hypothesis, the sibling characteristic lemma supplies the $2\times 2$ Cayley–Hamilton relation: the eigenvalue satisfies $\lambda^2-(\operatorname{tr} W)\lambda+\det W=0$. Rewrite with $\det W=1$, clear the nonzero $x$ denominator by field simplification, and close by nonlinear arithmetic on the resulting polynomial identity. The reciprocal enters only as algebra on that identity.
why it matters
This is the forced-trace half of the circularity fence in SeamTransferCore: balance plus one delivered eigenvalue yield $\operatorname{Tr} W=x+x^{-1}$, so the character anomaly equals the T5 cost $J(x)$ with $J$ nowhere in the hypotheses (charAnomaly_eq_J). Downstream, balanced_conjugate reuses the trace to prove $x^{-1}$ is also an eigenvalue; conserving_trace_eq lifts the same conclusion from pair-form conservation (R2) via the det-one equivalence; and the ledger-discharge chain uses the $x+x^{-1}$ shape for AM–GM tightness at identity. Framework landmark: T5 $J$-uniqueness emerges from a unit determinant and a single real eigenvalue on the pair fiber.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.