pith. sign in
theorem

atomic_tick

proved
show as:
module
IndisputableMonolith.Foundation.Atomicity
domain
Foundation
line
258 · github
papers citing
67 papers (below)

plain-language theorem explainer

Finite sets of events equipped with a decidable well-founded precedence relation admit a linear extension realized as a one-per-tick schedule. Researchers formalizing causal constraints in recognition histories cite this for constructing atomic serializations. The proof is a term-mode wrapper that invokes the existence lemma for sequential schedules and retains only the covering and ordering fields.

Claim. Let $E$ be a type of events and let $prec$ be a precedence relation on $E$ (i.e., $prec(e_1,e_2)$ asserts $e_1$ must precede $e_2$). Assume $prec$ is decidable and well-founded. For any finite subset $H$ of $E$, there exists a list $sigma$ of distinct events whose underlying set equals $H$ such that $prec(e_1,e_2)$ implies the index of $e_1$ in $sigma$ is strictly smaller than the index of $e_2$.

background

Precedence is the relation $E to E to Prop$ read as “must occur before.” Schedule is the structure consisting of a list of events together with a pairwise distinctness proof; it encodes a one-per-tick posting order. The module works abstractly over any event type equipped with such a relation and assumes only finiteness of the history together with decidability of precedence. It deliberately stays independent of cost functions or convexity. The key upstream result is the existence theorem for sequential schedules, which supplies a list that is pairwise distinct, covers the finite set, and respects precedence.

proof idea

The term proof invokes exists_sequential_schedule on the given precedence, well-foundedness witness and finite set. It obtains a schedule together with its nodup, cover and respect fields, then returns the schedule paired with the cover and respect components, discarding nodup. Classical logic is used only to access the existential.

why it matters

The declaration supplies the constructive atomic-tick serialization that tightens T2 inside the Atomicity module. It guarantees that any finite recognition history can be posted sequentially while respecting ledger precedence, without introducing axioms or cost assumptions. This step supports the forcing chain by ensuring one-event-per-tick evolution remains possible for finite histories, thereby grounding later conservation and emergence arguments.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 30 of 67)

The full set is indexed internally; the public theorem page shows a capped sample so high-use declarations do not become many-thousand-row pages.