hyperbolicWitness_eigen
plain-language theorem explainer
The hyperbolic witness matrix at ratio x has x as a real eigenvalue, with eigenvector the first standard basis vector. Non-vacuity proofs for seam-transfer and ledger-closure pricing cite this fact. The argument is a direct 2×2 eigenvector check: exhibit a nonzero fiber vector and simplify the matrix-vector product.
Claim. For every real $x$, the hyperbolic witness transfer $W(x)$ has real eigenvalue $x$: there exists a nonzero $v \in \mathbb{R}^2$ with $W(x)\,v = x\,v$.
background
SeamTransferCore implements LEG-B Phase B of the Scale-Holonomy Trace Core: the per-closure recognition cost of a seam crossing at mismatch ratio $x$ is the character anomaly $C = \mathrm{Tr}(W)/2 - 1$ of a balanced transfer $W$ on the double-entry pair fiber. The circularity fence forbids positing $W = \mathrm{diag}(x, x^{-1})$ as an assumption; only a delivered-leg scaling by $x$ is allowed, and the conjugate leg is derived from $\det W = 1$.
HasRealEigen formalizes that delivered-leg condition: some nonzero fiber vector scales by $x$ under one closure. Nothing about the other leg is assumed. The hyperbolic witness family is the concrete $2\times 2$ matrix used only as an existence witness for non-vacuity (never as the physical seam transfer). Upstream ledger notions of balance and reciprocity motivate why unit determinant means double-entry conservation, but this lemma itself is pure linear algebra on that witness.
proof idea
Term-style existence proof for the eigenvalue predicate. Exhibit the fiber vector $v = (1,0)$. Nonzeroness: if $v = 0$ then the $0$-component forces $1 = 0$ after congrFun and simp. The eigen-equation $W(x),v = x,v$ is checked componentwise by funext over Fin 2, with fin_cases and simplification of mulVec against the explicit witness matrix (two-term dot products on Fin 2). No external lemmas beyond matrix arithmetic.
why it matters
This is the delivered-leg half of the hyperbolic witness package. Downstream non-vacuity theorems build on it: seamTransferPricing_turnRatioCost packages the witness so turn-ratio cost is transfer-priced; ledgerClosurePricing_turnRatioCost and ledgerClosurePricing_readingCost inhabit the weak ledger-closure premise at every admissible trace reading; calibration_is_load_bearing and faithfulness_is_load_bearing use the same eigen-clause when showing those TraceReading conjuncts are necessary.
In the forcing chain this supports the reduction from CensusPricing (which names $J$) to SeamTransferPricing (which does not): a unit-determinant $2\times 2$ transfer plus one real eigenvalue forces $\mathrm{Tr}(W) = x + x^{-1}$ and hence the character anomaly equals the T5 cost $J(x) = (x + x^{-1})/2 - 1$. The physical identification of the seam's actual transfer remains open; the witness only closes existence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.