hyperbolicWitness
plain-language theorem explainer
The diagonal matrix diag(x, x^{-1}) is the explicit hyperbolic witness that a balanced 2×2 transfer can deliver any nonzero real ratio x. Holography and ledger-discharge proofs cite it only for non-vacuity: the SeamTransferPricing and LedgerClosurePricing premises are inhabited. The body is a one-line matrix literal; balance and the eigenvalue x are proved in sibling lemmas.
Claim. For each real $x$, define the $2\times 2$ real matrix $W(x)=\mathrm{diag}(x,x^{-1})$. This is a pure witness object: it is balanced ($\det W=1$ when $x\neq 0$) and has real eigenvalue $x$, so the structural hypotheses of seam-transfer pricing are non-empty for every mismatch ratio.
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 transfer $W$ on the seam's double-entry pair fiber.
The panel guardrail (circularity fence) forbids treating $W=\mathrm{diag}(x,x^{-1})$ as the physical construction of the seam transfer. Balance ($\det W=1$) plus one real eigenvalue $x\neq 0$ already forces the conjugate eigenvalue $x^{-1}$ and the trace $x+x^{-1}$, so the anomaly equals the T5 cost $J(x)=(x+x^{-1})/2-1$ with $J$ nowhere in the inputs.
This definition supplies only an inhabiting family: for every ratio there exists some balanced matrix with that delivered leg. Downstream non-vacuity theorems plug it into LedgerClosurePricing and related discharge lemmas; the physical claim remains that the seam's actual transfer lies in that class.
proof idea
Definition, not a theorem. The body is the Mathlib matrix literal !![x, 0; 0, x⁻¹], i.e. the diagonal hyperbolic element of $\mathrm{SL}(2,\mathbb{R})$ (when $x\neq 0$). Sibling lemmas hyperbolicWitness_det and hyperbolicWitness_eigen discharge $\det=1$ and the eigenvalue claim by unfolding and simp/mul_inv_cancel₀.
why it matters
Without an explicit witness, the weak premises of seam and ledger pricing could be vacuous. Downstream, ledgerClosurePricing_turnRatioCost and ledgerClosurePricing_readingCost cite this family to show every TraceReading (including the anomaly reading) is realized by an induced cost of the form $f(x+x^{-1})$. Load-bearing checks calibration_is_load_bearing and faithfulness_is_load_bearing, and the B2 uniqueness route b2_unique_zero_of_anomalyLedger, sit on that inhabited chain.
In the framework this is the hyperbolic conjugacy class that carries genuine mismatch ratios; the elliptic (rotation) class cannot, which is the landed phase-branch poison. The witness underwrites the reduction from CensusPricing (which names $J$) to SeamTransferPricing (determinant, eigenvalue, trace reading only), tying the per-closure half of the panel program to T5 $J$-uniqueness without smuggling $J$ into the hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.