Phase
plain-language theorem explainer
The phase index in the eight-tick cycle is drawn from the finite set of eight consecutive integers. Modelers of recognition dynamics and eight-beat periodicity cite this abbreviation when labeling lock and balance segments. It is introduced by a direct alias to the standard finite set with eight elements.
Claim. The phase index belongs to the set $0,1,2,3,4,5,6,7$. This set enumerates the successive stages of the eight-beat recognition cycle.
background
The module states the eight-tick hypothesis: recognition traces exhibit periodicity with an eight-beat cycle. The first four phases (0 through 3) constitute the lock interval during which structure forms; the remaining four phases (4 through 7) constitute the balance interval during which equilibration occurs. This is presented as an explicit hypothesis about observed traces rather than a derived axiom.
proof idea
The declaration is a direct abbreviation that identifies the phase index with the finite set Fin 8 supplied by the Mathlib library. No lemmas are invoked and no tactics are applied.
why it matters
This abbreviation anchors the eight-tick octave (T7) within the forcing chain. It is referenced by the elementary bit cost, the conversion from tick counts to octaves, the phase-locked vacuum modes, and the voxel symmetry condition. Downstream applications include the superconducting gap scale and the modified Newtonian dynamics status assessment. It fills the testing interface for the eight-phase periodicity hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.