AtomicTick
plain-language theorem explainer
AtomicTick is a typeclass on RecognitionStructure that requires a unique state in U to be posted at each natural-number tick. Ledger and chain developments cite it to enforce collision-free atomicity. The declaration consists of the postedAt predicate together with its uniqueness axiom.
Claim. A RecognitionStructure $M$ satisfies AtomicTick when there is a predicate postedAt : $ℕ → M.U →$ Prop such that $∀ t : ℕ, ∃! u : M.U$, postedAt $t$ $u$.
background
RecognitionStructure is the minimal carrier consisting of a type U together with a binary relation R : U → U → Prop, supplied as a stub to allow standalone compilation of chain axioms. AtomicTick augments this carrier with the postedAt map and the requirement that each tick selects exactly one element of U. Upstream Recognition and RecognitionForcing modules define analogous structures that add self-recognition and symmetry, while RSNativeUnits supplies the concrete gauge U with tick and voxel units.
proof idea
Direct class declaration. The two fields postedAt and unique_post are introduced without further proof obligations or reductions.
why it matters
AtomicTick supplies the atomicity axiom consumed by T2_atomicity, which concludes that any two postings at the same tick must coincide. It is instantiated for finite AccountRS carriers in LedgerPostingAdjacency to define accountAt and to relate legal atomic ticks to one-bit differences. Within the Recognition framework the class realizes the discrete tick structure that underlies the eight-tick octave and the phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.