Encyclopedia Foundation Foundation Pair Kernel Pair Cost Wpair Band Dist3 Le Third

ARTICLE 4 claims 4 theorems

Foundation Pair Kernel Pair Cost Wpair Band Dist3 Le Third

A machine-checked theorem places an upper limit on the interaction energy of two pinned defects in a discrete ledger, a small step toward showing how locality shapes cost.

Verify this page

A bound on interaction energy

The declaration Wpair_band_dist3_le_third is a theorem about a specific mathematical object: the interaction energy, denoted W, between two pinned points in a discrete weighted graph. The graph has four vertices arranged in a line, and the weight of an edge is 1 if the vertices are adjacent and 0 otherwise. The theorem states that for this graph, the interaction energy between the first and fourth vertices is at most one third. This is a precise, formal statement, proved in a machine-checked library of formal theorems.

To understand what this means, consider the framework's model. The framework models a physical system as a ledger, a discrete record of events. Here, the interaction energy W is defined as the minimum cost of a field configuration subject to two constraints: the field has value 1 at one vertex and 0 at another. This cost is the quadratic action, a measure of how much the field varies across the graph. The theorem Wpair_band_dist3_le_third is one instance of a more general pattern: for a line of n vertices, the interaction energy between the first and d-th vertex is at most 1/d. This is a discrete analogue of an inverse-distance decay, a hallmark of local interactions.

The theorem is part of a larger effort to show that the framework's cost function is not vacuous. It is a guard against a potential flaw: the interaction energy could be zero for far-apart points, which would mean the model measures nothing. The theorem, along with others, shows that the energy is positive for adjacent points and decreases with distance, so the model is informative. The theorem also helps distinguish a local coupling, where only nearby points interact, from a non-local one, where all points interact. For the same far pair, the interaction energy is strictly larger in the non-local case.

Importantly, the theorem does not claim that the interaction energy follows an exact inverse-distance law. It only provides an upper bound. The full nonlinear interaction kernel, beyond the quadratic approximation used here, remains an open target. The theorem also does not imply anything about the continuum limit, such as the familiar 1/(4πr) form of a Green's function, which is a separate, numerically measured result. The theorem is a precise, limited statement about a discrete model, and it is a building block, not a complete physical law.

THEOREM Wpair_band_dist3_le_third · IndisputableMonolith/Foundation/PairKernelPairCost.lean
Wpair_band_dist3_le_third · IndisputableMonolith/Foundation/PairKernelPairCost.lean:366 
/-- **Distance-3 decay.** On the band graph the pair at index-distance `3` costs at most `1/3`
    (the ramp over three links). Together with `W_band(0,1) ≥ 1` and `W_band(0,2) ≤ 1/2` this is
    the discrete `1/d` law `1, 1/2, 1/3, …` — the lattice precursor of the continuum `1/r`. -/
theorem Wpair_band_dist3_le_third :
    Wpair (bandWeight 4) (0 : Fin 4) (3 : Fin 4) ≤ 1 / 3 := by
  rw [Wpair_eq_pairMin]
  have hmem : ramp4 (0 : Fin 4) = 1 ∧ ramp4 (3 : Fin 4) = 0 := ⟨rfl, rfl⟩
  have hbdd : BddBelow
      (Set.range (fun ε : PinnedPair 4 (0:Fin 4) (3:Fin 4) => laplacian_action (bandWeight 4) ε.val)) := by
    refine ⟨0, ?_⟩; rintro x ⟨ε, rfl⟩; exact laplacian_action_nonneg _ ε.val
  have hle : pairMin (bandWeight 4) (0:Fin 4) (3:Fin 4) ≤ laplacian_action (bandWeight 4) ramp4 := by
    unfold pairMin
    exact ciInf_le hbdd (⟨ramp4, hmem⟩ : PinnedPair 4 (0:Fin 4) (3:Fin 4))
  have hval : laplacian_action (bandWeight 4) ramp4 = 1 / 3 := by
    have r0 : ramp4 (0 : Fin 4) = 1 := rfl
    have r1 : ramp4 (1 : Fin 4) = 2 / 3 := rfl
    have r2 : ramp4 (2 : Fin 4) = 1 / 3 := rfl
    have r3 : ramp4 (3 : Fin 4) = 0 := rfl
    have w : ∀ i j : Fin 4,
        (bandWeight 4).weight i j = if cellDist i j ≤ 1 then (1 : ℝ) else 0 := fun _ _ => rfl
    have w00 : (bandWeight 4).weight (0:Fin 4) (0:Fin 4) = 1 := by rw [w]; rw [if_pos (by decide)]
    have w01 : (bandWeight 4).weight (0:Fin 4) (1:Fin 4) = 1 := by rw [w]; rw [if_pos (by decide)]
    have w02 : (bandWeight 4).weight (0:Fin 4) (2:Fin 4) = 0 := by rw [w]; rw [if_neg (by decide)]
    have w03 : (bandWeight 4).weight (0:Fin 4) (3:Fin 4) = 0 := by rw [w]; rw [if_neg (by decide)]
    have w10 : (bandWeight 4).weight (1:Fin 4) (0:Fin 4) = 1 := by rw [w]; rw [if_pos (by decide)]
    have w11 : (bandWeight 4).weight (1:Fin 4) (1:Fin 4) = 1 := by rw [w]; rw [if_pos (by decide)]
    have w12 : (bandWeight 4).weight (1:Fin 4) (2:Fin 4) = 1 := by rw [w]; rw [if_pos (by decide)]
    have w13 : (bandWeight 4).weight (1:Fin 4) (3:Fin 4) = 0 := by rw [w]; rw [if_neg (by decide)]
    have w20 : (bandWeight 4).weight (2:Fin 4) (0:Fin 4) = 0 := by rw [w]; rw [if_neg (by decide)]
    have w21 : (bandWeight 4).weight (2:Fin 4) (1:Fin 4) = 1 := by rw [w]; rw [if_pos (by decide)]
    have w22 : (bandWeight 4).weight (2:Fin 4) (2:Fin 4) = 1 := by rw [w]; rw [if_pos (by decide)]
    have w23 : (bandWeight 4).weight (2:Fin 4) (3:Fin 4) = 1 := by rw [w]; rw [if_pos (by decide)]
    have w30 : (bandWeight 4).weight (3:Fin 4) (0:Fin 4) = 0 := by rw [w]; rw [if_neg (by decide)]
    have w31 : (bandWeight 4).weight (3:Fin 4) (1:Fin 4) = 0 := by rw [w]; rw [if_neg (by decide)]
    have w32 : (bandWeight 4).weight (3:Fin 4) (2:Fin 4) = 1 := by rw [w]; rw [if_pos (by decide)]
    have w33 : (bandWeight 4).weight (3:Fin 4) (3:Fin 4) = 1 := by rw [w]; rw [if_pos (by decide)]
    simp only [laplacian_action, Fin.sum_univ_four,
      w00, w01, w02, w03, w10, w11, w12, w13, w20, w21, w22, w23, w30, w31, w32, w33,
      r0, r1, r2, r3]
    norm_num
  rw [hval] at hle
  exact hle
THEOREM Wpair_band_le_inv_dist · IndisputableMonolith/Foundation/PairKernelPairCost.lean
Wpair_band_le_inv_dist · IndisputableMonolith/Foundation/PairKernelPairCost.lean:559 
/-- The two-body cost `Wpair` inherits the general `1/d` decay (since `Wpair = pairMin`). The kernel
    of two defects at index-distance `d` on the band chain is `≤ 1/d` for every `0 < d < n`. -/
theorem Wpair_band_le_inv_dist {n d : ℕ} (hd : 0 < d) (hdn : d < n) :
    Wpair (bandWeight n) (⟨0, by omega⟩ : Fin n) (⟨d, hdn⟩ : Fin n) ≤ 1 / (d : ℝ) := by
  rw [Wpair_eq_pairMin]; exact pairMin_band_le_inv_dist hd hdn
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
THEOREM local_below_nonlocal · IndisputableMonolith/Foundation/PairKernelPairCost.lean
local_below_nonlocal · IndisputableMonolith/Foundation/PairKernelPairCost.lean:346 
/-- Locality separation: the same far pair is strictly cheaper on the local (band) graph than on
    the non-local (mean-field) graph. -/
theorem local_below_nonlocal :
    Wpair (bandWeight 3) (0 : Fin 3) (2 : Fin 3) < Wpair (meanFieldWeight 3) (0 : Fin 3) (2 : Fin 3) := by
  have h1 := Wpair_band_far_le_half
  have h2 := Wpair_meanField_far_ge_one
  linarith

What this page does not claim

The interaction energy follows an exact inverse-distance law. The result applies to the continuum limit or to the full nonlinear interaction kernel. The theorem implies anything about the framework's constants or particle masses.

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