link_part_shift_invariant
plain-language theorem explainer
Under any global additive shift of the log-potentials, the double sum of weighted link costs is unchanged, for every link function and every admissible weight graph. Anyone proving that shift invariance only constrains the onsite term cites this identity. The proof is pure cancellation: each difference (εᵢ+c)−(εⱼ+c) equals εᵢ−εⱼ by ring, then two Finset.sum_congr steps.
Claim. For any finite carrier size $n$, any general ledger cost $C$ (admissible weighted graph, free onsite map, free link map), any log-potential assignment $\varepsilon$, and any real constant $c$, $$\sum_{i,j} w_{ij}\,\mathrm{link}\bigl((\varepsilon_i+c)-(\varepsilon_j+c)\bigr)=\sum_{i,j} w_{ij}\,\mathrm{link}(\varepsilon_i-\varepsilon_j).$$
background
Door 2 / L1-hard isolates onsite exclusion from shift invariance. A GeneralLedgerCost on $n$ carriers is an admissible nonnegative-symmetric weight graph together with a free absolute per-site map onsite : ℝ → ℝ and a free per-link map link : ℝ → ℝ. Total cost is $\sum_i \mathrm{onsite}(\varepsilon_i)+\sum_{ij} w_{ij},\mathrm{link}(\varepsilon_i-\varepsilon_j)$.
ShiftInvariant (hypothesis R1) asserts that adding any constant $c$ to every log-potential leaves that total cost unchanged: absolute account levels carry no cost, only relations do. The module stresses that pure difference-only actions (e.g. exact-$J$ cost) make shift invariance a null test, because they never write an onsite slot.
This lemma records the tautological half: the link double sum is automatically invariant under global shifts, for arbitrary link and arbitrary weights. It is the algebraic identity that later lets the full R1 hypothesis bite only on the onsite sum.
proof idea
Two nested Finset.sum_congr rfl reduce the claim to a pointwise identity on each pair $(i,j)$. The single algebraic step is
$$(\varepsilon_i+c)-(\varepsilon_j+c)=\varepsilon_i-\varepsilon_j,$$
proved by ring. Rewrite with that equality and both summands match. No property of link, of the weights, or of onsite is used.
why it matters
Feeds directly into shiftInvariant_iff_onsite_sum, whose doc-comment states the consequence: ShiftInvariant C is equivalent to shift invariance of the onsite sum alone, so R1 "only has teeth against the onsite term, never against link".
In the Door 2 / L1 package this is the null half that must be peeled off before the genuine forcing theorem l1_onsite_forced_constant can force the onsite map to a constant. It also explains why shift invariance of exact-$J$ (difference-only) cost is content-free evidence against onsite mass. The panel verdict keeps a separate locality gap open: shift invariance alone does not kill all-to-all Yukawa-like kernels; that needs an L0 finite-range hypothesis not yet on the Lean surface. Landmark contact is the double-entry gauge reading of R1 (absolute levels free), not T5–T8 uniqueness of $J$ itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.