exactJCostAsGeneralLedgerCost_onsite_zero
plain-language theorem explainer
The exact-J ledger cost, re-expressed as a general ledger cost, has onsite term identically the zero function (constant k = 0), not merely some unknown constant. Consistency check for the pair-kernel onsite-exclusion lane against the RS cost primitive. One-line term proof by definitional equality.
Claim. For any weighted ledger graph $G$ on $n \ge 1$ vertices, there exists $k \in \mathbb{R}$ with $k = 0$ such that the onsite component of the exact-$J$ cost (viewed as a general ledger cost on $G$) satisfies $\mathrm{onsite}(u) = k$ for every real $u$.
background
Door 2 / L1-hard asks whether shift invariance of a ledger cost forces any on-site mass term to be constant. The ambient class is GeneralLedgerCost: a weighted simplicial graph plus a free onsite map $\mathbb{R}\to\mathbb{R}$ and a link map of posting differences. A weighted ledger graph carries a nonnegative symmetric edge weight on $\mathrm{Fin}, n$.
The RS cost primitive is difference-only: exact $J$-cost uses link $u \mapsto \cosh u - 1$ (equivalently $J$ in log coordinates) and never writes an onsite slot. The re-expression as a general ledger cost sets onsite to the zero function by definition, so that the general forcing theorem can be applied to this slice without changing the action.
Module context: shift invariance alone is necessary but not sufficient to kill screened nonlocal kernels; a separate locality hypothesis is needed for that. This declaration is only the sanity end of the exact-$J$ embedding.
proof idea
Pure term proof. Witness the existential with $k = 0$; the equality $k = 0$ is rfl; the pointwise onsite identity is fun u => rfl because the re-expression defines onsite as fun _ => 0. No lemmas are applied.
why it matters
Doc-comment labels this a sanity corollary, not new content: applying the general onsite-forcing story to the exact-$J$ slice recovers $k = 0$ because the onsite term was already zero by construction, not merely forced constant. It closes the consistency check that the RS primitive sits inside the GeneralLedgerCost class without smuggling a hidden mass term.
No downstream dependents are recorded. In the broader Door 2 package it sits beside the genuine L1 result (shift invariance forces onsite constant for free onsite slots) and the mean-field counterexample showing shift invariance alone does not decide $1/r$ versus Yukawa screening. Framework landmark: T5 $J$-uniqueness supplies the link shape $\cosh(\log x)-1$; this theorem only audits the onsite slot of that embedding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.