SimpleTicks
plain-language theorem explainer
A predicate on natural numbers and booleans that holds exactly when the boolean matches the odd parity of the number. Researchers constructing minimal examples of atomic tick posting in recognition structures would cite this definition. It is realized by a direct functional equation using modulo arithmetic on the tick index.
Claim. The predicate $postedAt(t, v)$ holds if and only if the Boolean vertex $v$ equals the result of the test $t mod 2 = 1$.
background
The module sets up a minimal two-vertex recognition structure on the Boolean domain with a bidirectional edge. AtomicTick, defined upstream in the Chain module, is the class requiring a function $postedAt : Nat → U → Prop$ together with the axiom that each tick posts to exactly one unique vertex. BoundedStep, defined in Causality, is the class requiring a locally finite step relation whose out-neighbors are bounded in cardinality. This definition supplies the concrete $postedAt$ schedule that alternates vertices by parity.
proof idea
One-line definition via lambda abstraction that directly encodes the parity test. The AtomicTick instance that follows applies the definition inside the unique_post proof by reflexivity on the equality and simplification on the modulo expression.
why it matters
It supplies the minimal concrete witness for the AtomicTick class inside the Recognition framework, allowing verification of the BoundedStep instance on the two-state domain. The example illustrates periodic posting consistent with the eight-tick octave (T7) on a discrete structure. No downstream theorems depend on it, confirming its role as illustrative scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.