preserves_pairForm_iff_det_one
plain-language theorem explainer
A real 2×2 transfer preserves the double-entry pairing on the pair fiber exactly when its determinant is 1. Seam-transfer and census-pricing arguments cite this to turn ledger conservation into unimodularity, so SL(2,ℝ) is forced rather than assumed. The proof evaluates the form on the standard basis pair and uses the identity that the transformed pairing multiplies by det.
Claim. For every real $2\times 2$ matrix $W$, the following are equivalent: (i) $W$ preserves the double-entry pairing form, meaning $\mathrm{pairForm}(Wu,Wv)=\mathrm{pairForm}(u,v)$ for all $u,v\in\mathbb{R}^2$; (ii) $\det W=1$.
background
SeamTransferCore carries LEG-B Phase B of the Scale-Holonomy Trace Core: the per-closure recognition cost of a seam crossing is the character anomaly $C=\mathrm{Tr}(W)/2-1$ of the linear transfer $W$ that one closure induces on the seam's double-entry pair fiber (a real 2-plane of debit/credit legs).
The double-entry pairing form is the bilinear invariant that records ledger balance on that fiber. A transfer preserves the form when every pair of vectors keeps the same pairing after the map; that is the geometric sentence for double-entry conservation. The module's standing guardrail is never to posit $W=\mathrm{diag}(x,x^{-1})$: only a delivered-leg scaling and balance are allowed inputs, and reciprocity must be derived.
Upstream arithmetic supplies the unit multiplications used in the det identity. Downstream, conservation-plus-eigenvalue arguments convert this equivalence into $\mathrm{Tr},W=x+x^{-1}$ and thence into the T5 cost $J$.
proof idea
Bidirectional constructor on the biconditional.
Forward: instantiate preservation at the standard basis pair $e_0=[1,0]$, $e_1=[0,1]$. Unfolding shows their base pairing equals 1. The local map identity rewrites the transformed pairing as $\det(W)$ times the base pairing, so after mul_one one obtains $\det W=1$.
Reverse: for arbitrary $u,v$, the same map identity plus the hypothesis $\det W=1$ and one_mul restores equality of pairings. No spectral or positivity hypotheses appear; the argument is pure 2×2 multilinear algebra.
why it matters
This is the discharge of the balance premise: $\det=1$ is not a structural assumption about the seam, it is double-entry conservation restated. The panel's "why SL(2)?" question closes here: a pairing-preserving flow on a 2d real fiber has nowhere else to live (Sp(2,ℝ)=SL(2,ℝ) in this dimension).
Parent uses in SeamLedgerDischarge are load-bearing. conserving_trace_eq converts the conservation sentence into $\det=1$ via this theorem, then applies balanced_trace (Cayley–Hamilton) to force $\mathrm{Tr},W=x+x^{-1}$ with the reciprocal leg derived, never posited. Calibration and faithfulness load-bearing theorems, both ledger-closure pricing non-vacuity results, TraceReading, and b2_unique_zero_of_seamTransfer all thread the same conservation hypothesis through this equivalence.
In the forcing chain this sits under T5: once balance and a real eigenvalue $x\neq 0$ are in hand, the character anomaly equals $J(x)=(x+x^{-1})/2-1$, so the Recognition Composition Law cost emerges from ledger algebra alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.