anomalyLedger_iff_conserving
plain-language theorem explainer
At the character-anomaly trace reading $f(t)=t/2-1$, ledger-closure pricing of a seam cost $C$ is equivalent to conserving seam pricing. Anyone citing the B2 discharge bridge or the seam-ledger certificate needs this equivalence. The weak premise strictly generalizes the landed one, yet loses nothing at the anomaly point. Proof is a two-direction constructor: one arm applies an existing one-way lemma; the other unpacks the matrix witness and rewrites the cost equality.
Claim. For any cost $C:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$, the ledger-closure pricing condition at the anomaly reading $f(t)=t/2-1$ holds for $C$ if and only if $C$ satisfies conserving seam pricing (pairing-preserving $2\times 2$ transfer with real eigenvalue equal to the turn ratio, and $C$ equal to the anomaly of the transfer trace).
background
Module SeamLedgerDischarge types the R1–R4 residue of conserving seam pricing in its weakest honest form and shows that B2 (unique zero of the per-cycle seam cost at the deficit-free period $\beta=2\pi/\kappa$) survives a strict weakening of the fourth conjunct.
LedgerClosurePricing (relative to a trace reading $R$) asserts: for every $\kappa,T>0$ there is a real $2\times 2$ matrix $W$ that preserves the double-entry pairing form, has real eigenvalue equal to the turn ratio $\mathrm{turnRatio}(\kappa,T)$, and satisfies $C(\kappa,T)=R.f(\mathrm{Tr},W)$. The anomaly reading is the calibrated character $f(t)=t/2-1$. Conserving seam pricing is the landed four-conjunct premise from the seam-transfer core (conservation, real eigen, and cost tied to the anomaly of the trace).
The module already has the one-way map from anomaly ledger pricing to conserving seam pricing, plus the trace bound $\mathrm{Tr},W=x+x^{-1}\ge 2$ for pairing-conserving transfers with positive real eigenvalue.
proof idea
Iff by constructor.
Forward direction is a one-line application of the sibling lemma conservingSeamPricing_of_anomalyLedger.
Reverse: assume conserving seam pricing. For given $\kappa,T>0$, unpack the witness matrix $W$ together with pairing conservation, the real-eigenvalue hypothesis at the turn ratio, and the cost identity $C(\kappa,T)=\mathrm{Tr}(W)/2-1$. Re-package the same $W$ as a ledger-closure witness for the anomaly reading; the cost clause is the given identity transported by trans rfl (anomaly reading applied to the trace is definitionally that expression).
why it matters
This is the bridge theorem of the module: at the anomaly reading the weak premise is equivalent to conserving seam pricing, so the existing cited chain seamTransferPricing_of_conserving → censusPricing_of_seamTransfer → b2_unique_zero_of_conserving recovers $C=J(\mathrm{turnRatio})$ and B2 without re-proof. Downstream it is installed as anomaly_bridge in seamLedgerDischargeCert.
Framework role: it separates what is load-bearing for B2 (calibration $f(2)=0$ and faithfulness $f(t)\ne 0$ for $t>2$) from the specific anomaly normalization $\mathrm{Tr}/2-1$, which is not needed for the zero set. That matches the module claim that B2 is forced-conditional on any calibrated faithful reading. Open items remain B3 ($\kappa$ as horizon clock rate) and physical instantiation of ledger-closure pricing for the actual seam cost; this theorem does not close those.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.