exactJCostAsGeneralLedgerCost_eval
plain-language theorem explainer
Evaluating the exact-J ledger cost after it is re-embedded as a general ledger cost (onsite slot zero, link slot cosh−1) recovers the original exact-J action on every log potential. Anyone checking that the RS primitive sits inside the free-onsite class without changing its value will cite this. The proof is a short unfold-and-simp identity.
Claim. For any admissible weighted ledger graph $G$ on $n$ carriers and any log-potential $\varepsilon$, the evaluation of the general ledger cost that represents the exact $J$-cost (onsite term identically $0$, link term $u \mapsto \cosh u - 1$) at $\varepsilon$ equals the exact-$J$ action of $G$ on $\varepsilon$.
background
Door 2 / L1-hard asks whether shift invariance forces the onsite term of a ledger cost to be constant. The ambient object is a GeneralLedgerCost: an admissible weighted graph, a free absolute per-site map onsite : ℝ → ℝ, and a link map on posting differences. Nothing in that structure forces the onsite slot to vanish; that is what the forcing theorem must extract from ShiftInvariant.
The RS native cost is difference-only: the exact-$J$ action uses the T5 unique cost $J(x)=\cosh(\log x)-1$ on link ratios and never writes an onsite term. To place that primitive inside the free-onsite class without changing its meaning, one builds a general ledger cost whose onsite slot is the zero function and whose link slot is $u \mapsto \cosh u - 1$.
This lemma is the evaluation identity for that embedding: the general evaluator applied to the embedded cost must return exactly the original exact-$J$ action on every log potential.
proof idea
Term-level identity by unfolding. Expand the general evaluator, the embedding definition (onsite $\equiv 0$, link $= \cosh\cdot-1$), and the exact-$J$ action; simp closes the equality because both sides reduce to the same weighted sum of link costs on posting differences with a vanishing onsite contribution.
why it matters
The module's genuine obligation is to quantify over costs that can carry an onsite term and force that term constant from shift invariance, not by construction. Embedding the exact-$J$ action into that class is the bridge from the RS primitive to the free-onsite setting; this evaluation lemma certifies the bridge is value-preserving, so later forcing results about general costs apply to the actual RS cost without a hidden renormalization of the action.
It is a consistency check, not new physics: the panel already notes that proving shift invariance of a difference-only cost is a null test. The real L1 content lives in l1_onsite_forced_constant. Locality (finite-range weights) needed to kill Yukawa-like mean-field decoys remains outside this surface. No downstream consumers are wired yet; the lemma is infrastructure for the onsite-exclusion lane and the Door 2 provenance package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.