From a repeated state to a prediction
Find the whole
pattern.
A controller takes one step at each tick. Once a state repeats, what can we know about every later tick?
Give each state one fixed successor. The construction below finds where the repetition begins and how long one cycle lasts. It can then predict a distant state without running every intervening step.
← Begin with the arithmetic lessonFind the startup.
Find the cycle.
Our first example starts at state 0 and follows 0 → 1 → 2 → 3 → 4 → 2. States 0 and 1 occur once. States 2, 3 and 4 repeat.
Describe your own controller
Number the states from 0. Enter the next state for each one, separated by commas. For example, 1,2,3,4,2 says that state 0 goes to 1, state 1 goes to 2, and state 4 returns to 2. Use at most 32 states.
The outlined state is the prediction below.
The cycle starts at tick 2 and lasts 3 ticks.
Counts 2 and 5 reach the same state. Six comparison calls recover the pattern.
Show each comparison
First, keep the earlier count fixed and try gaps of 1, 2, and so on until the states match. Then try starting positions from 0 until moving forward by that gap reaches the same state.
- Period: compare ticks 2 and 3: different.
- Period: compare ticks 2 and 4: different.
- Period: compare ticks 2 and 5: same.
- Start: compare ticks 0 and 3: different.
- Start: compare ticks 1 and 4: different.
- Start: compare ticks 2 and 5: same.
Use the recovered pattern
At tick 1,000,000,000: state 4.
Remove the two startup ticks. The remaining count leaves a remainder of two when divided by three, so this tick has the state recorded at tick 4.
Why the prediction holds
Equal states must have
equal futures.
If the complete current state determines the next state, two matching states stay matched after one tick, two ticks, or any equal number of ticks. The Lean proof derives this from iteration. It supplies the condition needed by the classification theorem.
With that condition and exact state comparisons, a repeated pair at counts a < b determines one initial length and one positive period. The search uses at most b + 1 comparison calls, and never asks about a count greater than b. Finding the repeated pair and producing the states being compared are separate work.
Why does the first matching gap reveal the whole cycle?
Once a complete state repeats, the fixed update rule carries the controller around the same loop forever. The states within one shortest loop are all different: an earlier repeat would close a shorter loop. So the first gap that brings a repeated state back to itself is exactly one cycle. Testing starting positions then finds the first tick on that cycle.
This is why a later repeated pair still works. Its two counts can be many turns apart; the smaller comparisons find the shortest turn and the earliest start.
A matching display can mislead
Imagine four internal states, A → B → C → D → D, whose displayed labels are 0, 1, 0, 2. The display is 0 at ticks 0 and 2. One tick later those displays are 1 and 2. The repeated label did not mean the same complete state.
Applying the search to those labels would suggest a two-tick cycle and make a wrong prediction at tick 3. The full transition table in the tool avoids this ambiguity: its state number specifies the entire state of the model.
How this relates to existing methods
Initial sequences followed by cycles are familiar in finite-state mathematics. Floyd’s and Brent’s cycle-finding methods recover this structure from repeated application of a function. Brent’s original paper gives the classical setting and algorithms.
This example starts with a witnessed repeated pair and exposes the bounded comparisons that recover the pattern. The δ framework connects those comparisons to generated event records and states exactly which information the proof needs. No speed advantage over established methods is claimed. The implementation is checked against Floyd’s method under the same finite-state models.
What this lets you do
For a finite controller with a fixed update rule, you can retain the startup sequence and one complete cycle instead of an indefinitely growing state log. You can predict future states or compare different recorded counts. The event count itself still grows: compressing the state history does not erase how many events occurred.
Inspect the construction
The Lean source returns the recovered pattern together with proofs of its correctness, search bounds and predictions. It uses the existing δ classification. The proof also connects the result to the native records used in the arithmetic lesson. Read the verification report or download the complete Lean source package.