EightTickHypothesis
plain-language theorem explainer
The EightTickHypothesis class encodes the claim that any trace decomposes into a sequence of phases from Fin 8 such that consecutive phases are either identical or successive under the cycle successor. Researchers modeling RRF discretization of folding or recognition processes would cite it when testing observed 8-beat periodicity. The declaration is a direct class with fields for the extraction map and the cyclic adjacency condition.
Claim. Let Trace be a type of experimental traces. The eight-tick hypothesis on Trace consists of a map ticks : Trace → List(ℤ/8ℤ) such that for every trace t, every index i < L = |ticks(t)|, and j = (i + 1) mod L, the phases p_i = ticks(t)[i] and p_j = ticks(t)[j] satisfy p_i = p_j or p_j = p_i + 1 (mod 8).
background
Module RRF.Hypotheses.EightTick presents the 8-tick hypothesis as an explicit claim about observed traces, not a definitional axiom. Phase is the abbrev Fin 8, with phases 0-3 labeled LOCK (structure formation) and 4-7 labeled BALANCE (equilibration). The fundamental time quantum is the tick, defined as the RS-native unit τ₀ = 1.
proof idea
The declaration is the class definition itself. It introduces the two fields ticks and cyclic directly; the cyclic field states the adjacency condition as part of the class type. No lemmas or tactics are applied beyond the field declarations.
why it matters
This declaration supplies the explicit interface for the eight-tick octave (T7) in the forcing chain, providing the testing structure for LNAL bytecode 8-phase cycles. It lists concrete falsification criteria in the module documentation and anchors the discretization hypothesis for Recognition Science traces. No downstream theorems are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.