ShiftInvariant
plain-language theorem explainer
Global shift invariance for a general ledger cost: adding any real constant to every log-potential leaves the total cost unchanged. It is the named R1 double-entry gauge hypothesis (absolute account levels carry no cost; only relations do), stated as a Prop rather than derived. Downstream L1 forcing cites it to kill free on-site mass terms. The body is a pure universal quantification over potentials and shifts.
Claim. Let $C$ be a general ledger cost on $n$ log-potential carriers (free per-site term plus a link term on posting differences over a weighted graph). $C$ is shift-invariant when, for every assignment $\varepsilon$ and every $c\in\mathbb{R}$, $C(\varepsilon+c)=C(\varepsilon)$, where $(\varepsilon+c)_i=\varepsilon_i+c$.
background
This module is Door 2 / L1-hard in the pair-kernel provenance lane. The exact-$J$ cost action is difference-only by construction, so proving its shift invariance is a null test: it never had an on-site slot to begin with. The genuine obligation is to quantify over a wider class that can express an on-site term and force that term from a real hypothesis.
A general ledger cost on $n$ carriers packages an admissible nonnegative symmetric weight graph $G$, a free absolute per-site map $\mathrm{onsite}:\mathbb{R}\to\mathbb{R}$, and a per-link map $\mathrm{link}:\mathbb{R}\to\mathbb{R}$. Total evaluation is $\sum_i \mathrm{onsite}(\varepsilon_i)+\sum_{ij} w_{ij}\cdot\mathrm{link}(\varepsilon_i-\varepsilon_j)$. Nothing in the structure forces $\mathrm{onsite}$ to vanish or be constant.
R1 is hypothesis, not Meta-Principle output. Canonical MP only rejects recognition of uninhabited Nothing; it cannot reject an inhabited frozen anchor that an on-site mass would price against. The live MP-to-Axiom-R bet is closed negative.
proof idea
Definitional Prop, not a proved theorem. The body is the single universal statement that evaluation is unchanged under the uniform additive shift $\varepsilon\mapsto\varepsilon+c$.
No tactics or upstream lemmas fire at the definition site. Content is isolated later: the link (difference) half is automatic because $(\varepsilon_i+c)-(\varepsilon_j+c)=\varepsilon_i-\varepsilon_j$, while the onsite sum carries all the force. The sibling equivalence then rewrites the Prop as invariance of $\sum_i\mathrm{onsite}(\varepsilon_i)$ alone.
why it matters
Named premise for L1-FORCE: under this hypothesis and $n\ge 1$, the onsite part of any general ledger cost is forced to a constant function of its argument, so no writable on-site mass/absolute term survives. The same Prop is the left-hand side of the onsite-sum equivalence, the hypothesis the Yukawa onsite decoy fails (anti-cheat witness), and the property the mean-field ledger cost still satisfies.
Panel verdict (door2_L1_provenance): shift invariance is necessary but not sufficient to exclude screened kernels. An admissible, shift-invariant, purely difference-only cost can still use all-to-all weights and open a mass gap away from $k=0$. Killing that route needs a separate locality hypothesis L0 (finite-range weights), absent from this module and from the Lean surface. L1 closes only the on-site-mass branch of the $1/r$ vs Yukawa question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.