isEvenTick
plain-language theorem explainer
Even ticks in the 8-tick cycle are those with even indices and correspond to bosons. Researchers deriving spin-statistics or CPT symmetry from the discrete clock in Recognition Science cite this predicate. The definition reduces to a direct modulo-2 test on the index in the finite set of eight ticks.
Claim. Define the predicate even-tick$(k)$ to hold for $k$ in the set of eight ticks precisely when $k$ is even, i.e., $k$ mod $2 = 0$.
background
The module introduces the 8-tick structure as the fundamental discrete clock of Recognition Science. Phases run through multiples of π/4 and supply the discrete time underlying spin-statistics, CPT symmetry, gauge groups, and phase accumulation. The supplied doc-comment states that even ticks (0, 2, 4, 6) correspond to bosons while the sibling odd-tick definition assigns fermions to the complementary indices.
proof idea
The definition is a direct equality: the integer value of the index modulo 2 equals zero.
why it matters
The predicate supplies the even/odd split required by the eight-tick octave (T7) in the forcing chain. It thereby enables the boson-fermion distinction that feeds into CPT and gauge-structure derivations within the discrete-time model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.