seamTransferPricing_of_conserving
plain-language theorem explainer
Any cost functional priced by a pairing-conserving seam transfer is priced by a balanced (det = 1) seam transfer. The bridge is the classical identity that form-preserving linear maps on the 2d pair fiber are exactly SL(2). Downstream B2 discharge and census-pricing reductions cite this to drop the matrix determinant from the ledger premise while keeping the same conclusion.
Claim. If a cost $C:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ admits, for every $\kappa,T>0$, a $2\times 2$ real transfer $W$ that preserves the double-entry pairing form, has real eigenvalue equal to the turn ratio $x=\kappa T/(2\pi)$, and satisfies $C(\kappa,T)=\mathrm{Tr}(W)/2-1$, then the same data witness a balanced transfer: $\det W=1$, the same eigenvalue, and the same character-anomaly reading. In short, pairing conservation implies unit determinant on the pair fiber.
background
SeamTransferCore carries 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 transfer $W$ induced on the seam's double-entry pair fiber. The panel guardrail is never to posit $W=\mathrm{diag}(x,x^{-1})$; balance and one real eigenvalue force the reciprocal leg and the T5 cost $J(x)$.
ConservingSeamPricing is the ledger-facing premise: for each $(\kappa,T)$ there is a transfer that preserves the pairing form $\mathrm{pairForm}$, delivers the turn-ratio eigenvalue, and is read by the character anomaly. SeamTransferPricing is the same package with the conservation clause written as $\det W=1$. Both avoid naming $J$ in the inputs.
The classical fact used here is that on a 2-dimensional fiber, linear maps preserving the pairing form are exactly those of determinant one ($\mathrm{Sp}(2)=\mathrm{SL}(2)$). That equivalence is packaged as preserves_pairForm_iff_det_one.
proof idea
Term-mode, three steps. Introduce $\kappa,T$ and the positivity hypotheses. Unpack the conserving witness: a matrix $W$, form preservation, real eigenvalue at the turn ratio, and the character-anomaly equation for $C$. Re-pack the same $W$ for SeamTransferPricing, converting form preservation to $\det W=1$ by the forward direction of preserves_pairForm_iff_det_one; the eigenvalue and cost conjuncts pass through unchanged.
why it matters
This is the hinge that lets Phase B speak in pure ledger language. Downstream, b2_unique_zero_of_conserving composes it with the seam-transfer B2 theorem so that a pairing-conserving transfer prices the census by $J$ and forces the unique zero at the deficit-free period $\beta=2\pi/\kappa$, with "no $J$, no $\cosh$, no determinant, and no diagonal form anywhere in the premise."
censusPricing_of_anomalyLedger cites it (never re-proves it) in the chain anomaly-ledger $\to$ conserving $\to$ seam-transfer $\to$ CensusPricing. anomalyLedger_iff_conserving ties the landed anomaly reading to the conserving premise, so this bridge is on the critical path from ledger conservation to the B2 discharge.
Framework-wise it sits under the T5 J-uniqueness emergence: $J$ is not assumed; unit determinant plus one real eigenvalue force $\mathrm{Tr}(W)=x+x^{-1}$ and thus the character anomaly equals $J(x)$. Reciprocity is conservation, not a modeling choice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.