LedgerClosurePricing
plain-language theorem explainer
Typed weak R1–R4 premise for per-cycle seam cost: for every κ>0 and T>0 a 2×2 real transfer exists that conserves the double-entry pairing, carries the turn ratio κT/(2π) as a real eigenvalue, and reports cost through a fixed calibrated faithful function of the trace. B2 uniqueness and the anomaly bridge cite it as the forced-conditional hypothesis. Definitional Prop packaging four ledger residues; not a proved existence claim.
Claim. Fix a calibrated faithful trace reading $R$ (a map $f:\mathbb{R}\to\mathbb{R}$ with $f(2)=0$ and $f(t)\neq 0$ for all $t>2$) and a cost $C:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$. The ledger-closure pricing premise asserts: for all $\kappa>0$ and $T>0$ there is a real $2\times 2$ matrix $W$ such that $W$ preserves the double-entry pairing form, $W$ has real eigenvalue equal to the turn ratio $x=\kappa T/(2\pi)$, and $C(\kappa,T)=f(\mathrm{Tr}\,W)$.
background
This module types the seam-ledger residue in its weakest honest form and shows that B2 (the deficit-free period $\beta=2\pi/\kappa$ is the unique zero of per-cycle seam cost) survives weakening the fourth conjunct away from the exact character anomaly $\mathrm{Tr}(W)/2-1$.
A trace reading packages R4's zero-set content: cost depends on the transfer only through the trace (the unique conjugation invariant of unimodular $2\times 2$ maps), plus calibration $f(2)=0$ (identity closure is free) and faithfulness on $(2,\infty)$ (strictly imbalanced closures are not free). Conservation of the oriented debit/credit pairing is the ledger form of unimodularity; delivery is the real-eigenvalue condition at the turn ratio from B1's exponential-lattice geometry and B3's clock rate $\kappa$ (typed, still open).
Upstream, the landed conserving-seam premise and the trace bound (pairing-conserving transfer with real eigenvalue $x>0$ has $\mathrm{Tr},W=x+x^{-1}\ge 2$, equality iff $x=1$) supply the comparison target this weak premise generalizes.
proof idea
Definitional Prop, not a proof. The body is a universal quantifier over positive $\kappa,T$ asserting existence of a real $2\times 2$ matrix $W$ whose three conjuncts are exactly R2 (pairing conservation under $W$), R3 (real eigenvalue at the turn ratio), and weakened R4 (cost equals the fixed reading of $\mathrm{Tr},W$). R1 is carried by the matrix type itself. No tactics, no lemmas applied at the definition site.
why it matters
This is the typed weak premise on which the module's main B2 discharge is forced-conditional: for any calibrated faithful reading, ledger-closure pricing forces $C(\kappa,T)=0$ iff $T=2\pi/\kappa$, using the conserving-trace bound and turn-ratio uniqueness, with no $J$, cosh, or anomaly normalization in the zero-set argument.
Downstream it feeds the anomaly bridge (at the character-anomaly reading the weak premise is equivalent to conserving-seam pricing), the cited recovery of census pricing and $C=J(\mathrm{turnRatio})$ along the landed chain, non-vacuity witnesses, and tightness lemmas showing faithfulness and calibration are load-bearing. Framework role: isolates how little of T5's full J-pricing is needed for the B2 zero set on the holographic seam, while B3 ($\kappa$ as horizon clock) and physical instantiation of the premise remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.