Dependencies

A sequence \((s_t)_{t\geq 0}\) is a binary step sequence if it meets all of the following conditions:

1. \(s_0 = 0\).

2. 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\).

3. 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:

   1. 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).

   2. 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.

The set of indices where the sequence changes:

Construct a Turing machine that generates a given finite binary step sequence.

Encode a configuration’s tape as a natural number using the tape’s encoding function.

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\).

Extract \(k\) from a difference of the form \(\pm 2^k\). Returns none if the difference is 0 or not a power of 2.

Configuration for leftward-unbounded TM:

• q: Current state of type \(\Lambda \)

• tape: A LeftwardTape instance

A leftward-unbounded TM0 machine is just a standard TM0 machine (type alias).

Step function that enforces leftward constraints. Returns none if the machine halts or if a rightward move from position 0 is attempted.

A tape structure that restricts operations to positions \(\leq 0\):

• tape: The underlying Tape from Mathlib

• head_pos: Current head position as an integer

• head_nonpos: Invariant that head_pos \(\leq 0\)

For a Boolean tape, encode its contents as a natural number:

where true_positions are absolute tape positions \(\leq 0\) containing true.

Generate a sequence by running machine \(M\) from initial configuration and encoding each step:

The difference between consecutive sequence values:

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

See Mathlib documentation.

The difference in encoding when writing at a position is \(0\) or \(\pm 2^k\) where \(k\) is the absolute value of the position.

When the integer encoding difference equals zero, the same value was written.

Writing the same value as currently exists results in zero encoding difference.

If the sequence changes at time \(t\), then the machine hasn’t terminated at step \(t\).

One step of a TM changes the encoding by \(0\) or \(\pm 2^k\).

The \(k\) value in a sequence change equals the absolute position where the write occurred.

Movement constraint between \(k\) values: \(|k_j - k_i| \leq j - i\).

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.

Every TM-generated sequence is a binary step sequence.

If \((s_t)_{t \geq 0}\) is a binary step sequence, then for any \(t \geq 0\), we have \(s_t {\lt} 2^{t+1}\).