Foundation Pair Kernel Operational Locality S4 Tiled Jminimal Generator Finite R

A finite reach from minimal cost

A ledger, a discrete record of events, can change in many ways. This theorem concerns the cheapest possible changes, those that minimize a specific cost function called Jlog. The framework's earlier work proved that a minimal-cost change is always a single posting: it alters exactly one entry. This declaration, tiledJMinimalGenerator_finiteRangeOn, takes that result and applies it to a three-dimensional grid of cells. It states that if you build a process where every allowed transition is such a minimal-cost posting, then the process has a finite range: any cell can only influence other cells within a fixed, bounded distance, in this case a distance of one.

The proof works by translating the one-bit motion result into the larger grid. The theorem tiledJMinimalDependency3_operationally_local establishes that the dependency relation, defined by realizable minimal-cost transitions, is local. The declaration in question then exports this locality to a statement about any weighted graph whose non-zero edges are all such minimal transitions: it must satisfy FiniteRangeOn with radius one. This means the influence of any single cell cannot jump across the grid; it is confined to its immediate neighborhood, as measured by the grid's own distance function.

The theorem is careful about what it does not show. It does not claim that every local process is minimal-cost, only that minimal-cost processes are local. It also does not define what the spatial identification of the grid is; that is chosen separately by the translated-cell semantics. The module explicitly records countermodels showing that weaker conditions, such as balanced conservation or shift-invariant cost, do not force locality. Those conditions can all hold while an all-pairs dependency, where every cell can influence every other, is also present. Only the minimum-J posting condition rules that out.

In Recognition Science, this result is a step toward showing how spatial locality, the idea that causes have nearby effects, can emerge from the ledger's own cost structure rather than being put in by hand. The theorem is machine-checked, meaning a computer verified the proof, and it uses no unproven assumptions beyond the standard logical axioms. For the general reader, the takeaway is concrete: in this framework, the cheapest possible action is also the most contained one, a single local step that cannot reach across the whole system.

/-- Consumer-changing export: any generator whose nonzero weights are
realizable minimum-J translated-cell dependencies is finite-range at one
D=3 lattice step. -/
theorem tiledJMinimalGenerator_finiteRangeOn
    {L : ℕ} (hL : 2 ≤ L)
    (G : WeightedLedgerGraph (L * L * L))
    (hSupport :
      ∀ i j, G.weight i j ≠ 0 →
        TiledJMinimalDependency3 hL i j) :
    FiniteRangeOn G (encodedDist3 L) 1 :=
  finiteRangeOn_export_v1
    (tiledJMinimalDependency3_operationally_local hL)
    hSupport

/-- **S4 locality theorem.** The operational dependency induced by minimum-J
posting in translated D=3 cells satisfies `LocalOperationalDependency3`
at radius one. The theorem is exact on the account-axis MODEL identification;
production selection of that identification remains the physical hard fork. -/
theorem tiledJMinimalDependency3_operationally_local
    {L : ℕ} (hL : 2 ≤ L) :
    LocalOperationalDependency3 L 1 (TiledJMinimalDependency3 hL) := by
  intro i j hij
  rcases hij with ⟨origin, A, B, hstep, rfl, rfl⟩
  have hdist :
      dist3
        (patternAtCell hL origin (parity 3 A))
        (patternAtCell hL origin (parity 3 B)) = 1 := by
    rw [patternAtCell_dist3]
    exact oneBitDiff_patternDist3
      (jMinimalPostingStep_oneBitDiff hstep)
  simpa only [encodedDist3, Equiv.symm_apply_apply] using hdist.le

/-- Atomicity, balanced conservation, shift-invariant J-cost, period eight,
D=3, and a nontrivial distinction all coexist with an all-pairs dependency.
Thus none of those scalar or temporal declarations chooses spatial locality. -/
theorem committed_candidate_routes_admit_allPairs :
    Nonempty (AtomicTick (tickCarrier 8)) ∧
      Conserves (globalBalancedLedger 8) ∧
      ShiftInvariant (meanFieldLedgerCost 8) ∧
      EightTickFromDimension 3 = eight_tick ∧
      (∃ a b : Fin (2 * 2 * 2), a ≠ b) ∧
      ¬ LocalOperationalDependency3 2 1
        (allPairsDependency :
          Fin (2 * 2 * 2) → Fin (2 * 2 * 2) → Prop) := by
  refine ⟨⟨globalAtomicTick (fun _ => 0)⟩,
    globalBalancedLedger_conserves 8,
    meanFieldLedgerCost_shift_invariant 8,
    rfl, ?_, allPairsDependency_not_local3 2 (by omega)⟩
  exact ⟨0, 1, by decide⟩

What this page does not claim

The theorem does not claim that all local processes are minimal-cost, only that minimal-cost processes are local. The theorem does not specify which spatial identification of the grid is physically correct; that is a separate definitional choice. The theorem does not prove that balanced conservation or shift-invariant cost alone imply locality; in fact it shows they do not.

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