AtomicTick
plain-language theorem explainer
The AtomicTick re-export supplies the discrete time structure for recognition processes under the RRF namespace. Ledger and chain formalizations cite it to enforce unique account posting at each tick via the postedAt predicate. The declaration is a direct abbreviation aliasing the class definition from the Recognition module.
Claim. Let $M$ be a recognition structure. An atomic tick on $M$ consists of a predicate $postedAt : Nat → M.U → Prop$ such that for every $t ∈ Nat$ there exists a unique $u ∈ M.U$ satisfying $postedAt(t, u)$.
background
This module re-exports core recognition concepts to bridge the Recognition and RRF frameworks, making the discrete time model available under the RRF namespace. The AtomicTick class equips any RecognitionStructure with a postedAt predicate on natural-number ticks together with a uniqueness axiom. Upstream results supply the identical class: class AtomicTick (M : RecognitionStructure) where postedAt : Nat → M.U → Prop and unique_post : ∀ t : Nat, ∃! u : M.U, postedAt t u.
proof idea
The declaration is a one-line abbreviation that directly aliases Recognition.AtomicTick, inheriting the class fields and uniqueness axiom without further reduction.
why it matters
This re-export supports the T2 atomicity theorem deriving uniqueness of postings and enables concrete ledger constructions such as AccountRS with its atomic tick instance. It supplies the discrete time slot required by the recognition chain and ledger posting adjacency results. The placement aligns with the atomicity step that precedes the eight-tick octave structure in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.