diag_balanced_iff
plain-language theorem explainer
For a real diagonal 2×2 matrix, unit determinant is equivalent to the product of the two diagonal entries equaling one. Ledger and holography workers cite this when reading double-entry balance on diagonal seam transfers: the credit leg is the reciprocal of the debit leg exactly when the transfer is balanced. The proof rewrites the elementary 2×2 determinant and closes both directions by linear arithmetic.
Claim. For all real numbers $a$ and $b$, the diagonal matrix $\operatorname{diag}(a,b)$ satisfies $\det\operatorname{diag}(a,b)=1$ if and only if $a\,b=1$.
background
SeamTransferCore develops the panel's Phase-B claim that the per-closure recognition cost of a seam crossing is the character anomaly $C=\operatorname{Tr}(W)/2-1$ of a transfer $W$ acting on the seam's double-entry pair fiber. Balance means $\det W=1$: on the ledger, the two legs of one posting multiply to the identity.
The module's circularity fence forbids positing $W=\operatorname{diag}(x,x^{-1})$ up front. Only a delivered-leg scaling by $x$ is assumed; the conjugate $x^{-1}$ must be derived from unit determinant plus a real eigenvalue. On a diagonal transfer the two legs are exactly the diagonal entries, so the balance condition collapses to their product equaling one.
This elementary equivalence is the diagonal special case of that reciprocity reading. It sits beside the broader facts that a balanced transfer with real eigenvalue $x\neq 0$ has $x^{-1}$ as its other eigenvalue, and that the trace is then forced to $x+x^{-1}$, yielding the T5 cost $J(x)=\cosh(\log x)-1$.
proof idea
Rewrite the determinant via the standard Fin-2 formula: $\det\begin{pmatrix}a&0\0&b\end{pmatrix}=a b-0$. Split the biconditional. Each direction is immediate linear arithmetic on the equality $a b=1$.
why it matters
The declaration pins the ledger meaning of $\det=1$ on diagonal transfers: credit is the reciprocal of debit exactly when the posting is balanced. That reading is the first plank of the SeamTransferCore program (balance forces the reciprocal leg; reciprocity is conservation, not a modeling choice).
Downstream the same algebra yields the forced conjugate eigenvalue, the forced trace $x+x^{-1}$, and the identification of the character anomaly with the T5 J-cost, without ever naming $J$ in the inputs. The module then reduces CensusPricing to structural seam facts (2d pair fiber, unit determinant, delivered-leg eigenvalue, trace reading). The elliptic retrodiction later shows the rotation class cannot carry a genuine mismatch ratio at all.
No downstream uses are recorded yet; the lemma is local infrastructure for the diagonal case of the balance fence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.