Foundation Pair Kernel Pair Cost Pair Kernel Discriminates

The discriminating pair cost

The declaration pairKernel_discriminates is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It states a precise, finite fact: for a system of three points, the two-body interaction cost W(a,b), defined as the minimum energy needed to pin one point to value 1 and another to value 0 while letting the rest relax, is bounded below by 1 for adjacent points on a local (band) graph, at most 1/2 for distant points on that same graph, and at least 1 for distant points on a non-local (mean-field) graph where every point connects to every other. The theorem is proved in the Lean 4 proof assistant with zero axioms beyond the standard three, and it is the framework's first concrete demonstration that its pair cost is not a vacuous or flat instrument.

The classical background here is the Dirichlet principle: given a graph with edge weights, the energy of a field is the sum over edges of the weight times the squared difference of the field values. Pinning two points to different values forces the field to bend, and the minimal bending energy is the pair cost. The framework's contribution is to show that this cost, built from its own ledger of recognition events, satisfies the inequalities above. On a band graph where only adjacent points interact, the cost drops from at least 1 for neighbors to at most 1/2 for points two steps apart, so it is distance-dependent. On a mean-field graph where every pair interacts, the same distant pair costs at least 1, strictly more than the band graph's 1/2. The pair cost therefore discriminates: it sees whether the underlying coupling is local or non-local.

The proof is not a tautology. It uses the fact that the gradient current, defined as the edge weight times the field difference, is antisymmetric, and its divergence is the discrete Laplacian. The sum of the discrete Laplacian over all points is zero, which makes the pinned-source field neutral and the minimization problem bounded below. The theorem also guards against a null trap: without pinning, the cost would be identically zero; with pinning, the direct link term survives every relaxation, so the cost is genuinely positive. The framework's library proves these lemmas in full, with no gaps.

What the theorem does not claim is as important as what it proves. It does not establish the continuum inverse-square form 1/(4πr²), which is a separate, numerically measured limit. It does not derive the full nonlinear pair kernel, which remains an open target. It does not link the pair cost to any specific physical constants such as 5/8 or 27/16, which appear nowhere in the proof. The theorem is a finite, discrete statement about three points on two specific graphs, and its power is that it shows the framework's cost function is a genuine, informative interaction energy, not a flat or trivial one. That is the first rung on the ladder toward forces.

/-- **The pair kernel discriminates local from non-local coupling (the decoy gate passes).**
    (i) Non-vacuous: `W_band(0,1) ≥ 1`. (ii) Local/cheap far: `W_band(0,2) ≤ 1/2`. (iii)
    Non-local/full-price far: `W_meanField(0,2) ≥ 1`. Consequences (arithmetic): band-adjacent
    `≥ 1 > 1/2 ≥` band-far, so `W` is distance-dependent (not flat) on the local graph; and
    band-far `≤ 1/2 < 1 ≤` mean-field-far, so the SAME far pair is strictly cheaper on the local
    graph than on the non-local one. Instrument INFORMATIVE. -/
theorem pairKernel_discriminates :
    (1:ℝ) ≤ Wpair (bandWeight 3) (0 : Fin 3) (1 : Fin 3) ∧
    Wpair (bandWeight 3) (0 : Fin 3) (2 : Fin 3) ≤ 1 / 2 ∧
    (1:ℝ) ≤ Wpair (meanFieldWeight 3) (0 : Fin 3) (2 : Fin 3) :=
  ⟨Wpair_band_adjacent_pos, Wpair_band_far_le_half, Wpair_meanField_far_ge_one⟩

/-- **The pair kernel discriminates local from non-local coupling (the decoy gate passes).**
    (i) Non-vacuous: `W_band(0,1) ≥ 1`. (ii) Local/cheap far: `W_band(0,2) ≤ 1/2`. (iii)
    Non-local/full-price far: `W_meanField(0,2) ≥ 1`. Consequences (arithmetic): band-adjacent
    `≥ 1 > 1/2 ≥` band-far, so `W` is distance-dependent (not flat) on the local graph; and
    band-far `≤ 1/2 < 1 ≤` mean-field-far, so the SAME far pair is strictly cheaper on the local
    graph than on the non-local one. Instrument INFORMATIVE. -/
theorem pairKernel_discriminates :
    (1:ℝ) ≤ Wpair (bandWeight 3) (0 : Fin 3) (1 : Fin 3) ∧
    Wpair (bandWeight 3) (0 : Fin 3) (2 : Fin 3) ≤ 1 / 2 ∧
    (1:ℝ) ≤ Wpair (meanFieldWeight 3) (0 : Fin 3) (2 : Fin 3) :=
  ⟨Wpair_band_adjacent_pos, Wpair_band_far_le_half, Wpair_meanField_far_ge_one⟩

/-- 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

/-- **Induced σ-source is discrete-Gauss-neutral.** The recognition current of a pinned-defect field
    is antisymmetric, so the general Gauss law `sum_divF_zero` forces its total divergence to zero.
    This uses the (arbitrary-antisymmetric) Gauss law on a gradient instance — not the `grad φ`
    tautology. The neutrality is what makes the dual source-coupled cost bounded below. -/
theorem pinned_source_neutral {n : ℕ} (G : WeightedLedgerGraph n) (ε : Fin n → ℝ) :
    ∑ i : Fin n, discrete_laplacian G ε i = 0 := by
  have h := sum_divF_zero (gradientCurrent_antisym G ε)
  rw [← h]
  apply Finset.sum_congr rfl
  intro i _
  exact (gradientCurrent_divF_eq G ε i).symm

What this page does not claim

The theorem does not derive the continuum 1/(4πr²) form, which is a separate numerically measured limit. The theorem does not establish the full nonlinear pair kernel, which remains an open target. The theorem does not use or imply any specific physical constants such as 5/8 or 27/16.

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: