postedAt
plain-language theorem explainer
postedAt supplies the concrete map sending each natural-number tick t to the unique state v = t mod 3 inside the three-element universe of the cyclic recognition structure M. Modelers of discrete atomic processes and ledger constructions cite it when they need an explicit AtomicTick instance for a finite cycle. The definition is a direct equality together with a one-line Nat.mod_lt verification that the representative lies in Fin 3.
Claim. For the recognition structure $M$ whose state space is $U = Fin 3$ with successor relation $R(i,j) := j = (i+1) mod 3$, the posting predicate is defined by $postedAt(t,v) := v = t mod 3$, where the modulus representative is witnessed by the proof that $t mod 3 < 3$.
background
In Recognition.Cycle3 the structure $M$ is the three-state cycle whose universe is $Fin 3$ and whose recognition relation advances the index by one step modulo 3. The AtomicTick class (appearing in both IndisputableMonolith.Recognition and IndisputableMonolith.Chain) packages a postedAt predicate together with the uniqueness axiom that exactly one state is posted at each tick. The present definition supplies the concrete postedAt map required to instantiate that class for the cyclic carrier, consistent with the RS-native gauge in which each tick is a single discrete advance.
proof idea
The definition is written directly as the equality $v = ⟨t % 3, p⟩$ where $p$ is the short proof $Nat.mod_lt _ (by decide : 0 < 3)$. The AtomicTick instance that follows simply re-uses this postedAt, exhibits the same modular representative, and discharges uniqueness by reflexivity and simplification on the postedAt equation.
why it matters
The definition furnishes the AtomicTick instance for $M$ that is consumed by T2_atomicity (in both Chain and Recognition) to prove that distinct states cannot be posted at the same tick. It is also used by LedgerPostingAdjacency constructions and by modeling examples. Within the Recognition Science framework it realizes the atomic posting step that precedes the forcing-chain arguments leading to the eight-tick octave and the emergence of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.