Foundation Pair Kernel Onsite Exclusion Shift Invariant Iff Onsite Sum

The shift-invariance equivalence

In a ledger model of recognition, a cost rule assigns a number to each configuration of values. One natural symmetry to ask for is shift invariance: adding the same constant to every value leaves the total cost unchanged. This means absolute levels carry no cost, only the relations between values do. The declaration shiftInvariant_iff_onsite_sum proves that this symmetry holds for the whole cost rule if and only if it holds for the sum of the per-site terms alone. The per-link terms, which depend only on differences between values, are automatically shift-invariant for any link function and any weight graph, because (x + c) - (y + c) = x - y.

The proof is a theorem in the framework's machine-checked library of formal theorems. It works over a general class of cost rules where the per-site term is a genuinely free parameter, not fixed to zero by definition. This is the anti-cheat: the theorem must rule out non-constant per-site terms by the shift-invariance hypothesis, not by the shape of the definition. The equivalence isolates the non-vacuous content of shift invariance: it only has teeth against the per-site term, never against the link terms.

What the theorem does not claim is as important as what it proves. Shift invariance alone does not force the per-site term to be constant; that stronger conclusion requires an additional hypothesis, and the library proves it separately under the name l1_onsite_forced_constant. The equivalence also does not exclude non-local, all-to-all coupling structures. The library explicitly constructs a mean-field cost rule that is shift-invariant but has full support, meaning every pair of sites is coupled, even maximally separated ones. Excluding that requires a separate locality hypothesis, which is not part of this theorem and is not yet anywhere in the library's surface.

In plain terms, the declaration sharpens what shift invariance can and cannot do. It shows the symmetry reduces to a condition on the per-site term, and it marks the boundary of that reduction. The reader can now see that proving the absence of a per-site mass term requires more than shift invariance, and that ruling out non-local screening requires a different kind of assumption entirely.

/-- Consequently, `ShiftInvariant C` is *equivalent* to the onsite sum alone being
    shift-invariant. This isolates exactly the non-vacuous content: `ShiftInvariant`
    only has teeth against the onsite term, never against `link`. -/
theorem shiftInvariant_iff_onsite_sum {n : ℕ} (C : GeneralLedgerCost n) :
    ShiftInvariant C ↔
      ∀ (ε : LogPotential n) (c : ℝ),
        (∑ i : Fin n, C.onsite (ε i + c)) = ∑ i : Fin n, C.onsite (ε i) := by
  constructor
  · intro hR1 ε c
    have h := hR1 ε c
    unfold GeneralLedgerCost.eval at h
    rw [link_part_shift_invariant C ε c] at h
    linarith
  · intro honsite ε c
    unfold GeneralLedgerCost.eval
    rw [link_part_shift_invariant C ε c, honsite ε c]

/-- The link (difference-only) part of `eval` never changes under a global shift, for
    *any* `link` function and *any* weight graph — a pure consequence of the fact that
    `(εᵢ + c) − (εⱼ + c) = εᵢ − εⱼ`. This is the tautological half of `ShiftInvariant`;
    it is exactly what makes `exactJCostAction`'s own shift invariance a null test (it
    has no onsite slot, so it only ever exercises this half). -/
theorem link_part_shift_invariant {n : ℕ} (C : GeneralLedgerCost n)
    (ε : LogPotential n) (c : ℝ) :
    (∑ i : Fin n, ∑ j : Fin n, C.G.weight i j * C.link ((ε i + c) - (ε j + c)))
      = ∑ i : Fin n, ∑ j : Fin n, C.G.weight i j * C.link (ε i - ε j) := by
  apply Finset.sum_congr rfl
  intro i _
  apply Finset.sum_congr rfl
  intro j _
  have : (ε i + c) - (ε j + c) = ε i - ε j := by ring
  rw [this]

/-- **The honest negative.** The mean-field ledger cost is shift-invariant (it has no
    onsite term, so `ShiftInvariant` holds for the shape reason isolated in
    `shiftInvariant_iff_onsite_sum`, not because locality was ever assumed), yet its
    weight graph is non-local (`meanFieldWeight_full_support`). So `L1`
    (`l1_onsite_forced_constant`), even fully proved and even fully forced from
    first principles, does NOT by itself exclude a screened kernel: excluding the
    mean-field / all-to-all route needs a SEPARATE locality hypothesis `L0`
    (finite-range weights), which is not addressed in this module and, per the panel
    audit, is currently nowhere in the Lean surface. This is the scoped, honest residual
    of Door 2 / L1-hard: on-site exclusion is real and forced (conditional on
    `ShiftInvariant`), but on-site exclusion alone is not the whole story. -/
theorem meanFieldLedgerCost_shift_invariant (n : ℕ) :
    ShiftInvariant (meanFieldLedgerCost n) := by
  rw [shiftInvariant_iff_onsite_sum]
  intro ε c
  simp [meanFieldLedgerCost]

/-- The mean-field weight has full support: every pair, including every distinct pair,
    is coupled with nonzero weight. This is the formal shape of "not finite-range" — a
    genuinely local weight graph must vanish outside a bounded neighborhood as `n`
    grows, and this one never does. -/
theorem meanFieldWeight_full_support (n : ℕ) (i j : Fin n) :
    (meanFieldWeight n).weight i j ≠ 0 := by
  simp [meanFieldWeight]

What this page does not claim

Shift invariance alone forces the per-site term to be constant. The theorem excludes non-local, all-to-all coupling structures. The declaration itself proves the absence of a per-site mass term.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PairKernelOnsiteExclusion.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: