ConservingSeamPricing
plain-language theorem explainer
Conservation pricing for a seam cost C says every positive curvature-period pair admits a 2x2 transfer that preserves the double-entry pairing form, has a real eigenvalue equal to the turn ratio, and whose character anomaly equals C. Anyone reducing ledger conservation to CensusPricing or the B2 unique-zero statement cites this premise. It is a Prop definition packaging three ledger sentences (form conservation, delivered-leg scaling, anomaly reading), with the determinant condition translated away.
Claim. A cost $C:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ satisfies conserving seam pricing when for every $\kappa>0$ and $T>0$ there exists a real $2\times 2$ matrix $W$ such that $W$ preserves the double-entry pairing form $\omega(u,v)=u_0v_1-u_1v_0$, $W$ has real eigenvalue equal to the turn ratio $x(\kappa,T)$, and $C(\kappa,T)=\mathrm{Tr}(W)/2-1$.
background
Module SeamTransferCore lands Phase B of the Scale-Holonomy Trace Core: the per-closure recognition cost of a seam crossing at mismatch ratio $x$ is the character anomaly $\mathrm{Tr}(W)/2-1$ of the transfer $W$ one closure induces on the seam's double-entry pair fiber.
The pairing form is the signed area of the (debit, credit) parallelogram on that 2d fiber; double-entry says one closure cannot create or destroy it. Real-eigenvalue means some nonzero fiber vector scales by $x$ under $W$ (the delivered leg only; nothing is assumed about the other leg). Character anomaly is the unique conjugation-invariant scalar of the closure holonomy, normalized to vanish at the identity.
The sibling premise SeamTransferPricing names $\det W=1$ explicitly. This definition replaces that matrix invariant by preservation of the pairing form, so every conjunct is a ledger sentence: conservation, delivery, invariant reading. Balance then forces the reciprocal leg, and the anomaly equals the T5 cost $J(x)=(x+x^{-1})/2-1$.
proof idea
Pure Prop definition, not a proved theorem. The body quantifies over positive $\kappa,T$ and asserts existence of a real $2\times 2$ matrix $W$ with three conjuncts: the linear action of $W$ preserves the pairing form on every pair of fiber vectors; $W$ has real eigenvalue equal to the turn ratio at $(\kappa,T)$; and $C(\kappa,T)$ equals the character anomaly of $W$. No tactics or lemmas fire here; later theorems (pair-form iff unit determinant, reduction to transfer pricing, B2 unique zero) consume this package.
why it matters
Determinant-free packaging of the Phase-B pricing premise. Downstream, the conserving-to-transfer lift recovers SeamTransferPricing (pairing preservation implies unit determinant), and the full Phase-B chain theorem runs from this premise to CensusPricing and the unique zero of $C$ at the deficit-free period $\beta=2\pi/\kappa$, with no $J$, cosh, determinant, or diagonal form named in the hypothesis.
In SeamLedgerDischarge, the anomaly-reading instance of ledger-closure pricing is equivalent to this premise, and the discharge certificate bundles R1-R4 around that equivalence. Framework landmark: T5 J-uniqueness. $J$ is not an input; it emerges from balanced trace plus character-anomaly algebra once conservation and one real eigenvalue are given. Physical instantiation of the premise for the actual seam remains a named MODEL until derived from seam geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.