pairForm_map
plain-language theorem explainer
A real 2×2 linear map multiplies the double-entry pairing of any two vectors by exactly its determinant. Anyone proving that pairing-preserving seam transfers are unimodular cites this identity. The proof is a direct expansion of the bilinear form against the 2×2 determinant formula, finished by ring.
Claim. For every real $2\times 2$ matrix $W$ and every pair of vectors $u,v\in\mathbb{R}^2$, the double-entry pairing form satisfies $\omega(Wu,Wv)=(\det W)\,\omega(u,v)$.
background
SeamTransferCore treats the seam as a 2d real pair fiber carrying a double-entry ledger. The pairing form $\omega$ on that fiber is the antisymmetric bilinear form that records the signed area of two posts (classically $u_1 v_2-u_2 v_1$). A linear transfer $W$ is the monodromy induced by one closure of the seam.
The module's panel brief is that the per-closure recognition cost is the character anomaly $\mathrm{Tr}(W)/2-1$ of a balanced transfer. Balance means $\det W=1$, so that the pairing is conserved rather than rescaled. Before that equivalence can be stated, one needs the exact scaling law for $\omega$ under arbitrary $W$.
This lemma is that scaling law: the classical 2d symplectic identity $\omega(Wu,Wv)=(\det W),\omega(u,v)$. It is pure linear algebra on $\mathrm{Fin},2$; no Recognition-specific hypothesis enters.
proof idea
Unfold the definition of the pairing form, then simplify with the standard expansions of matrix-vector multiplication, the two-term dot product on $\mathrm{Fin},2$, and the explicit $2\times 2$ determinant formula. The resulting polynomial identity in the eight entries of $W,u,v$ is discharged by ring. No external lemmas beyond Mathlib matrix primitives are required.
why it matters
This is the computational engine behind preserves_pairForm_iff_det_one, which equates pairing preservation with unimodularity: a transfer preserves $\omega$ for all vectors if and only if $\det W=1$. That theorem discharges the panel's balance premise as double-entry conservation rather than an extra structural assumption, closing the "why SL(2)?" question (in 2d real fibers, $\mathrm{Sp}(2,\mathbb{R})=\mathrm{SL}(2,\mathbb{R})$).
Downstream, balance plus a real eigenvalue $x\neq 0$ forces the conjugate eigenvalue $x^{-1}$ and the trace $x+x^{-1}$, so the character anomaly equals the T5 cost $J(x)$. The present identity is the first algebraic step of that chain: without the exact det-scaling of $\omega$, the iff with $\det=1$ does not open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.