HasRealEigen
plain-language theorem explainer
A 2×2 real matrix W has real eigenvalue x when some nonzero fiber vector is scaled by x under one seam closure. This is the delivered-leg predicate only: the crossing delivers mismatch ratio x per unit required, with no assumption on the conjugate leg. Downstream seam-ledger and horizon-clock results cite it as the typed reading of hyperbolic mismatch. The body is the standard eigenvector existence statement.
Claim. For a real $2\times 2$ matrix $W$ and a real number $x$, $W$ has real eigenvalue $x$ if there exists a nonzero vector $v\in\mathbb{R}^{2}$ such that $W v = x v$. On the seam this means the delivered leg scales by the mismatch ratio $x$ under one closure; nothing is assumed about the other leg.
background
SeamTransferCore implements the panel's Scale-Holonomy Trace Core (Phase B): the per-closure recognition cost of a seam crossing at mismatch ratio $x$ is the character anomaly $C=\mathrm{Tr}(W)/2-1$ of the transfer $W$ induced on the seam's double-entry pair fiber.
The standing guardrail is never to posit $W=\mathrm{diag}(x,x^{-1})$ (that would smuggle in the T5 cost $J$). Only the delivered-leg scaling by $x$ is assumed; balance ($\det W=1$) then forces the conjugate eigenvalue $x^{-1}$ and the trace identity $\mathrm{Tr},W=x+x^{-1}$, so the character anomaly equals $J(x)=(x+x^{-1})/2-1$.
This definition is the pure scaling half of that program: an ordinary real-eigenvalue predicate on the $2\times 2$ fiber, with no determinant or conjugacy-class content. Downstream, HyperbolicMismatchClass strengthens it by $x>0$ and $x\neq 1$ to mark genuine hyperbolic mismatch.
proof idea
Definitional, not a proof. The body is the standard eigenvector clause: existence of a nonzero $v:\mathrm{Fin},2\to\mathbb{R}$ with $W\cdot v=x\cdot v$. No lemmas are applied; siblings such as balanced_conjugate, balanced_trace, and charAnomaly_eq_J consume this predicate together with $\det W=1$.
why it matters
This is the typed delivered-leg atom for the seam program. HorizonClockRate packages it as HyperbolicMismatchClass (real eigenvalue, positive, not unit), grounding the hyperbolic mismatch reading against the elliptic class that cannot carry genuine $x\neq\pm 1$.
SeamLedgerDischarge uses it throughout the conserving-trace chain: pairing conservation plus a real eigenvalue $x>0$ yields $\mathrm{Tr},W=x+x^{-1}\ge 2$ with equality iff $x=1$ (conserving_trace_eq, conserving_trace_bound, conserving_trace_eq_two_iff). Calibration and faithfulness load-bearing theorems quantify over transfers that satisfy this predicate at the turn ratio. That is how the T5 cost $J$ emerges from algebra (balance + one eigenvalue) rather than being named in the inputs, and how CensusPricing reduces to checkable seam structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.