eigen_char
plain-language theorem explainer
Any real eigenvalue x of a 2×2 real matrix W is a root of the characteristic polynomial x² − (tr W)x + det W = 0. Seam-transfer and holography arguments cite this as the algebraic bridge from a delivered-leg scaling to trace and determinant constraints. The proof extracts a nonzero kernel vector for W − xI, forces the determinant to vanish, and rewrites via the 2×2 expansion of det(W − xI).
Claim. Let $W$ be a $2\times 2$ real matrix and $x\in\mathbb{R}$. If $W$ has real eigenvalue $x$ (some nonzero $v\in\mathbb{R}^2$ with $Wv=xv$), then $x$ is a root of the characteristic polynomial: $x^2-(\operatorname{tr} W)\,x+\det W=0$.
background
SeamTransferCore treats the holonomy of one seam closure as a linear transfer $W$ on the double-entry pair fiber $\mathbb{R}^2$. The delivered leg of a mismatch is encoded purely as a real eigenvalue: there exists nonzero $v$ with $Wv=xv$, with no assumption on the conjugate leg. That is the only scaling input.
The module's program is to force the T5 cost $J$ from balance alone. Balance means $\det W=1$ (double-entry conservation). Once a real eigenvalue $x\neq 0$ is given, the characteristic identity $x^2-(\operatorname{tr} W)x+\det W=0$ becomes the algebraic lever that produces the reciprocal eigenvalue and the forced trace $x+x^{-1}$.
Locally this lemma is the Cayley–Hamilton bookkeeping step for $2\times 2$ matrices: eigenvalues are roots of $\lambda^2-(\operatorname{tr})\lambda+\det$. The sibling expansion of $\det(W-xI)$ is used to match that monic polynomial exactly.
proof idea
Unpack the eigenvalue hypothesis to a nonzero $v$ with $Wv=xv$. Rewrite as $(W-xI)v=0$ by distributing mulVec over subtraction and scalar action on the identity. Nontrivial kernel implies $\det(W-xI)=0$ via the standard exists-mulVec-eq-zero criterion. Substitute the in-module identity that expands $\det(W-x\cdot 1)$ to $x^2-(\operatorname{tr} W)x+\det W$, and conclude. Pure $2\times 2$ linear algebra; no Recognition-specific hypotheses enter.
why it matters
This is the characteristic-polynomial hinge for the panel's Phase B circularity fence. Downstream, balanced_trace applies it under $\det W=1$ and $x\neq 0$ to obtain $\operatorname{tr} W=x+x^{-1}$ by field simplification: the reciprocal leg is derived, not posited. That forces the character anomaly $\operatorname{tr}(W)/2-1$ to equal $J(x)$, so the T5 cost emerges from determinant balance plus one delivered eigenvalue.
It is also reused by elliptic_no_real_mismatch: on a rotation transfer the same identity plus $\det=1$ and trace $2\cos\theta$ shows no real eigenvalue exists except $\pm 1$. Genuine mismatch ratios therefore cannot live on the elliptic conjugacy class, explaining why phase-branch pricing was structurally impossible.
Together these close the per-closure half of SeamTransferPricing: census cost reduces to a checkable trace reading on a balanced pair-fiber transfer, without naming $J$ in the inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.