octavePhase
plain-language theorem explainer
octavePhase maps any natural number t to its position in the 8-tick cycle by taking t modulo 8. Physicists modeling periodic phenomena in the Recognition Science framework, including phase synchronization with the gap-45 rung, cite this definition to index the fundamental octave period. The implementation is a direct modular arithmetic reduction that automatically satisfies the Fin 8 bound via Nat.mod_lt.
Claim. The phase within an octave for a tick count $t$ is the integer $t mod 8$ in the finite set $0,1,…,7$.
background
RS-Native units treat the tick as the atomic time quantum and organize measures on the φ-ladder. The octave is defined as 8 ticks, the fundamental evolution period. Upstream, EightTick.phase supplies the corresponding real-valued phases $kπ/4$ for $k$ in Fin 8, while MusicalScale.octave sets the ratio to 2 and Constants.octave anchors the period.
proof idea
The definition computes the remainder of t divided by 8 and packages it with the proof that the remainder is strictly less than 8, supplied by Nat.mod_lt. It is a direct one-line definition relying on built-in natural number modulo.
why it matters
This definition supplies the discrete phase index for the eight-tick octave, which is central to T7 in the forcing chain and enables synchronization via lcm(8,45)=360 that forces D=3. It is used directly by octaveTrajectory and octaveTrajectory_periodic in Cost.Ndim.Octave to construct phase-shifted cosine trajectories for n=8 visualizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.