- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
A sequence \((s_t)_{t\geq 0}\) is a binary step sequence if it meets all of the following conditions:
\(s_0 = 0\).
For each step \(t \geq 0\), the difference \(\delta _t = s_{t+1} - s_t\) is either \(0\) or has the form \(\pm 2^k\) for some non-negative integer \(k\).
Let \(I = \{ t \geq 0 \mid \delta _t \neq 0\} \) be the set of indices where the sequence changes. For each \(t \in I\), define \(k_t = \log _2 |\delta _t|\). The following must hold:
For every \(t \in I\), we must have \(k_t \leq t\). This reflects that the head, starting at position 0, can reach at most position \(-t\) after \(t\) steps (moving leftward).
For any two indices \(i, j \in I\) with \(i {\lt} j\), we must have \(|k_j - k_i| \leq j - i\). This constrains the head’s movement between any two write operations.
Consider a Turing machine \(M\) with:
A tape unbounded to the left, with cells indexed by non-positive integers \(0, -1, -2, \ldots \)
A binary tape alphabet \(\{ \text{false}, \text{true}\} \)
An initial tape configuration where all cells contain \(\text{false}\)
A read/write head starting at position \(0\)
Let \(T_t(i)\) be the content of tape cell \(i\) at time step \(t \geq 0\). The integer sequence \((s_t)_{t \geq 0}\) generated by \(M\) is defined by:
We denote the head’s position at the beginning of step \(t\) (i.e., before the transition from \(t\) to \(t+1\)) as \(p_t\).
Configuration type from Mathlib representing the current state and tape contents of a Turing machine. See Mathlib documentation.
The basic Turing machine model from Mathlib with states of type \(\Lambda \) and tape symbols of type \(\Gamma \). A machine is a function from state and symbol to an optional statement. See Mathlib documentation.
Statement type for machine operations:
move d: Move the head in direction \(d\)
write a: Write symbol \(a\) at the current position
Every finite binary step sequence is TM-generable.
Formalization Note: The theorem statement is complete and type-checks in Lean. The proof constructs an explicit Turing machine using states indexed by sequence position. The construction is complete except for the helper lemma construction_generates_sequence, which requires additional lemmas about machine state tracking through the computation. Specifically, we need to prove that after \(j\) steps, the machine is in state \(j\) with the head at the position specified by the constructed head path.