module module high

`IndisputableMonolith.Foundation.Atomicity`

The Atomicity module defines a precedence relation on events for the Recognition Science foundation. It supplies minimality checks, topological sorting, sequential schedules, and atomic tick operations. Researchers building event-ordering arguments in the forcing chain cite this module; it is a definition module with no internal proofs.

claimThe module introduces the precedence relation $\prec$ on events with the reading that $e_1 \prec e_2$ means $e_1$ must occur before $e_2$. It further defines the predicate isMinimalIn, the function topoSort, the type Schedule, the operation postAtTick, and the atomic_tick construction.

background

The module resides in the Foundation domain and imports only Mathlib. Its documentation states that prec e1 e2 is read as “e1 must occur before e2”. It introduces supporting notions: isMinimalIn for minimal elements under precedence, topoSort and topoSort_respects for order-preserving permutations, Schedule together with postAtTick and exists_sequential_schedule, and atomic_tick for indivisible processing steps. The local setting is the atomic decomposition of processes that precedes the J-cost function, phi-ladder, and T0-T8 forcing chain.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the event-ordering primitives that atomic_tick and sequential_preserves_conservation rely on inside the same module. It provides the base layer for the UnifiedForcingChain and the T5-T8 steps that later invoke J-uniqueness and the eight-tick octave.

scope and limits

Does not assume the precedence relation is total or transitive.
Does not derive the numerical value of spatial dimensions D = 3.
Does not connect precedence to the Recognition Composition Law.
Does not prove existence of a global time coordinate.

declarations in this module (26)

abbrev Precedence L33
def isMinimalIn L40
lemma exists_minimal_in L50
def topoSort L72
lemma topoSort_perm L91
lemma topoSort_respects L139
structure Schedule L202
def postAtTick L211
theorem exists_sequential_schedule L217
theorem sequential_preserves_conservation L234
theorem atomic_tick L258
def enum L282
lemma enum_surjective L285
def eligible L289
lemma eligible_mono L292
lemma exists_minimal_eligible L299
structure Candidate L315
lemma exists_candidate_index L322
def chooseCandidate L332
lemma chooseCandidate_none_iff L348
lemma chooseCandidate_some_spec L357
def minIndex L369
lemma minIndex_spec L372
lemma minIndex_min L377
def scheduleByMinIndex L385
theorem atomic_tick_countable L429