lock_start
plain-language theorem explainer
The declaration assigns the zero element of the eight-element finite set to mark the onset of the LOCK segment within the hypothesized 8-beat cycle. Researchers modeling discrete recognition traces cite this constant when partitioning each cycle into structure-formation and equilibration halves. The definition is a direct constant assignment inside the Fin 8 type.
Claim. The phase marking the beginning of the LOCK interval is defined as $0$ in the finite set of eight phases.
background
The module states the 8-tick hypothesis: observed folding and recognition traces exhibit periodicity over eight phases, with phases 0-3 forming the LOCK interval for structure formation and phases 4-7 forming the BALANCE interval for equilibration. Phase is the abbrev Fin 8, the standard finite type with elements 0 through 7. This supplies the testing interface for the explicit hypothesis about LNAL bytecode cycles rather than a definitional axiom.
proof idea
The definition is a one-line wrapper that directly assigns the zero element of Fin 8.
why it matters
This constant supplies the concrete starting index for the LOCK segment and thereby implements the T7 eight-tick octave (period 2^3) landmark from the forcing chain. It anchors the phase-partitioning interface in the RRF hypothesis module. No downstream results currently depend on it, leaving open its later use in explicit trace-validation lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.