isOddTick
plain-language theorem explainer
The definition marks phases 1, 3, 5 and 7 inside the Fin 8 cycle as odd. Workers on discrete-time spin-statistics models cite it to separate fermion from boson sectors. It is a direct parity check on the integer representative of the phase index.
Claim. For each phase index $k$ in the set of eight discrete phases, the predicate holds precisely when the representative integer of $k$ satisfies $k mod 2 = 1$.
background
The module establishes the fundamental discrete clock of Recognition Science as an 8-tick cycle whose phases are labeled 0 through 7. These phases are realized as the type Fin 8, imported from ChurchTuringPhysicsStructure, and each tick is the RS-native time quantum of unit length. The module doc states that the structure underlies spin-statistics via the rule that odd phases correspond to fermions and even phases to bosons, together with CPT symmetry and gauge-group structure.
proof idea
One-line definition that extracts the integer value of the Fin 8 element and tests its remainder modulo 2.
why it matters
It supplies the concrete predicate needed for the fermion-boson distinction inside the eight-tick octave (T7). The predicate sits next to sibling definitions for phase periodicity and the generation of Z8, completing the discrete-clock layer that feeds CPT and gauge constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.