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:
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.
Configuration type from Mathlib representing the current state and tape contents of a Turing machine. 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
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.
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\)
A leftward-unbounded TM0 machine is just a standard TM0 machine (type alias).
Configuration for leftward-unbounded TM:
q: Current state of type \(\Lambda \)
tape: A LeftwardTape instance
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.
For a Boolean tape, encode its contents as a natural number:
where true_positions are absolute tape positions \(\leq 0\) containing true.
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.
Generate a sequence by running machine \(M\) from initial configuration and encoding each step:
2.5 Layer 5: Binary Step Sequences
The final layer characterizes the structure of TM-generated sequences.
The difference between consecutive sequence values:
The set of indices where the sequence changes:
Extract \(k\) from a difference of the form \(\pm 2^k\). Returns none if the difference is 0 or not a power of 2.