LockPhasePrediction
plain-language theorem explainer
LockPhasePrediction packages a real-valued structural-change metric on events together with the ordering constraint that LOCK phases must exceed BALANCE phases in any 8-tick trace. Researchers testing the RRF 8-tick discretization hypothesis would cite this structure when formalizing empirical predictions. The declaration is a plain structure definition whose only content is the metric field and the universal inequality.
Claim. A structure on an event type $E$ consisting of a function $f:E→ℝ$ (structural change) and the property that, for every ticked trace $τ$, every index $i$ whose phase is LOCK, and every index $j$ whose phase is BALANCE, $f(τ.events[i])≥f(τ.events[j])$.
background
The module supplies an explicit hypothesis interface for the 8-tick discretization of recognition traces. TickedTrace records a finite sequence of events together with a phase map from Fin(length) into the eight phases. Upstream, phase(k) for k:Fin 8 returns kπ/4, with LOCK phases conventionally the first four and BALANCE the last four; tick is the RS-native time quantum normalized to 1. The module documentation states that observed folding traces are hypothesized to exhibit this 8-phase periodicity, with LOCK intervals corresponding to structure formation and BALANCE to equilibration.
proof idea
This is a structure definition. The body is empty; the declaration simply introduces the two fields (structuralChange and lock_higher) and records their intended interpretation via the attached doc-comments.
why it matters
The structure encodes the central prediction obligation of the 8-tick hypothesis: LOCK phases must display measurably higher structural change. It sits inside the RRF.Hypotheses.EightTick module and directly implements the falsification criteria listed in the module documentation. The declaration therefore supplies the concrete interface needed to confront the eight-tick octave (T7) with data; no downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.