Foundation Pair Kernel Tick Locality Max Separated Schedule Consecutive Maximall

A schedule that jumps

In the Recognition Science framework, a ledger (a discrete record of events) advances in ticks, and each tick posts an event to exactly one site among a finite set of accounts. A schedule is any rule that chooses which site posts at each tick. The declaration maxSeparatedSchedule_consecutive_maximally_separated proves a fact about one particular schedule: on a carrier with at least two sites, the schedule that posts site 0 at the first tick and site n−1 at every later tick places those two consecutive posts as far apart as the index metric allows, a distance of n−1.

The proof is short and direct. The declaration defines the schedule, shows the first post lands at index 0 and the second at index n−1, and then computes the natural distance between those indices, which is n−1. The theorem is tagged THEOREM because it is proved in the machine-checked library of formal theorems with no unproved assumptions.

The point of this fact is negative. One might hope that consecutive ticks in a ledger would post to nearby sites, so that temporal adjacency would imply spatial adjacency. This schedule shows the opposite: a perfectly valid posting order can jump from one end of the index range to the other in a single tick. The declaration is a witness that the atomic-tick primitive, which only requires exactly one post per tick, places no constraint on which sites couple. Any sequence of sites is a valid schedule, so temporal order alone cannot force a spatial range cutoff.

In Recognition Science, this closes a specific provenance question. The locality property called FiniteRange, meaning a coupling graph has zero weight beyond some distance, was once a candidate for derivation from the atomic-tick schedule. The schedule above, together with an all-to-all coupling graph that also admits a valid atomic tick, shows that derivation is impossible. Locality, if it holds, must come from the spatial recognition relation between sites, not from the temporal posting order.

What the declaration does not claim is broader. It does not say that locality is false in the framework; a band coupling graph already satisfies FiniteRange 1. It does not say that atomic ticks are unconstrained in every sense; the unique-post requirement is real. It only says that one specific hoped-for derivation, from tick adjacency to index adjacency, fails, and that the route to locality must pass through the spatial geometry of the recognition relation.

/-- The first two (tick-adjacent) posts of `maxSeparatedSchedule` are index-maximally separated:
    `cellDist (s 0) (s 1) = n − 1`. Tick-adjacency is not index-adjacency. -/
theorem maxSeparatedSchedule_consecutive_maximally_separated (n : ℕ) (hn : 2 ≤ n) :
    cellDist (maxSeparatedSchedule n hn 0) (maxSeparatedSchedule n hn 1) = n - 1 := by
  have h0 := maxSeparatedSchedule_val_zero n hn
  have h1 := maxSeparatedSchedule_val_one n hn
  unfold cellDist Nat.dist
  rw [h0, h1]
  omega

/-- Any posting sequence `s : ℕ → Fin n` is a valid `AtomicTick` schedule on `tickCarrier n`.
    `unique_post` holds for *every* `s`, so atomic-tick validity carries no adjacency/range content. -/
def scheduleAtomicTick {n : ℕ} (s : ℕ → Fin n) : AtomicTick (tickCarrier n) where
  postedAt := fun t u => u = s t
  unique_post := by
    intro t
    refine ⟨s t, rfl, ?_⟩
    intro u hu
    exact hu

/-- **Null test / decoy.** For every radius `R`, a carrier of size `R + 2` carries a valid
    `AtomicTick` instance while its all-to-all mean-field weight graph fails `FiniteRange R`.
    Atomic-tick validity does not make the weight graph finite-range. -/
theorem atomicTick_does_not_force_finiteRange (R : ℕ) :
    ∃ n : ℕ, Nonempty (AtomicTick (tickCarrier n)) ∧ ¬ FiniteRange (meanFieldWeight n) R := by
  refine ⟨R + 2, ⟨scheduleAtomicTick (fun _ => ⟨0, by omega⟩)⟩, ?_⟩
  exact meanFieldWeight_not_finiteRange R (R + 2) (le_refl _)

What this page does not claim

This does not claim that locality is false in the framework; a band coupling graph already satisfies FiniteRange 1. This does not claim that atomic ticks are unconstrained in every sense; the unique-post requirement is real. This does not claim that the index metric is the only possible measure of distance between sites.

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