is
plain-language theorem explainer
Instance packaging that the conserving seam-pricing residue is the landed form of the typed R1–R4 package, with that premise inhabited. Every field is an unconditional theorem; only the physical seam's match to ledger-closure pricing stays a named model hypothesis for forced-conditional B2 discharge. Anyone wiring weak trace readings to the conserving chain would reach for it. Pure instance assembly: no tactic proof body.
Claim. There is an instance witnessing that the conserving seam-pricing package is inhabited. Its component fields are unconditional theorems. The physical identification of the actual seam cost $C$ with ledger-closure pricing for some trace reading $R$ (i.e., existence of a unimodular $2\times 2$ real matrix $W$ conserving the debit/credit pairing, with real eigenvalue equal to the turn ratio, and $C(\kappa,T)=R.f(\mathrm{tr}\,W)$) remains a named model premise, consumed only by forced-conditional discharge theorems stated separately.
background
Module SeamLedgerDischarge types the R1–R4 residue of conserving seam pricing in its weakest honest form and shows that B2 (uniqueness of the deficit-free period $\beta=2\pi/\kappa$ as the zero of per-cycle seam cost) survives dropping the exact character-anomaly normalization.
Ledger-closure pricing (the typed model premise) asks: for each $\kappa,T>0$ there exists a real $2\times 2$ matrix $W$ that conserves the double-entry pairing form, has real eigenvalue equal to the turn ratio at $(\kappa,T)$, and whose cost equals a chosen trace reading $R$ applied to $\mathrm{tr},W$. Conservation of the pairing is unimodularity on the pair fiber; the key unconditional lemma is the conserving trace bound $\mathrm{Tr},W=x+x^{-1}\ge 2$ for $x>0$, equality iff $x=1$.
The anomaly reading $f(t)=t/2-1$ recovers full conserving seam pricing and the classical $C=J(\mathrm{turnRatio})$ chain; the weak premise needs only calibration $f(2)=0$ and faithfulness $f(t)\ne 0$ for $t>2$.
proof idea
Definition-style instance (no proof body). It assembles already-proved unconditional fields into the landed conserving seam-pricing structure and records inhabitation of that premise. No new lemmas are invoked; physical ledger-closure pricing for the actual seam is deliberately left as a named model hypothesis rather than discharged here.
why it matters
Closes the packaging step in the holography seam-ledger story: the R1–R4 residue is typed and inhabited at the conserving level, so B2 discharge can be stated forced-conditionally on the weaker ledger-closure premise (any calibrated faithful trace reading), not only on the anomaly normalization $\mathrm{Tr}(W)/2-1$. Downstream, the bridge at the anomaly reading equates the weak premise with full conserving seam pricing and re-cites the existing seam-transfer and census pricing chain to recover $C=J(\mathrm{turnRatio})$ and B2, without re-proving it.
Framework role: supports the holographic cost zero-set (unique period $2\pi/\kappa$) while keeping honest about what remains open: B3 ($\kappa$ as horizon clock rate) and the physical instantiation that the actual seam functional satisfies ledger-closure pricing for some trace reading. Tightness theorems in the same module show calibration and faithfulness are load-bearing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.