AtomicTick
plain-language theorem explainer
The AtomicTick class equips any RecognitionStructure M with a map from natural-number ticks to elements of M.U such that each tick posts to exactly one u. Ledger and chain constructions cite this interface to enforce discrete atomicity. The declaration is a direct class definition that re-exports the upstream Chain version inside the Recognition module.
Claim. Let $M$ be a recognition structure with universe $U$. $M$ admits atomic ticks when there is a predicate postedAt $: Nat → U → Prop$ such that for every $t ∈ Nat$ there exists a unique $u ∈ U$ with postedAt $t$ $u$.
background
A RecognitionStructure is a pair consisting of a type $U$ and a binary relation $R$ on $U$. The local module defines a concrete $M$ by taking $U$ from the RS-native units (where $τ_0 = 1$ tick) and letting $R$ be structural equality. AtomicTick augments this carrier with a discrete time axis whose postings are unique. The upstream Chain module supplies the identical class as a minimal stub; RecognitionForcing supplies an alternative RecognitionStructure carrying self-recognition and symmetry axioms.
proof idea
This is a class definition, not a theorem. It introduces the two fields postedAt and unique_post directly as the interface contract.
why it matters
AtomicTick supplies the atomicity interface consumed by T2_atomicity (which derives posting uniqueness) and by the ledger constructions accountAt, AccountRS, and legalAtomicTick_oneBitDiff. It therefore anchors the T1–T2 segment of the forcing chain inside RS-native units. The declaration leaves open how the recognition relation $R$ interacts with the posting map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.