Encyclopedia Foundation Foundation Pair Kernel Pair Cost Band Dirichlet Eq Adjacent

ARTICLE 2 claims 2 theorems

Foundation Pair Kernel Pair Cost Band Dirichlet Eq Adjacent

A machine-checked theorem gives a simple formula for the interaction energy of two pinned points on a line, and it is careful about what it does not say.

Verify this page

A band's cost formula

In the Recognition Science framework, a ledger (a discrete record of events on a graph) carries a cost for each configuration of values on its nodes. The declaration bandDirichlet_eq_adjacent proves a clean identity: on a graph where nodes are arranged on a line and each node connects only to its immediate neighbors, the cost of a configuration equals the sum of squared differences between adjacent values. In symbols, for a function g on the nodes, the cost is Σ (g(a) − g(a+1))². This is a THEOREM: it is derived from the definition of the cost and the band graph structure, with no additional assumptions.

The theorem matters because it makes the cost concrete and computable on the simplest nontrivial graph. It shows that the cost penalizes sharp changes between neighboring nodes: a configuration where values change rapidly has a high cost, while a flat configuration has zero cost. This is the discrete analogue of a smoothness penalty. The theorem also feeds into a larger result: on a three-node band graph, the interaction energy between two pinned points is positive for adjacent points and smaller for points separated by one node, so the cost genuinely depends on distance. The declaration is a building block, not the final story.

What the theorem does not claim is just as important. It says nothing about the full nonlinear interaction energy, which remains an open problem. It does not derive the continuum 1/(4πr) form of a Green's function, nor does it compare 1/r decay with a Yukawa potential. Those are separate targets. The theorem works only with the quadratic, Gaussian truncation of the exact cost, which is a modeling choice, not a derived law. And it applies to band graphs on a line, not to arbitrary graphs or to the mean-field graph where every node connects to every other.

In the framework's own terms, this theorem is a vertebra in a longer spine: it establishes a concrete, non-vacuous interaction energy that can discriminate between local and non-local couplings. For a reader, the payoff is a precise, checkable statement about how cost behaves on a simple graph, and a clear boundary around what remains to be proved.

THEOREM bandDirichlet_eq_adjacent · IndisputableMonolith/Foundation/PairKernelPairCost.lean
bandDirichlet_eq_adjacent · IndisputableMonolith/Foundation/PairKernelPairCost.lean:440 
/-- **Band Dirichlet energy = sum of squared adjacent differences.** For any index-function `g`, the
    quadratic action on the nearest-neighbor band graph collapses to the 1D chain energy
    `∑ (g a − g (a+1))²` over adjacent links. The double sum over all pairs reduces to nearest
    neighbors because the band weight vanishes beyond range 1. -/
theorem bandDirichlet_eq_adjacent {n : ℕ} (g : ℕ → ℝ) :
    laplacian_action (bandWeight n) (fun i => g i.val)
      = ∑ a ∈ Finset.range (n - 1), (g a - g (a + 1)) ^ 2 := by
  have peel : ∀ (h : ℕ → ℝ),
      (∑ a ∈ Finset.range n, if a + 1 ∈ Finset.range n then h a else 0)
        = ∑ a ∈ Finset.range (n - 1), h a := by
    intro h
    cases n with
    | zero => simp
    | succ m =>
      rw [Finset.sum_range_succ, Nat.succ_sub_one, if_neg (by simp [Finset.mem_range]), add_zero]
      apply Finset.sum_congr rfl
      intro a ha
      rw [Finset.mem_range] at ha
      rw [if_pos (Finset.mem_range.mpr (by omega))]
  have hconv : laplacian_action (bandWeight n) (fun i => g i.val)
      = (1 / 2) * ∑ a ∈ Finset.range n, ∑ b ∈ Finset.range n,
          (if Nat.dist a b ≤ 1 then (1:ℝ) else 0) * (g a - g b) ^ 2 := by
    unfold laplacian_action
    congr 1
    rw [← Fin.sum_univ_eq_sum_range (fun a => ∑ b ∈ Finset.range n,
          (if Nat.dist a b ≤ 1 then (1:ℝ) else 0) * (g a - g b) ^ 2) n]
    apply Finset.sum_congr rfl; intro i _
    rw [← Fin.sum_univ_eq_sum_range (fun b =>
          (if Nat.dist i.val b ≤ 1 then (1:ℝ) else 0) * (g i.val - g b) ^ 2) n]
    apply Finset.sum_congr rfl; intro j _
    rfl
  rw [hconv]
  have hrw : (∑ a ∈ Finset.range n, ∑ b ∈ Finset.range n,
        (if Nat.dist a b ≤ 1 then (1:ℝ) else 0) * (g a - g b) ^ 2)
      = ∑ a ∈ Finset.range n, ∑ b ∈ Finset.range n,
          ((if a = b then (g a - g b) ^ 2 else 0)
            + (if b = a + 1 then (g a - g b) ^ 2 else 0)
            + (if a = b + 1 then (g a - g b) ^ 2 else 0)) := by
    apply Finset.sum_congr rfl; intro a _; apply Finset.sum_congr rfl; intro b _
    exact band_indicator_decomp a b _
  have hdiag : (∑ a ∈ Finset.range n, ∑ b ∈ Finset.range n, if a = b then (g a - g b) ^ 2 else 0)
      = 0 := by
    apply Finset.sum_eq_zero; intro a _
    apply Finset.sum_eq_zero; intro b _
    by_cases h : a = b
    · simp [h]
    · simp [h]
  have hsuper : (∑ a ∈ Finset.range n, ∑ b ∈ Finset.range n, if b = a + 1 then (g a - g b) ^ 2 else 0)
      = ∑ a ∈ Finset.range (n - 1), (g a - g (a + 1)) ^ 2 := by
    have hin : ∀ a, (∑ b ∈ Finset.range n, if b = a + 1 then (g a - g b) ^ 2 else 0)
        = if a + 1 ∈ Finset.range n then (g a - g (a + 1)) ^ 2 else 0 := by
      intro a; rw [Finset.sum_ite_eq' (Finset.range n) (a + 1) (fun b => (g a - g b) ^ 2)]
    rw [Finset.sum_congr rfl (fun a _ => hin a)]
    exact peel (fun a => (g a - g (a + 1)) ^ 2)
  have hsub : (∑ a ∈ Finset.range n, ∑ b ∈ Finset.range n, if a = b + 1 then (g a - g b) ^ 2 else 0)
      = ∑ a ∈ Finset.range (n - 1), (g a - g (a + 1)) ^ 2 := by
    rw [Finset.sum_comm]
    have hin : ∀ b, (∑ a ∈ Finset.range n, if a = b + 1 then (g a - g b) ^ 2 else 0)
        = if b + 1 ∈ Finset.range n then (g (b + 1) - g b) ^ 2 else 0 := by
      intro b; rw [Finset.sum_ite_eq' (Finset.range n) (b + 1) (fun a => (g a - g b) ^ 2)]
    rw [Finset.sum_congr rfl (fun b _ => hin b), peel (fun b => (g (b + 1) - g b) ^ 2)]
    apply Finset.sum_congr rfl; intro a _; ring
  rw [hrw]
  simp only [Finset.sum_add_distrib]
  rw [hdiag, hsuper, hsub]
  ring
THEOREM band_distance_dependent · IndisputableMonolith/Foundation/PairKernelPairCost.lean
band_distance_dependent · IndisputableMonolith/Foundation/PairKernelPairCost.lean:339 
/-- Band is distance-dependent: the adjacent pair strictly outcosts the far pair. -/
theorem band_distance_dependent :
    Wpair (bandWeight 3) (0 : Fin 3) (2 : Fin 3) < Wpair (bandWeight 3) (0 : Fin 3) (1 : Fin 3) := by
  have h1 := Wpair_band_far_le_half
  have h2 := Wpair_band_adjacent_pos
  linarith

What this page does not claim

The theorem does not derive the continuum 1/(4πr) form of a Green's function. The theorem does not compare 1/r decay with a Yukawa potential. The theorem applies only to the quadratic truncation of the exact cost, not the full nonlinear cost.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND