seamTransferCoreCert
plain-language theorem explainer
Bundles the Phase-B per-closure seam-transfer core into one certificate: balance forces the reciprocal eigenvalue, the character anomaly equals the T5 cost J, any balanced seam-transfer pricing implies CensusPricing, the elliptic branch is phase-cost and mismatch-dead, and the ledger pairing plus conservation identities hold. Cite this for the Scale-Holonomy Trace Core (panel 2026-07-05). The proof is a pure structure inhabitant wiring each field to its already-proved lemma.
Claim. There is a certificate establishing all of the following: any real $2\times 2$ matrix $W$ with $\det W=1$ and a real eigenvalue $x\neq 0$ also has eigenvalue $x^{-1}$; the character anomaly $\mathrm{Tr}(W)/2-1$ equals $J(x)$ whenever $x>0$ is a real eigenvalue of such a $W$; every cost functional priced by a balanced seam transfer satisfies CensusPricing; the character anomaly of a plane rotation equals phase cost, and a rotation admits no real eigenvalues other than $\pm 1$; $J(x)=(x-1)(1-x^{-1})/2$ for $x\neq 0$; and the balance/reciprocity conservation identities for the pair form hold.
background
This module is LEG-B Phase B of the Scale-Holonomy Trace Core. The panel decision fixes the per-closure recognition cost of a seam crossing at mismatch ratio $x$ as the character anomaly $C=\mathrm{Tr}(W)/2-1$ of the transfer $W$ that one closure induces on the seam's double-entry pair fiber (a real $2\times 2$ matrix). Double-entry balance means $\det W=1$. The delivered leg is assumed only to scale by $x$; the reciprocal leg is not posited.
The T5 cost is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). The character anomaly is defined as $\mathrm{Tr}(W)/2-1$. A real eigenvalue means $\det(W-xI)=0$. The elliptic class is the rotation family; its anomaly is the phase-cost object already shown sign-dead and lattice-blind in TurnRatioCarrier.
Upstream, balanced_conjugate derives the reciprocal eigenvalue from $\det=1$ alone (the circularity fence). charAnomaly_eq_J then obtains $J$ from Cayley-Hamilton plus balance. censusPricing_of_seamTransfer reduces the J-naming CensusPricing premise to SeamTransferPricing, which never names $J$.
proof idea
Term-mode structure inhabitant: each field of SeamTransferCoreCert is filled by the corresponding proved lemma. conjugate_forced is balanced_conjugate; anomaly_is_J is charAnomaly_eq_J; reduction is censusPricing_of_seamTransfer; elliptic_is_phaseCost is charAnomaly_rotation; elliptic_mismatch_dead is elliptic_no_real_mismatch; pairing_identity is Jcost_pairing; falsifier_discriminates is pricing_discriminated; balance_is_conservation is preserves_pairForm_iff_det_one; reciprocity_forced is trace_inv_eq_of_det_one. No new algebra is done at the certificate layer.
why it matters
This is the landed per-closure half of the Scale-Holonomy Trace Core (panel 2026-07-05, Phase B). It discharges the circularity fence: reciprocity is conservation ($\det=1$), not a modeling choice, so $J$ emerges from the algebra rather than being smuggled in as $\mathrm{diag}(x,x^{-1})$. That is the local realization of T5 J-uniqueness on the seam fiber.
The reduction field makes CensusPricing (which names $J$) downstream of SeamTransferPricing (which does not): a 2d pair fiber, unit determinant, delivered-leg eigenvalue, and a trace reading. The elliptic fields retrodict the kernel's phase-branch dead end as the wrong conjugacy class. The pairing identity reads $J$ as the product of the two one-sided relative imbalances any double-entry audit already records. No downstream consumers are wired yet in the graph; the certificate is the export surface for later census and carrier uniqueness arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.