SeamTransferCoreCert
plain-language theorem explainer
Bundled Prop packing the Phase-B per-closure seam-transfer core: balance forces the reciprocal eigenvalue, the character anomaly equals J, SeamTransferPricing reduces to CensusPricing, the elliptic class is phase-cost and mismatch-dead, plus pairing, falsifier, and reciprocity identities. Anyone auditing the Scale-Holonomy Trace Core cites this bundle. It is a pure structure of unconditional fields; the inhabitant theorem wires the named lemmas.
Claim. A certificate asserting: (1) any $2\times 2$ real $W$ with $\det W=1$ and a real eigenvalue $x\neq 0$ also has eigenvalue $x^{-1}$; (2) if moreover $x>0$, then $\mathrm{Tr}(W)/2-1=J(x)$; (3) any cost priced by a balanced seam transfer satisfies census pricing; (4) the character anomaly of rotation by $\theta$ equals the phase cost of $\theta$; (5) a rotation has no real eigenvalue except $\pm 1$; (6) $J(x)=(x-1)(1-x^{-1})/2$ for $x\neq 0$; (7) $J(3)/J(2)\neq 2$; (8) pair-form preservation iff $\det W=1$; (9) if $\det W=1$ and $WV=I$ then $\mathrm{Tr} V=\mathrm{Tr} W$.
background
Module SeamTransferCore lands the per-closure half of the Scale-Holonomy Trace Core (Phase B). The panel decision fixes the recognition cost of a seam crossing at mismatch ratio $x$ as the character anomaly $C=\mathrm{Tr}(W)/2-1$ of the transfer $W$ induced on the seam's double-entry pair fiber.
HasRealEigen W x means some nonzero fiber vector scales by $x$ under one closure: the delivered leg only; nothing about the other leg is assumed. charAnomaly W is that unique conjugation-invariant scalar, normalized to vanish at the identity. SeamTransferPricing C is the structural premise: for each $(\kappa,T)$ there exists a balanced ($\det=1$) transfer whose delivered-leg eigenvalue is the turn ratio and whose character anomaly equals $C(\kappa,T)$. None of those conjuncts names $J$.
Upstream, $J(x)=(x+x^{-1})/2-1$ is the T5 recognition cost. The circularity fence is explicit: never posit $W=\mathrm{diag}(x,x^{-1})$; derive the conjugate from balance and one eigenvalue.
proof idea
Pure structure definition: nine fields of type Prop, no proof body. Inhabitation is separate (seamTransferCoreCert), which fills each field by a one-line application of the corresponding lemma: balanced_conjugate, charAnomaly_eq_J, censusPricing_of_seamTransfer, charAnomaly_rotation, elliptic_no_real_mismatch, plus the pairing identity, numeric falsifier, pair-form conservation, and reciprocity/trace lemmas. The structure only packages the claim surface.
why it matters
This is the typed claim surface for LEG-B Phase B. Downstream, seamTransferCoreCert proves the certificate holds by wiring the individual theorems. The bundle encodes the panel guardrail: reciprocity is conservation (det = 1 forces the conjugate eigenvalue and equal traces under inversion), not a modeling choice. J emerges from Cayley–Hamilton on a unit-determinant 2×2 matrix with one real eigenvalue (T5 landmark), with no J in the inputs.
The reduction field is the load-bearing bridge: CensusPricing (which names J) becomes downstream of SeamTransferPricing (which does not). The elliptic fields retrodict the earlier dead end as the wrong conjugacy class: rotations carry phaseCost and admit no genuine real mismatch. The numeric falsifier is panel Live Bet 2, discriminating J from naive linear surplus ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.