Foundation Pair Kernel Tick Locality Max Separated Schedule Val One

A schedule that jumps

In a recognition ledger, a discrete record of events, an atomic tick posts exactly one site at a time. The question is whether that one-post-per-tick rule, by itself, forces nearby sites in the ledger to be the ones that interact. The answer is no. The declaration maxSeparatedSchedule_val_one is a small piece of that negative result: it states that a valid schedule can post site 0 at the first tick and site n - 1 at the second tick, so the two consecutive posts are as far apart as the ledger allows.

The schedule is built for a ledger with n sites, where n is at least 2. At tick 0 it posts site 0, and at every later tick it posts site n - 1. The theorem maxSeparatedSchedule_val_one proves that the site posted at tick 1 has index n - 1. A companion theorem, maxSeparatedSchedule_consecutive_maximally_separated, then shows that the distance between the first two posts, measured by the index metric cellDist, equals n - 1. Two events that happen one after the other in time can be maximally far apart in space.

The point is a separation of concepts. The atomic tick is a temporal schedule: it only says which site posts when. The pair weight graph, which records which sites couple, is a spatial structure. The theorem shows that the temporal rule places no constraint on the spatial one. Even if one tried to read coupling directly from posting adjacency, the induced range would live in tick order, and translating that to the index metric would require a separate commitment that the schedule is index-local. Atomic tick validity alone does not supply that commitment.

This negative result is not a failure of the framework. It is a precise boundary. The locality cutoff for interactions is not carried by the temporal primitive; it must come from the spatial recognition relation itself. The framework's library already contains a positive example: a band coupling graph that is finite-range with radius 1. What remains open is deriving that the recognition relation is finite-neighborhood, a target for future work, not an impossibility.

theorem maxSeparatedSchedule_val_one (n : ℕ) (hn : 2 ≤ n) :
    (maxSeparatedSchedule n hn 1).val = n - 1 := by
  simp [maxSeparatedSchedule]

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

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

This does not claim that finite-range coupling is impossible; a band graph already realizes it. This does not claim that the atomic tick rule is false; it is a valid temporal constraint. This does not claim that the recognition relation is all-to-all; the mean-field graph is one possible choice, not a forced one.

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: