Foundation Pair Kernel Locality Mean Field Ledger Cost Not Finite Range

The locality hypothesis

In the Recognition Science framework, a ledger (a discrete record of events) assigns weights to pairs of sites, and the question is how far apart two sites can be while still influencing each other. The locality hypothesis FiniteRange states that the weight between two sites is zero once their index distance exceeds a fixed radius R. This is a postulate, not a derived result; the framework does not yet prove that such a range cutoff must exist.

The declaration meanFieldLedgerCost_not_finiteRange proves a specific negative fact: the mean-field ledger cost, which couples every pair of sites with equal weight, violates FiniteRange at every fixed radius once the carrier is large enough. Concretely, for any radius R, if the number of sites n is at least R + 2, then sites 0 and R + 1 are more than R cells apart yet still coupled with weight 1. This matters because the mean-field graph is the carrier of a screening honest-negative: a counterexample that survives an earlier shift-invariance condition. The locality hypothesis rejects exactly that counterexample, so it is load-bearing rather than vacuous.

The same module also proves the hypothesis is not empty. A nearest-neighbor band graph, which couples only adjacent sites, is an admissible ledger graph and satisfies FiniteRange 1. It is non-trivial: adjacent sites do couple with weight 1. Together, the two theorems bundle into finiteRange_is_discriminating, showing that the locality condition is satisfiable and discriminating.

What the declaration does not claim is equally precise. It does not prove that the locality hypothesis excludes screening; that step requires a dispersion or Fourier analysis that remains numerical in the framework's harness, not a formal theorem. It does not derive the range cutoff from any more primitive principle; the provenance of FiniteRange is an open target. And it makes no claim about specific coupling forms like 1/r versus Yukawa, nor about any hydrogenic quantities.

/-- The same teeth, stated on the built honest-negative cost `meanFieldLedgerCost`: its
    weight graph (`meanFieldWeight`) is not finite-range. This is the direct link — L0 is
    exactly the hypothesis that rejects the screening carrier that survives L1. -/
theorem meanFieldLedgerCost_not_finiteRange (R n : ℕ) (hn : R + 2 ≤ n) :
    ¬ FiniteRange (meanFieldLedgerCost n).G R :=
  meanFieldWeight_not_finiteRange R n hn

/-- The band graph satisfies the locality hypothesis at radius `1`: nothing couples beyond
    one cell. So `FiniteRange` is not empty — a real admissible cost lives inside it. -/
theorem bandWeight_finiteRange (n : ℕ) : FiniteRange (bandWeight n) 1 := by
  intro i j hR
  simp only [bandWeight]
  exact if_neg (not_le.mpr hR)

/-- **L0 status bundle.** `FiniteRange` is (a) satisfiable by an admissible non-trivial
    graph (the band graph, radius `1`), and (b) violated by the mean-field graph that
    carries the built screening honest-negative (at every fixed radius, for large enough
    carriers). A hypothesis with both properties is neither vacuous nor trivially true: it
    does real work. It remains HYPOTHESIS-tier — its RS provenance (a forced range cutoff)
    is OPEN. -/
theorem finiteRange_is_discriminating :
    (∀ n, FiniteRange (bandWeight n) 1) ∧
      (∀ R n, R + 2 ≤ n → ¬ FiniteRange (meanFieldWeight n) R) :=
  ⟨bandWeight_finiteRange, meanFieldWeight_not_finiteRange⟩

What this page does not claim

The locality hypothesis excludes screening; that step remains numerical. The finite-range cutoff is derived from any more primitive principle. Any specific coupling form like 1/r versus Yukawa follows from this declaration.

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