Foundation Pair Kernel Tick Locality Max Separated Schedule

A schedule that jumps

In the Recognition Science framework, a ledger is a discrete record of events, and a tick is a single posting moment in that record. One primitive rule, the atomic tick, says that exactly one site posts at each tick. A natural guess follows: if events only couple when they post in neighboring ticks, then the ledger's interactions should be local, meaning a site only affects sites within some fixed distance. The declaration maxSeparatedSchedule exists to test that guess, and it breaks it.

The schedule is simple. Number the sites from 0 to n−1. At tick 0, post site 0. At every later tick, post site n−1. This is a perfectly valid atomic tick, since each tick has exactly one post. Yet the first two posts, which are adjacent in time, land on sites that are as far apart as the carrier allows: their index distance is n−1. Tick-adjacency is not index-adjacency. Reading coupling strength directly off posting order would therefore force a range cutoff in tick-order, not in the spatial metric that actually matters.

The framework proves this cleanly. The theorem maxSeparatedSchedule_consecutive_maximally_separated shows the consecutive posts are index-maximally separated, and maxSeparatedSchedule_isValidAtomicTick confirms the schedule is a genuine atomic tick. The bundled theorem atomicTick_finiteRange_provenance_closed_negative assembles the full verdict: a valid atomic tick can coexist with an all-to-all coupling graph, and with a schedule whose consecutive posts are maximally far apart. The temporal primitive constrains nothing about which sites couple.

In Recognition Science, the consequence is precise. The atomic tick does not force a finite interaction range. Locality, if it exists, must come from the spatial recognition relation, the structure that says which sites are neighbors, not from the order of postings. The framework's own bandWeight graph already realizes a finite range of 1, but nothing in the tick schedule forces that choice over the all-to-all mean-field graph.

What the declaration does not claim is just as important. It does not show that locality is false: a local coupling graph remains a valid, proved option. It does not show that the framework admits arbitrary screening, since the finite-range condition still excludes the all-to-all route. And it does not touch any specific interaction law, such as an inverse-square or Yukawa form. The schedule is a counterexample, not a physical theory.

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

/-- The scrambling schedule is itself a valid `AtomicTick`, so the maximal separation above is
    realized by a genuine atomic-tick posting order — no schedule regularity is entailed. -/
theorem maxSeparatedSchedule_isValidAtomicTick (n : ℕ) (hn : 2 ≤ n) :
    Nonempty (AtomicTick (tickCarrier n)) :=
  ⟨scheduleAtomicTick (maxSeparatedSchedule n hn)⟩

/-- **L0 provenance verdict (bundle).** At carrier size `n = R + 2` all three facts hold at once:
    (1) a valid `AtomicTick` instance exists, (2) the all-to-all mean-field weight graph fails
    `FiniteRange R` (the null test), and (3) a valid `AtomicTick` schedule posts index-maximally
    separated sites at consecutive ticks (`cellDist (s 0) (s 1) = n − 1 = R + 1`). Together:
    atomic-tick posting adjacency does not force `FiniteRange`; the route to a THEOREM-grade `L0`
    via the tick schedule is CLOSED NEGATIVE. `L0` stays HYPOTHESIS, its provenance the spatial
    coupling geometry (`M.R` / lattice adjacency), not the temporal tick primitive. -/
theorem atomicTick_finiteRange_provenance_closed_negative (R : ℕ) :
    Nonempty (AtomicTick (tickCarrier (R + 2))) ∧
      ¬ FiniteRange (meanFieldWeight (R + 2)) R ∧
      cellDist (maxSeparatedSchedule (R + 2) (by omega) 0)
          (maxSeparatedSchedule (R + 2) (by omega) 1) = R + 1 := by
  refine ⟨⟨scheduleAtomicTick (maxSeparatedSchedule (R + 2) (by omega))⟩,
    meanFieldWeight_not_finiteRange R (R + 2) (le_refl _), ?_⟩
  have h := maxSeparatedSchedule_consecutive_maximally_separated (R + 2) (by omega)
  simpa using h

What this page does not claim

Locality is false; a finite-range coupling graph remains a valid option. The framework admits arbitrary screening; the finite-range condition still excludes the all-to-all route. Any specific interaction law, such as inverse-square or Yukawa, is derived from the tick schedule.

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: