TickedTrace
plain-language theorem explainer
TickedTrace pairs a finite list of events with a phase map from each position into the 8-element cycle. Researchers testing the Recognition Science 8-tick discretization against folding or recognition traces would cite this structure. It is introduced by a direct structure declaration whose fields are the event sequence and the Fin-indexed phase assignment.
Claim. A ticked trace over an event type $E$ consists of a list $e_0, e_1, …, e_{n-1}$ together with a function that assigns to each index $i$ a phase in the 8-cycle (Fin 8), where phases 0–3 label the LOCK segment and 4–7 label the BALANCE segment.
background
The module states the 8-tick hypothesis explicitly: observed traces are discretized into repeating 8-beat cycles with LOCK phases (0–3) for structure formation and BALANCE phases (4–7) for equilibration. Phase is the sibling abbrev Fin 8. Upstream, Constants.tick supplies the fundamental time quantum τ₀ = 1, while Foundation.EightTick.phase defines the concrete angles kπ/4 for k = 0 … 7. The structure therefore supplies the concrete data type on which the hypothesis can be tested.
proof idea
This is a structure definition; no tactics or lemmas are applied. The two fields are declared directly: events : List Event and phase : Fin events.length → Phase.
why it matters
TickedTrace supplies the testing interface for the explicit 8-tick hypothesis in the RRF layer. It is the immediate parent of LockPhasePrediction, which adds the obligation that LOCK phases exhibit higher structural change. The declaration therefore anchors the eight-tick octave (T7) of the forcing chain and the LNAL bytecode cycle length inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.