hyperbolicWitness_det
plain-language theorem explainer
For any nonzero real ratio $x$, the diagonal hyperbolic witness $\mathrm{diag}(x,x^{-1})$ has determinant $1$. Downstream non-vacuity proofs for seam-transfer and ledger-closure pricing cite this to inhabit the balanced-transfer premise without naming $J$. The argument unfolds the matrix, applies the $2\times 2$ determinant formula, and cancels $x\cdot x^{-1}$.
Claim. For every real number $x \neq 0$, if $W = \mathrm{diag}(x, x^{-1})$ denotes the $2 \times 2$ hyperbolic witness matrix, then $\det W = 1$.
background
SeamTransferCore implements the panel's Phase B claim: 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. Balance means $\det W = 1$; the delivered leg is a real eigenvalue $x \neq 0$. From those two inputs alone, the conjugate eigenvalue is forced to $x^{-1}$ and the trace to $x + x^{-1}$, so the anomaly equals the T5 cost $J(x) = (x + x^{-1})/2 - 1$.
The hyperbolic witness is explicitly $\mathrm{diag}(x, x^{-1})$. Module documentation stresses it is a non-vacuity witness only, not the physical construction: "the physical claim is that the SEAM's transfer inhabits it." The circularity fence forbids positing $W = \mathrm{diag}(x,x^{-1})$ as the seam map; reciprocity must be derived from $\det = 1$ and one real eigenvalue.
This lemma records the elementary fact that the witness itself is balanced whenever $x \neq 0$.
proof idea
Unfold the definition of the hyperbolic witness to the concrete matrix $!![x, 0; 0, x^{-1}]$. Rewrite the determinant via the standard $2\times 2$ formula $\det = ad - bc$, which here is $x \cdot x^{-1} - 0$. Cancel by $\mathrm{mul_inv_cancel}_0$ using the hypothesis $x \neq 0$, yielding $1$. Four-line tactic proof; no external RS lemmas beyond Mathlib matrix determinants.
why it matters
Without a balanced witness, every SeamTransferPricing and LedgerClosurePricing existence claim would be formally empty. Downstream non-vacuity theorems lean on this determinant identity: seamTransferPricing_turnRatioCost, ledgerClosurePricing_turnRatioCost, and ledgerClosurePricing_readingCost each invoke it to supply a unit-determinant matrix carrying the turn-ratio eigenvalue. The load-bearing calibration and faithfulness theorems in SeamLedgerDischarge sit in the same discharge stack.
In the forcing chain this supports the emergence of $J$ (T5) from balance plus one real eigenvalue, rather than from naming $J$ in the inputs. The module's reduction theorem censusPricing_of_seamTransfer then lifts structural seam facts (2d pair fiber, unit det, delivered-leg eigenvalue, trace reading) to CensusPricing. The physical identification of the seam's actual transfer remains open; this lemma only keeps the witness side inhabited.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.