Integer Sequences from Turing Machine Tapes

2 Formalization Architecture

Our formalization is structured in layers, each building upon the previous to construct the complete theory of integer sequences from Turing machine tapes. This chapter presents all key definitions and their dependencies.

2.1 Layer 1: Mathlib Foundations

We build upon Lean’s Mathlib library, particularly the theory of Turing machines from Mathlib.Computability.PostTuringMachine:

Definition 1 TM0.Machine (Mathlib)
#

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.

Definition 2 TM0.Cfg (Mathlib)
#

Configuration type from Mathlib representing the current state and tape contents of a Turing machine. See Mathlib documentation.

Definition 3 TM0.Stmt (Mathlib)
#

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.

2.2 Layer 2: Leftward-Unbounded Tape Model

We extend the standard TM0 model with a tape that is unbounded to the left but restricted from moving right past position 0.

Definition 4 LeftwardTape
#

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

Definition 5 LeftTM0.Machine
#

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

Definition 6 LeftTM0.Cfg
#

Configuration for leftward-unbounded TM:

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

  • tape: A LeftwardTape instance

Definition 7 LeftTM0.step
#

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

2.3 Layer 3: Tape Encoding

The core of our construction is the encoding of tape configurations as natural numbers.

Definition 8 LeftwardTape.encode
#

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

\[ \text{encode}(T) = \sum _{i \in \text{true\_ positions}} 2^{|i|} \]

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

Definition 9 LeftTM0.encode_config
#

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

2.4 Layer 4: Sequence Generation

We generate integer sequences by running a Turing machine and encoding the tape at each step.

Definition 10 LeftTM0.sequence

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

\[ \text{sequence}(M, \text{init\_ cfg})(n) = \text{encode\_ config}(\text{steps}(M, n, \text{init\_ cfg})) \]

2.5 Layer 5: Binary Step Sequences

The final layer characterizes the structure of TM-generated sequences.

Definition 11 sequence_difference
#

The difference between consecutive sequence values:

\[ \text{sequence\_ difference}(s, t) = s(t+1) - s(t) \]
Definition 12 change_indices
#

The set of indices where the sequence changes:

\[ \text{change\_ indices}(s) = \{ t \in \mathbb {N} : s(t+1) \neq s(t)\} \]
Definition 13 extract_k_value
#

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