Foundation Pair Kernel Atomic Tick Countermodels Dist3 Triangle

The distance inequality

The triangle inequality is a familiar fact about ordinary space: the direct distance between two points is never more than the distance traveled through a third point. In a three-dimensional grid, where positions are labeled by whole-number coordinates, this inequality takes the form dist3 p r ≤ dist3 p q + dist3 q r, meaning the shortest path between two grid sites is no longer than any path that stops at an intermediate site. The declaration dist3_triangle in the Recognition Science library is a machine-checked proof of exactly this statement for the grid metric used in the framework's three-dimensional model.

The proof matters because the framework builds its picture of space from a discrete record of events, called a ledger, where each step records which site posts a recognition event. The grid metric dist3 measures distance between sites in this ledger. Establishing the triangle inequality for this metric is a prerequisite for treating the grid as a genuine geometric space: without it, statements about neighborhoods, separation, and locality would not behave as ordinary geometry requires. The theorem also has an encoded version, encodedDist3_triangle, which states the same inequality after translating grid coordinates into a flat list of positions, the form used in the framework's formal computations.

In Recognition Science, the triangle inequality is not an isolated curiosity. It underpins a locality premise called LocalOperationalDependency3: the assumption that one site's generator depends only on sites within a bounded radius. From this premise, the framework proves that two centers separated by more than twice the dependency radius cannot share any dependency site. The triangle inequality is what makes this separation argument work, since it guarantees that the path through a shared site cannot be shorter than the direct distance. The framework also shows that the all-pairs dependency, where every site depends on every other, fails this locality condition, and that a specific lattice generator satisfies it at radius one.

What dist3_triangle does not claim is equally important. It does not assert that physical space is three-dimensional, that the grid metric is the unique or correct model of space, or that the locality premise is true of the actual universe. The theorem is a formal statement about a defined metric, not an empirical claim. The framework's broader argument that three dimensions are forced by recognition dynamics is a separate, larger claim that this triangle inequality merely supports as one component. The theorem also does not say anything about the Green function or response behavior; it concerns only the distance metric itself.

/-- Triangle inequality for the D=3 `ℓ¹` metric. -/
theorem dist3_triangle {L : ℕ} (p q r : Site3 L) :
    dist3 p r ≤ dist3 p q + dist3 q r := by
  have hx :
      Nat.dist p.1.1.val r.1.1.val ≤
        Nat.dist p.1.1.val q.1.1.val + Nat.dist q.1.1.val r.1.1.val := by
    unfold Nat.dist
    omega
  have hy :
      Nat.dist p.1.2.val r.1.2.val ≤
        Nat.dist p.1.2.val q.1.2.val + Nat.dist q.1.2.val r.1.2.val := by
    unfold Nat.dist
    omega
  have hz :
      Nat.dist p.2.val r.2.val ≤
        Nat.dist p.2.val q.2.val + Nat.dist q.2.val r.2.val := by
    unfold Nat.dist
    omega
  unfold dist3
  omega

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

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

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

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

What this page does not claim

The theorem does not assert that physical space is three-dimensional. The theorem does not claim the grid metric is the unique or correct model of space. The theorem does not state any property of Green functions or response behavior.

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: