Encyclopedia Foundation Foundation Pair Kernel Pair Cost Wpair Mean Field Far Ge One

ARTICLE 3 claims 3 theorems

Foundation Pair Kernel Pair Cost Wpair Mean Field Far Ge One

A machine-checked proof shows that two pinned points in a fully connected graph always carry at least one unit of interaction energy, a fact that separates a local from a non-local model.

Verify this page

The far-pair lower bound

In a discrete model of interaction energy, two fixed points on a graph can be forced to hold different values, and the cost of that configuration is measured by a quantity called pair cost, the minimum energy needed to keep the two points pinned apart. The declaration Wpair_meanField_far_ge_one is a proved theorem in the framework's machine-checked library of formal theorems. It states a lower bound: on a fully connected graph with three points, where every point connects to every other point with weight one, the pair cost for two points that are not adjacent is at least one. The proof is direct: the cost cannot be less than the weight of the direct link between the two pinned points, and that weight is exactly one.

This lower bound matters because it is part of a discrimination test. The framework also proves that on a local, banded graph, the same far pair has a pair cost at most one half. So the same two points, with the same pinned values, cost at least twice as much energy when the graph is fully connected than when it is local. The instrument is not flat: it detects whether the underlying coupling is short-range or long-range. The theorem is one of three inequalities that together establish this discrimination, and it is the one that sets the non-local floor.

The declaration does not claim that this lower bound holds for the full nonlinear pair kernel, which remains open. It applies only to the quadratic, Gaussian truncation of the exact action, a modeling choice. It also does not derive the continuum inverse-distance form of the interaction, nor any specific value for a physical coupling constant. The bound is a statement about a finite, discrete graph with three points, and its proof uses only the nonnegativity of the quadratic action and the direct-link weight.

THEOREM Wpair_meanField_far_ge_one · IndisputableMonolith/Foundation/PairKernelPairCost.lean
Wpair_meanField_far_ge_one · IndisputableMonolith/Foundation/PairKernelPairCost.lean:277 
/-- **Non-locality side of the decoy gate.** On the mean-field (all-to-all) graph the same far pair
    `(0,2)` still pays the full direct coupling `w = 1`, so `W ≥ 1` regardless of separation. -/
theorem Wpair_meanField_far_ge_one :
    (1:ℝ) ≤ Wpair (meanFieldWeight 3) (0 : Fin 3) (2 : Fin 3) := by
  have hab : (0 : Fin 3) ≠ (2 : Fin 3) := by decide
  have h := Wpair_ge_weight (meanFieldWeight 3) hab
  have hw : (meanFieldWeight 3).weight (0 : Fin 3) (2 : Fin 3) = 1 := rfl
  rwa [hw] at h
THEOREM Wpair_band_far_le_half · IndisputableMonolith/Foundation/PairKernelPairCost.lean
Wpair_band_far_le_half · IndisputableMonolith/Foundation/PairKernelPairCost.lean:289 
/-- **Locality side of the decoy gate.** On the band (nearest-neighbor) graph, the far pair `(0,2)`
    costs at most `1/2`: the field relaxes through the intermediate site, so distant defects couple
    weakly. Proved by exhibiting the ramp config (upper bound on the infimum). -/
theorem Wpair_band_far_le_half :
    Wpair (bandWeight 3) (0 : Fin 3) (2 : Fin 3) ≤ 1 / 2 := by
  rw [Wpair_eq_pairMin]
  have hab : (0 : Fin 3) ≠ (2 : Fin 3) := by decide
  have hmem : ramp3 (0 : Fin 3) = 1 ∧ ramp3 (2 : Fin 3) = 0 := by
    constructor <;> simp [ramp3]
  have hbdd : BddBelow
      (Set.range (fun ε : PinnedPair 3 (0:Fin 3) (2:Fin 3) => laplacian_action (bandWeight 3) ε.val)) := by
    refine ⟨0, ?_⟩; rintro x ⟨ε, rfl⟩; exact laplacian_action_nonneg _ ε.val
  have hle : pairMin (bandWeight 3) (0:Fin 3) (2:Fin 3) ≤ laplacian_action (bandWeight 3) ramp3 := by
    unfold pairMin
    exact ciInf_le hbdd (⟨ramp3, hmem⟩ : PinnedPair 3 (0:Fin 3) (2:Fin 3))
  have hval : laplacian_action (bandWeight 3) ramp3 = 1 / 2 := by
    have r0 : ramp3 (0 : Fin 3) = 1 := rfl
    have r1 : ramp3 (1 : Fin 3) = 1 / 2 := rfl
    have r2 : ramp3 (2 : Fin 3) = 0 := rfl
    have w : ∀ i j : Fin 3,
        (bandWeight 3).weight i j = if cellDist i j ≤ 1 then (1 : ℝ) else 0 := fun _ _ => rfl
    have w00 : (bandWeight 3).weight (0 : Fin 3) (0 : Fin 3) = 1 := by rw [w]; rw [if_pos (by decide)]
    have w01 : (bandWeight 3).weight (0 : Fin 3) (1 : Fin 3) = 1 := by rw [w]; rw [if_pos (by decide)]
    have w02 : (bandWeight 3).weight (0 : Fin 3) (2 : Fin 3) = 0 := by rw [w]; rw [if_neg (by decide)]
    have w10 : (bandWeight 3).weight (1 : Fin 3) (0 : Fin 3) = 1 := by rw [w]; rw [if_pos (by decide)]
    have w11 : (bandWeight 3).weight (1 : Fin 3) (1 : Fin 3) = 1 := by rw [w]; rw [if_pos (by decide)]
    have w12 : (bandWeight 3).weight (1 : Fin 3) (2 : Fin 3) = 1 := by rw [w]; rw [if_pos (by decide)]
    have w20 : (bandWeight 3).weight (2 : Fin 3) (0 : Fin 3) = 0 := by rw [w]; rw [if_neg (by decide)]
    have w21 : (bandWeight 3).weight (2 : Fin 3) (1 : Fin 3) = 1 := by rw [w]; rw [if_pos (by decide)]
    have w22 : (bandWeight 3).weight (2 : Fin 3) (2 : Fin 3) = 1 := by rw [w]; rw [if_pos (by decide)]
    simp only [laplacian_action, Fin.sum_univ_three,
      w00, w01, w02, w10, w11, w12, w20, w21, w22, r0, r1, r2]
    norm_num
  rw [hval] at hle
  exact hle
THEOREM Wpair_ge_weight · IndisputableMonolith/Foundation/PairKernelPairCost.lean
Wpair_ge_weight · IndisputableMonolith/Foundation/PairKernelPairCost.lean:220 
theorem Wpair_ge_weight {n : ℕ} (G : WeightedLedgerGraph n) {a b : Fin n} (hab : a ≠ b) :
    G.weight a b ≤ Wpair G a b := by
  rw [Wpair_eq_pairMin]; exact pairMin_ge_weight G hab

What this page does not claim

The lower bound applies only to the quadratic approximation of the action, not the full nonlinear pair kernel. The theorem does not derive the continuum inverse-distance form of the interaction. The result is specific to a graph with three points and does not generalize to other sizes without further proof.

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