1
Introduction
2
Formalization Architecture
▶
2.1
Layer 1: Mathlib Foundations
2.2
Layer 2: Leftward-Unbounded Tape Model
2.3
Layer 3: Tape Encoding
2.4
Layer 4: Sequence Generation
2.5
Layer 5: Binary Step Sequences
3
The Basic Construction
4
Structural Properties
5
Supporting Lemmas
6
Universality Results
7
Implementation Notes
8
Connections and Open Questions
▶
Alternative Encodings.
Complexity of Generation.
9
Implementation Status
▶
Current Status
Completed Components
What’s Complete
Remaining Work
10
Conclusion
Dependency graph
Integer Sequences from Turing Machine Tapes
Eric Vergo
1
Introduction
2
Formalization Architecture
2.1
Layer 1: Mathlib Foundations
2.2
Layer 2: Leftward-Unbounded Tape Model
2.3
Layer 3: Tape Encoding
2.4
Layer 4: Sequence Generation
2.5
Layer 5: Binary Step Sequences
3
The Basic Construction
4
Structural Properties
5
Supporting Lemmas
6
Universality Results
7
Implementation Notes
8
Connections and Open Questions
Alternative Encodings.
Complexity of Generation.
9
Implementation Status
Current Status
Completed Components
What’s Complete
Remaining Work
10
Conclusion