Foundation Pair Kernel Locality Band Weight Adjacent Coupled

The band graph witness

The declaration bandWeight_adjacent_coupled proves a simple fact about a specific weighted graph: when sites are arranged in a line and each site is coupled only to its immediate neighbors, the coupling strength between two adjacent sites is exactly 1. This is a ledger, a discrete record of events where each pair of sites carries a number representing their interaction. The graph in question, called the band graph, assigns weight 1 to pairs at index-distance 1 and weight 0 to all pairs farther apart.

The theorem matters because it supplies a concrete witness for a hypothesis called FiniteRange, which states that no coupling exists between sites separated by more than a fixed number of steps. The band graph satisfies this hypothesis at radius 1, and the adjacent-coupled theorem confirms that the graph is not trivial: it genuinely couples neighboring sites. Without this witness, the hypothesis could be vacuously true, meaning it excludes nothing. The theorem shows that at least one admissible, non-degenerate cost function lives inside the hypothesis.

The same module also proves that a different graph, the mean-field graph where every site couples to every other site with weight 1, violates FiniteRange at every fixed radius once the carrier is large enough. This contrast is what makes the hypothesis discriminating: it accepts the band graph and rejects the mean-field graph. The framework uses this to argue that FiniteRange is load-bearing, not a null assumption.

What the theorem does not claim is equally important. It does not prove that FiniteRange excludes screening effects; that step requires a separate dispersion analysis that is numerical, not formal. It does not derive FiniteRange from any more primitive principle; the provenance of the hypothesis remains open. And it says nothing about specific coupling strengths like 1/r versus Yukawa forms, nor about any physical constants such as 5/8 or Z_eff. The theorem is a narrow formal result about one graph, used as a building block in a larger argument.

/-- Sanity: the band graph does couple adjacent sites (weight `1` on the nearest-neighbor
    pair `0,1`), so it is not the trivial diagonal graph — the witness carries real content. -/
theorem bandWeight_adjacent_coupled (n : ℕ) (hn : 2 ≤ n) :
    (bandWeight n).weight ⟨0, by omega⟩ ⟨1, by omega⟩ = 1 := by
  have hd : cellDist (⟨0, by omega⟩ : Fin n) (⟨1, by omega⟩ : Fin n) ≤ 1 := by
    show Nat.dist 0 1 ≤ 1
    unfold Nat.dist
    omega
  simp only [bandWeight]
  exact if_pos hd

/-- The band graph satisfies the locality hypothesis at radius `1`: nothing couples beyond
    one cell. So `FiniteRange` is not empty — a real admissible cost lives inside it. -/
theorem bandWeight_finiteRange (n : ℕ) : FiniteRange (bandWeight n) 1 := by
  intro i j hR
  simp only [bandWeight]
  exact if_neg (not_le.mpr hR)

theorem meanFieldWeight_not_finiteRange (R n : ℕ) (hn : R + 2 ≤ n) :
    ¬ FiniteRange (meanFieldWeight n) R := by
  intro hFR
  have hi : (0 : ℕ) < n := by omega
  have hj : R + 1 < n := by omega
  have hrange : R < cellDist (⟨0, hi⟩ : Fin n) (⟨R + 1, hj⟩ : Fin n) := by
    show R < Nat.dist 0 (R + 1)
    unfold Nat.dist
    omega
  have h1 := hFR ⟨0, hi⟩ ⟨R + 1, hj⟩ hrange
  simp only [meanFieldWeight] at h1
  exact one_ne_zero h1

What this page does not claim

FiniteRange does not by itself exclude screening effects without the separate dispersion step. The theorem does not derive FiniteRange from any more primitive principle; its provenance is open. The theorem says nothing about specific coupling forms like 1/r versus Yukawa, nor about constants like 5/8 or Z_eff.

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/PairKernelLocality.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: