octavePhase
plain-language theorem explainer
The octavePhase definition maps each index i in Fin 8 to the real phase angle 2πi/8. Researchers constructing n=8 cosine trajectories or eight-tick periodic models in Recognition Science cite it to generate uniform shifts for coefficient visualizations. The implementation is a direct arithmetic expression with no lemmas or tactics applied.
Claim. For each index $i$ in the finite set $0,1,2,3,4,5,6,7$, the phase angle equals $2π i / 8$.
background
The module defines coefficient trajectories for the n=8 octave case. Upstream results supply the Phase abbreviation as Fin 8, the 8-tick phase space appearing in both ChurchTuringPhysicsStructure and the EightTick hypotheses. The sibling octavePhase in RSNativeUnits computes the phase index via t mod 8 and notes that lcm(8,45)=360 synchronizes octave and gap-45 cycles.
proof idea
Direct definition that casts the Fin 8 index to ℝ and scales by 2π/8. No lemmas are invoked; the expression serves as a primitive for the downstream octaveTrajectory and octaveTrajectory_periodic declarations.
why it matters
It supplies the phase argument to octaveTrajectory, which builds the Vec 8 cosine vector, and to the periodicity theorem octaveTrajectory_periodic. The definition realizes the eight-tick octave landmark (T7) and supports gap-45 synchronization noted in RSNativeUnits. It closes the scaffolding for n=8 cost visualizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.