Encyclopedia Foundation Foundation Pair Kernel Tick Locality Atomic Tick Finite Range Provenance Closed

ARTICLE 3 claims 3 theorems

Foundation Pair Kernel Tick Locality Atomic Tick Finite Range Provenance Closed

A machine-checked theorem proves that the timing of recognition events cannot, by itself, force a limit on how far apart two events can influence each other.

Verify this page

A closed negative result

In the Recognition Science framework, a ledger is a discrete record of events, and a recognition event is a single posting to that record. One primitive idea, called the atomic tick, says that exactly one site posts at each moment in time. A natural question is whether this timing rule forces a spatial consequence: that a recognition event can only affect sites within some fixed distance, a property the framework calls finite range. The declaration atomicTick_finiteRange_provenance_closed_negative settles that question with a theorem: the answer is no.

The theorem, proved in the machine-checked library of formal theorems, shows that the atomic tick imposes no structure on which sites couple. The rule that exactly one site posts per tick is satisfied by every possible posting sequence, so it constrains nothing about the spatial arrangement of couplings. The proof exhibits a concrete counterexample: a carrier with a valid atomic tick whose weight graph connects every site to every other site, and therefore fails the finite-range property at any fixed radius. Even reading coupling directly from posting order fails, because consecutive posts can be maximally far apart in the index metric. Tick-adjacency is not index-adjacency.

The result is a closed negative: the temporal primitive does not force the spatial cutoff. The framework does not conclude that finite range is false; a local coupling graph already satisfies it. The conclusion is that the range cutoff must come from the spatial recognition relation itself, not from the tick schedule. This is a boundary result that tells future work where to look: the locality property must be carried by the geometry of the coupling relation, which remains an open target.

THEOREM atomicTick_finiteRange_provenance_closed_negative · IndisputableMonolith/Foundation/PairKernelTickLocality.lean
atomicTick_finiteRange_provenance_closed_negative · IndisputableMonolith/Foundation/PairKernelTickLocality.lean:171 
/-- **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
THEOREM atomicTick_finiteRange_provenance_closed_negative · IndisputableMonolith/Foundation/PairKernelTickLocality.lean
atomicTick_finiteRange_provenance_closed_negative · IndisputableMonolith/Foundation/PairKernelTickLocality.lean:171 
/-- **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
THEOREM maxSeparatedSchedule_consecutive_maximally_separated · IndisputableMonolith/Foundation/PairKernelTickLocality.lean
maxSeparatedSchedule_consecutive_maximally_separated · IndisputableMonolith/Foundation/PairKernelTickLocality.lean:153 
/-- 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

What this page does not claim

This does not claim that finite range is false or impossible in the framework. This does not claim that the atomic tick is an invalid or useless primitive. This does not claim that the framework cannot derive locality from other principles.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND