module module high

`IndisputableMonolith.Foundation.Atomicity`

The Atomicity module introduces a precedence relation on events to enforce ordering in the Recognition Science foundation. Researchers modeling causal sequences or discrete scheduling in physics would cite it for its minimal-element and topological-sort primitives. The module supplies definitions and basic lemmas that let later results construct sequential schedules while preserving conservation. It consists entirely of definitions and supporting lemmas with no complex proofs.

claimLet $E$ be a set of events. A precedence relation $prec : E → E → Prop$ is defined so that $prec(e_1, e_2)$ asserts $e_1$ must occur before $e_2$. The module also supplies predicates $isMinimalIn$ for events with no predecessors and functions $topoSort$ that produce linear extensions respecting the relation.

background

Recognition Science models physical processes as sequences of atomic events whose order is governed by a precedence relation. The module defines this relation (Precedence) and equips it with standard order-theoretic tools: minimality checks, existence of minimal elements, and topological sorting that respects the given precedence. These constructions sit inside the broader Foundation layer that later builds atomic ticks and sequential schedules. The module imports only Mathlib, relying on its standard library for Prop, lists, and permutation lemmas.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Atomicity supplies the ordering primitives that later modules use to construct sequential schedules and prove conservation preservation. It directly supports the atomic_tick and sequential_preserves_conservation declarations listed among its siblings, which in turn feed the eight-tick octave structure of the unified forcing chain. The module therefore closes the gap between raw event sets and the discrete time steps required by T7.

scope and limits

Does not assume or prove that precedence is a total order.
Does not encode physical distances or metric structure on events.
Does not connect precedence to the phi-ladder or numerical constants.
Does not discharge any hypothesis about global consistency of the order.

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