pairForm
plain-language theorem explainer
Defines the signed area (skew pairing) on the two-dimensional debit–credit fiber of a seam ledger: ω(u,v) = u₀v₁ − u₁v₀. Anyone proving double-entry conservation for a transfer matrix W cites this as the invariant that W must preserve. The body is a one-line bilinear expression, the standard 2×2 determinant pairing.
Claim. For vectors $u,v\in\mathbb{R}^2$, the double-entry pairing is $\omega(u,v)=u_0 v_1-u_1 v_0$, the signed area of the parallelogram they span on the (debit, credit) pair fiber.
background
SeamTransferCore treats a seam crossing as a linear transfer $W$ acting on a two-dimensional pair fiber whose coordinates are the debit and credit legs of a double-entry posting. The module's panel program is that the per-closure recognition cost is the character anomaly $C=\mathrm{Tr}(W)/2-1$ of a balanced transfer, and that this equals the T5 cost $J(x)$ once balance and a delivered eigenvalue $x$ are imposed.
The pairing form is the ledger's conservation object: a posting and its counter-posting span an oriented area, and double-entry says one closure cannot create or destroy that area. In matrix language, conservation is $\omega(Wu,Wv)=\omega(u,v)$ for all $u,v$, which is equivalent to $\det W=1$ (the 2d symplectic identity). Balance is therefore not an extra modeling choice; it is preservation of this form.
Sibling material in the module then derives the reciprocal eigenvalue and the forced trace $\mathrm{Tr},W=x+x^{-1}$ from $\det W=1$ plus one real eigenvalue, so $J$ emerges rather than being posited.
proof idea
Pure definition: the body is the alternating bilinear expression $u,0\cdot v,1-u,1\cdot v,0$ on $\mathrm{Fin},2\to\mathbb{R}$. No lemmas are applied. Downstream proofs treat preservation of this form as the conservation hypothesis and convert it to unit determinant via the sibling equivalence with $\det W=1$.
why it matters
This is the structural invariant that makes the circularity fence work in LEG-B Phase B: reciprocity and $J$ are derived from conservation of the pairing plus a delivered leg, never from writing $W=\mathrm{diag}(x,x^{-1})$ by hand.
Downstream, SeamLedgerDischarge builds the audit lemmas on it. conserving_trace_eq, conserving_trace_ge_two, conserving_trace_eq_two_iff, and the bundled conserving_trace_bound all take $\forall u,v,,\omega(Wu,Wv)=\omega(u,v)$ as the conservation premise and conclude $\mathrm{Tr},W=x+x^{-1}\ge 2$ with equality iff $x=1$. Load-bearing theorems calibration_is_load_bearing and faithfulness_is_load_bearing quantify over transfers that preserve the pairing. Ledger-closure pricing objects read costs off the same conserved structure.
In framework terms it is the 2d avatar of double-entry balance that forces the T5 cost $J(x)=(x+x^{-1})/2-1$ once the character anomaly is read from the trace.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.