anomalyReading
plain-language theorem explainer
The character-anomaly reading is the map f(t)=t/2−1 on real transfer traces, packaged as a calibrated and faithful trace reading (f(2)=0 and f(t)≠0 for t>2). Anyone bridging the weak ledger-closure premise back to ConservingSeamPricing, CensusPricing, or the B2 unique-zero statement cites this instance. The body is a structure instance: norm_num for calibration, a one-line positivity argument for faithfulness.
Claim. The character-anomaly reading is the real function $f(t)=t/2-1$, viewed as a trace reading: it is calibrated, $f(2)=0$, and faithful on the realizable range, $f(t)\neq 0$ whenever $t>2$.
background
SeamLedgerDischarge types the R1–R4 residue of conserving seam pricing in its weakest honest form: cost depends on the transfer only through a reading of the trace, plus two audit normalizations. The structure TraceReading packages exactly that residue. Its field f is a real function of the trace (R4 class-function content, using that the trace is the unique conjugation invariant of a unimodular 2×2 transfer). Calibration requires f(2)=0: the identity closure posts zero cost. Faithfulness requires f(t)≠0 for t>2: a strictly imbalanced closure cannot read as free.
The module proves that B2 (unique zero of per-cycle seam cost at the deficit-free period β=2π/κ) already follows from any such reading under LedgerClosurePricing; the exact anomaly normalization is not load-bearing for the zero set. This definition supplies the classical character-anomaly choice f(t)=t/2−1 so the weak premise can be compared with the landed ConservingSeamPricing chain.
proof idea
Structure instance, not a deep proof. The reading field is definitionally t ↦ t/2 − 1. Calibration is f(2)=0, discharged by norm_num. Faithfulness: given t>2, linarith yields 0 < t/2 − 1, hence f(t)≠0 by ne_of_gt. No upstream lemmas beyond the TraceReading field obligations.
why it matters
This is the bridge instance that reconnects the weakened ledger premise to the landed chain without re-proving it. Downstream, anomalyLedger_iff_conserving shows LedgerClosurePricing at this reading is equivalent to ConservingSeamPricing; conservingSeamPricing_of_anomalyLedger, censusPricing_of_anomalyLedger, and cost_eq_J_of_anomalyLedger then recover C=J(turnRatio) (T5 pricing) by citation. b2_unique_zero_of_anomalyLedger checks that the weak and landed B2 routes agree on the zero set. SeamLedgerDischargeCert and ledgerClosurePricing_turnRatioCost also consume it.
Framework role: it is one admissible reading among many; the module’s main B2 theorem never needs this specific f. It exists so the character-anomaly normalization used in the original conserving-seam story remains available, while proving that calibration plus faithfulness alone force the unique zero. B3 (κ as horizon clock rate) and physical instantiation of LedgerClosurePricing stay open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.