Encyclopedia Foundation Foundation Pair Kernel Atomic Tick Countermodels Separated Centers Have Disjoint

ARTICLE 5 claims 5 theorems

Foundation Pair Kernel Atomic Tick Countermodels Separated Centers Have Disjoint

If two sites in a three-dimensional lattice are far enough apart, they cannot both depend on the same third site.

Verify this page

Disjoint dependency neighborhoods

In the Recognition Science framework, a ledger, a discrete record of recognition events, tracks which sites influence which. A site-indexed generator declares its dependencies: a site's update may read only sites it lists. The declaration separated_centers_have_disjoint_dependencies proves a geometric consequence of that declared locality. If two sites are separated by more than twice the dependency radius, the theorem forces their dependency neighborhoods to be disjoint. No site can be depended on by both.

The proof rests on the triangle inequality for the encoded D=3 metric, the distance function on a three-dimensional lattice. The theorem is target-blind: it never mentions range cutoffs, Green functions, or any long-distance law. It states only what operational locality, a bounded dependency relation, implies about separated sites. The exclusion witness is the all-pairs dependency, which fails operational locality on any nontrivial box. This is what separates a genuinely local generator from one that merely appears local.

The committed D=3 box generator satisfies the operational premise at radius one. Its dependency relation is bounded, so the disjointness theorem applies. The generator's weights are supported on those dependencies, and the export finiteRangeOn_export_v1 proves bounded support for the generator weights. No range predicate is placed on a Green response; the theorem concerns only declared dependencies, not the inverse problem. The framework models locality as a property of the generator's declared action graph, not as a property of the solution.

THEOREM separated_centers_have_disjoint_dependencies · IndisputableMonolith/Foundation/PairKernelAtomicTickCountermodels.lean
separated_centers_have_disjoint_dependencies · IndisputableMonolith/Foundation/PairKernelAtomicTickCountermodels.lean:145 
/-- **Independent consequence of operational locality.** Centers farther
apart than twice the dependency radius cannot share a dependency site. This
does not state a range property of weights and does not mention Green
response. -/
theorem separated_centers_have_disjoint_dependencies
    {L radius : ℕ}
    {dependency :
      Fin (L * L * L) → Fin (L * L * L) → Prop}
    (hlocal : LocalOperationalDependency3 L radius dependency)
    {a b : Fin (L * L * L)}
    (hsep : radius + radius < encodedDist3 L a b) :
    ¬ ∃ x, dependency a x ∧ dependency b x := by
  rintro ⟨x, hax, hbx⟩
  have hax' : encodedDist3 L a x ≤ radius := hlocal a x hax
  have hbx' : encodedDist3 L b x ≤ radius := hlocal b x hbx
  have hxb' : encodedDist3 L x b ≤ radius := by
    rw [encodedDist3_comm]
    exact hbx'
  have htri := encodedDist3_triangle L a x b
  omega
THEOREM encodedDist3_triangle · IndisputableMonolith/Foundation/PairKernelAtomicTickCountermodels.lean
encodedDist3_triangle · IndisputableMonolith/Foundation/PairKernelAtomicTickCountermodels.lean:139 
/-- Triangle inequality after encoding the D=3 carrier into `Fin (L³)`. -/
theorem encodedDist3_triangle
    (L : ℕ) (i j k : Fin (L * L * L)) :
    encodedDist3 L i k ≤ encodedDist3 L i j + encodedDist3 L j k := by
  exact dist3_triangle ((enc3 L).symm i) ((enc3 L).symm j) ((enc3 L).symm k)
THEOREM allPairsDependency_not_local3 · IndisputableMonolith/Foundation/PairKernelAtomicTickCountermodels.lean
allPairsDependency_not_local3 · IndisputableMonolith/Foundation/PairKernelAtomicTickCountermodels.lean:172 
/-- On any nontrivial D=3 box, the all-pairs dependency is not radius-one
operational locality. This is the exclusion witness for the new premise. -/
theorem allPairsDependency_not_local3 (L : ℕ) (hL : 2 ≤ L) :
    ¬ LocalOperationalDependency3 L 1
      (allPairsDependency :
        Fin (L * L * L) → Fin (L * L * L) → Prop) := by
  intro hlocal
  let o : Site3 L :=
    ((⟨0, by omega⟩, ⟨0, by omega⟩), ⟨0, by omega⟩)
  let e : Site3 L :=
    ((⟨1, by omega⟩, ⟨1, by omega⟩), ⟨0, by omega⟩)
  have hle : encodedDist3 L (enc3 L o) (enc3 L e) ≤ 1 :=
    hlocal (enc3 L o) (enc3 L e) trivial
  have hdist : encodedDist3 L (enc3 L o) (enc3 L e) = 2 := by
    simp only [encodedDist3, Equiv.symm_apply_apply, dist3, o, e]
    unfold Nat.dist
    omega
  omega
THEOREM lattice3Generator_operationally_local · IndisputableMonolith/Foundation/PairKernelAtomicTickCountermodels.lean
lattice3Generator_operationally_local · IndisputableMonolith/Foundation/PairKernelAtomicTickCountermodels.lean:200 
/-- The D=3 generator dependency satisfies the operational premise at radius
one. This is theorem-grade for the committed box geometry, not a derivation
that production physics must choose that geometry. -/
theorem lattice3Generator_operationally_local (L : ℕ) :
    LocalOperationalDependency3 L 1
      (lattice3Generator L).dependency :=
  lattice3RecognitionRelation_bounded L
THEOREM lattice3Generator_finiteRangeOn · IndisputableMonolith/Foundation/PairKernelAtomicTickCountermodels.lean
lattice3Generator_finiteRangeOn · IndisputableMonolith/Foundation/PairKernelAtomicTickCountermodels.lean:218 
/-- **Consumer-changing export.** Operational locality plus declared weight
support feeds the S2 metric export and proves `FiniteRangeOn` for the local
generator weights. No range predicate is placed on a Green response. -/
theorem lattice3Generator_finiteRangeOn (L : ℕ) :
    FiniteRangeOn
      (lattice3Generator L).graph (encodedDist3 L) 1 :=
  finiteRangeOn_export_v1
    (lattice3Generator_operationally_local L)
    (lattice3Generator L).weight_uses_dependency

What this page does not claim

The theorem does not place any range bound on a Green response. The theorem does not prove that production physics must choose the D=3 box geometry. The theorem does not establish that the all-pairs dependency is impossible, only that it fails operational locality.

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