Foundation Pair Kernel Pair Cost Pair Min Band Le Inv Dist

The inverse-distance bound

In the Recognition Science framework, a ledger is a discrete record of events, and the framework's library is a machine-checked collection of formal theorems about such records. One family of results concerns the interaction energy of two pinned defects: points where the record is forced to take fixed values. The declaration pairMin_band_le_inv_dist proves a precise bound for a specific graph, the band graph, where each point connects only to its immediate neighbors.

On a band graph with n points, take two defects separated by a distance d. The theorem states that the minimum possible interaction energy, pairMin, is at most 1/d. In plain terms, the energy between two pinned points cannot exceed the reciprocal of their separation. This is a formal, machine-checked statement: it holds for any positive distance d less than the graph size n, and the proof is complete with no gaps.

The bound matters because it is the first step toward a classical result. In continuous physics, the potential energy between two charges falls off as one over distance, the familiar Coulomb law. This theorem shows that the same inverse-distance decay emerges from a purely discrete, graph-based ledger, before any continuum limit is taken. It is a structural property of the framework's quadratic action, not a numerical coincidence.

The theorem is deliberately narrow. It applies only to the band graph, not to arbitrary graphs. It bounds the minimum energy from above; it does not say the energy equals 1/d, only that it is no larger. And it concerns the quadratic approximation to the framework's exact cost function, not the full nonlinear theory. The framework's library also proves that the energy is positive and that it distinguishes local from non-local couplings, but this particular declaration only establishes the upper bound.

What a reader can take away is this: the inverse-distance law, so familiar from electrostatics, has a discrete precursor in the Recognition Science framework, and that precursor is now a proved theorem. The result does not by itself derive the continuum Coulomb law, nor does it apply to all coupling geometries. But it is a concrete, checkable fact about how interaction energy decays on a simple chain, and it opens the door to further results in the framework's program.

/-- **General 1D decay: `pairMin (bandWeight n) 0 d ≤ 1/d`.** On the band chain, two defects at
    index-distance `d` cost at most `1/d`: the linear ramp over `d` links carries a difference `1/d`
    per link, total energy `d · (1/d)² = 1/d`. This is the closed-form kernel decay generalizing the
    three committed points (`1, 1/2, 1/3`). The 1D discrete Green's function. -/
theorem pairMin_band_le_inv_dist {n d : ℕ} (hd : 0 < d) (hdn : d < n) :
    pairMin (bandWeight n) (⟨0, by omega⟩ : Fin n) (⟨d, hdn⟩ : Fin n) ≤ 1 / (d : ℝ) := by
  have hd0 : (d : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
  set g : ℕ → ℝ := fun k => 1 - ((min k d : ℕ) : ℝ) / (d : ℝ) with hg
  have hab : (⟨0, by omega⟩ : Fin n) ≠ (⟨d, hdn⟩ : Fin n) := by
    simp only [ne_eq, Fin.mk.injEq]; omega
  haveI : Nonempty (PinnedPair n (⟨0, by omega⟩ : Fin n) (⟨d, hdn⟩ : Fin n)) :=
    pinnedPair_nonempty hab
  have hg0 : g 0 = 1 := by
    simp only [hg]; rw [min_eq_left (Nat.zero_le d)]; norm_num
  have hgd : g d = 0 := by
    simp only [hg]; rw [min_self, div_self hd0]; ring
  have hmem : (fun i => g i.val) (⟨0, by omega⟩ : Fin n) = 1
            ∧ (fun i => g i.val) (⟨d, hdn⟩ : Fin n) = 0 := ⟨hg0, hgd⟩
  have hbdd : BddBelow (Set.range (fun ε : PinnedPair n (⟨0, by omega⟩ : Fin n) (⟨d, hdn⟩ : Fin n) =>
      laplacian_action (bandWeight n) ε.val)) := by
    refine ⟨0, ?_⟩; rintro x ⟨ε, rfl⟩; exact laplacian_action_nonneg _ ε.val
  have hle : pairMin (bandWeight n) (⟨0, by omega⟩ : Fin n) (⟨d, hdn⟩ : Fin n)
           ≤ laplacian_action (bandWeight n) (fun i => g i.val) := by
    unfold pairMin
    exact ciInf_le hbdd (⟨fun i => g i.val, hmem⟩ :
      PinnedPair n (⟨0, by omega⟩ : Fin n) (⟨d, hdn⟩ : Fin n))
  have hval : laplacian_action (bandWeight n) (fun i => g i.val) = 1 / (d : ℝ) := by
    rw [bandDirichlet_eq_adjacent g]
    have hterm : ∀ a, (g a - g (a + 1)) ^ 2 = if a < d then (1 / (d : ℝ)) ^ 2 else 0 := by
      intro a
      by_cases ha : a < d
      · rw [if_pos ha]
        have hstep : g a - g (a + 1) = 1 / (d : ℝ) := by
          simp only [hg, min_eq_left (show a ≤ d by omega), min_eq_left (show a + 1 ≤ d by omega)]
          push_cast
          field_simp
          ring
        rw [hstep]
      · rw [if_neg ha]
        have hstep : g a - g (a + 1) = 0 := by
          simp only [hg, min_eq_right (show d ≤ a by omega), min_eq_right (show d ≤ a + 1 by omega)]
          ring
        rw [hstep]; ring
    rw [Finset.sum_congr rfl (fun a _ => hterm a)]
    have hcard : ((Finset.range (n - 1)).filter (fun a => a < d)) = Finset.range d := by
      ext a; simp only [Finset.mem_filter, Finset.mem_range]; omega
    rw [← Finset.sum_filter, hcard, Finset.sum_const, Finset.card_range, nsmul_eq_mul]
    field_simp
  calc pairMin (bandWeight n) (⟨0, by omega⟩ : Fin n) (⟨d, hdn⟩ : Fin n)
      ≤ laplacian_action (bandWeight n) (fun i => g i.val) := hle
    _ = 1 / (d : ℝ) := hval

What this page does not claim

The theorem does not claim that the pair energy equals 1/d, only that it is bounded above by 1/d. The theorem does not apply to arbitrary graphs; it is specific to the band graph. The theorem does not derive the full nonlinear pair kernel, which remains open.

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: