anomalyReading_apply
plain-language theorem explainer
The character-anomaly trace reading evaluates as $t/2 - 1$ on every real $t$. Anyone citing the bridge from weak ledger closure to ConservingSeamPricing needs this identity so that $R.f(\mathrm{Tr}\,W)$ is definitionally the character anomaly. The proof is pure reflexivity: the reading is defined that way.
Claim. For every real number $t$, the anomaly trace reading applied to $t$ equals $t/2 - 1$.
background
This module types the R1–R4 residue of conserving seam pricing in its weakest honest form. A TraceReading is a real function $f$ on traces used as a cost probe; the weak premise LedgerClosurePricing asks only that $f$ be calibrated at $2$ ($f(2)=0$) and faithful for $t>2$ ($f(t)\neq 0$), then forces the unique zero of the per-cycle seam cost at the deficit-free period $\beta=2\pi/\kappa$ (B2).
The character anomaly of a unimodular transfer $W$ is $\mathrm{Tr}(W)/2 - 1$. The named anomaly reading is the TraceReading whose probe is exactly that map. Conserving transfers already satisfy $\mathrm{Tr},W = x + x^{-1}\ge 2$ for real eigenvalue $x>0$ (AM–GM plus unimodularity), so the anomaly vanishes precisely at the identity eigenvalue $x=1$.
The local goal is to show that specializing the weak premise to this reading recovers the stronger ConservingSeamPricing package from SeamTransferCore without re-proving the pricing chain.
proof idea
One-line term proof by rfl. The anomaly reading is defined so that its probe field is $\lambda t., t/2 - 1$; applying that field is definitionally equal to the right-hand side. Marked @[simp] so later rewrites fire automatically.
why it matters
Feeds the bridge theorem conservingSeamPricing_of_anomalyLedger: if the weak ledger-closure premise holds for the anomaly reading, the four conjuncts of ConservingSeamPricing follow because $R.f(\mathrm{Tr},W)$ is definitionally the character anomaly. That bridge then cites the existing chain seam-transfer pricing → census pricing → B2 unique zero, recovering $C=J(\mathrm{turnRatio})$ without re-proof.
In the module's acceptance narrative this is item 3 of what is theorem: the exact anomaly normalization is not load-bearing for the B2 zero set under the weak premise, yet when one does use it, the strong package is recovered definitionally. Framework-wise this sits in the holography seam ledger, linking conserving transfer traces to the J-cost identity $J(x)=(x+x^{-1})/2-1$ (T5) via the character anomaly. B3 (identifying $\kappa$ with the horizon clock rate) and physical instantiation of LedgerClosurePricing remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.