SeamTransferPricing
plain-language theorem explainer
A cost functional C(κ,T) is seam-transfer-priced when, for every positive curvature and period, some SL(2,ℝ) matrix on the seam's 2d double-entry fiber has the turn ratio as a real eigenvalue and C equals that matrix's character anomaly Tr(W)/2−1. Holography and TurnRatioCarrier authors cite it as the J-free structural premise that replaces CensusPricing. The body is a pure Prop definition, not a proved statement.
Claim. A bifunction $C:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ is seam-transfer-priced if for every $\kappa>0$ and $T>0$ there exists a $2\times 2$ real matrix $W$ with $\det W=1$, a real eigenvalue equal to the turn ratio $x=\kappa T/(2\pi)$, and $C(\kappa,T)$ equal to the character anomaly $\mathrm{Tr}(W)/2-1$ of $W$.
background
SeamTransferCore implements the panel's Phase-B decision: the per-closure recognition cost of a seam crossing is the character anomaly of the transfer that one closure induces on the seam's double-entry pair fiber. The standing guardrail is never to posit $W=\mathrm{diag}(x,x^{-1})$ up front (that would smuggle in the T5 cost $J$). Instead one assumes only a delivered-leg real eigenvalue $x$ and unit determinant; reciprocity and the trace identity are derived.
Character anomaly is $\mathrm{Tr}(W)/2-1$. Balance ($\det W=1$) plus a nonzero real eigenvalue $x$ forces the conjugate eigenvalue $x^{-1}$ (product of eigenvalues equals the determinant), and Cayley–Hamilton then forces $\mathrm{Tr} W=x+x^{-1}$, so the anomaly equals $J(x)=(x+x^{-1})/2-1$. The turn ratio $x=\kappa T/(2\pi)$ is the mismatch scale carried by TurnRatioCarrier.
This definition packages four checkable structural facts—2d fiber, unit determinant (double-entry conservation), delivered-leg eigenvalue, and trace reading—none of which names $J$. It is the typed premise meant to replace the older CensusPricing hypothesis that did name $J$.
proof idea
Definitional Prop, not a proof. The body quantifies over positive $\kappa,T$ and asserts existence of a matrix $W\in M_2(\mathbb{R})$ satisfying three conjuncts: $\det W=1$, real eigenvalue equal to the turn ratio of $(\kappa,T)$, and equality of $C(\kappa,T)$ with the character anomaly of $W$. No tactics or lemmas are invoked; downstream theorems discharge or consume the Prop.
why it matters
This is the J-free structural premise of the Phase-B reduction. The reduction theorem censusPricing_of_seamTransfer shows any such $C$ satisfies CensusPricing, by rewriting the cost as the anomaly and applying charAnomaly_eq_J (balance plus real eigenvalue forces anomaly $=J(x)$). Composing further yields b2_unique_zero_of_seamTransfer: the deficit-free period $\beta=2\pi/\kappa$ is the unique zero of any transfer-priced cost.
It feeds SeamTransferCoreCert (the bundled Phase-B certificate), the non-vacuity check seamTransferPricing_turnRatioCost (hyperbolic witness prices the turn-ratio cost), and the conserving-to-transfer bridge seamTransferPricing_of_conserving ($\mathrm{Sp}(2)=\mathrm{SL}(2)$). Framework landmark: T5 J-uniqueness emerges from algebra rather than being assumed—exactly the circularity fence the module is built to enforce. The physical identification of the seam's actual transfer remains open; only the pricing shape is fixed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.