b2_unique_zero_of_anomalyLedger
plain-language theorem explainer
At the anomaly reading of the seam ledger, the per-cycle cost C vanishes exactly when the period equals the Euclidean deficit-free period 2π/κ. Anyone checking that the weak ledger-closure route and the landed conserving-seam route agree on B2's zero set would cite this. The proof is a one-line wrapper: convert the anomaly LedgerClosurePricing hypothesis to ConservingSeamPricing, then apply the existing B2 uniqueness theorem.
Claim. Let $C:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ satisfy ledger-closure pricing at the anomaly reading $f(t)=t/2-1$ (so for each $\kappa,T>0$ there is a pairing-conserving $2\times 2$ real matrix $W$ with real eigenvalue equal to the turn ratio at $(\kappa,T)$ and $C(\kappa,T)=f(\mathrm{Tr}\,W)$). Then for all $\kappa,T>0$, $C(\kappa,T)=0$ if and only if $T=2\pi/\kappa$.
background
This module types the R1–R4 residue of conserving seam pricing in its weakest honest form and shows that B2 (uniqueness of the deficit-free period as the zero of the per-cycle seam cost) survives dropping the exact character-anomaly normalization as a load-bearing ingredient.
Ledger-closure pricing relative to a trace reading $R$ asserts: for every $\kappa,T>0$ there exists a real $2\times 2$ matrix $W$ that preserves the double-entry pairing form, has real eigenvalue equal to the turn ratio at $(\kappa,T)$, and prices the cycle by $C(\kappa,T)=R.f(\mathrm{Tr},W)$. The anomaly reading is the calibrated map $f(t)=t/2-1$.
The landed route already has B2 under full ConservingSeamPricing via the chain seam-transfer pricing → census pricing → unique zero of the conserving cost. At the anomaly reading the weak premise is equivalent to that conserving package, so the zero-set claim transfers.
proof idea
One-line term wrapper. First apply conservingSeamPricing_of_anomalyLedger to the hypothesis LedgerClosurePricing anomalyReading C, obtaining ConservingSeamPricing for $C$. Then feed that into b2_unique_zero_of_conserving, which already discharges $C,\kappa,T=0\leftrightarrow T=2\pi/\kappa$ for positive $\kappa,T$. No new algebra is done here; the work sits in the bridge and in the cited conserving uniqueness theorem.
why it matters
B2 is the claim that the Euclidean period $\beta=2\pi/\kappa$ is the unique zero of the per-cycle seam cost. The module's main forced-conditional result already gets B2 from any faithful, calibrated trace reading under ledger-closure pricing, without $J$ or $\cosh$. This theorem is the consistency check on the landed path: when the reading is specifically the anomaly $t/2-1$, the weak route and the conserving-seam chain agree on the same zero set.
It sits under the holography seam-ledger discharge and cites the existing conserving B2 theorem rather than re-proving it. No downstream consumers are wired yet. B3 (identifying $\kappa$ with the horizon's continued clock rate) and physical instantiation of ledger-closure pricing for the actual seam remain open; this result does not touch those.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.