isOddTick
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove any physical mapping of odd ticks to fermions.
- Does not encode the explicit radian values of the phases.
- Does not constrain the numerical duration of the fundamental tick.
formal statement (Lean)
40def isOddTick (k : Fin 8) : Bool := k.val % 2 = 1
proof body
Definition body.
41
42/-- Phase advance by one tick. -/