# One-tape time simulation in two-fifths-power space

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Simulating One-Tape Time in Two-Fifths-Power Space](../../preprints/Simulating-One-Tape-Time-in-Two-Fifths-Power-Space-September-25-2026/article.pdf)

## Scope

The formalization gives two-fifths-power space simulation of a fixed deterministic machine with one writable tape and finitely many read-only input heads. Heads move at most one cell per step, initial contents are independent of the time bound, and contents and input symbols must be accessible in polylogarithmic space. Given a binary time cap $T\ge2$, the simulator returns the source's finite-control outcome and halting flag using $O(T^{2/5}(\log(T+2))^C)$ space.

A second simulator needs no time cap: on an input that halts at time $t$, it returns the halted outcome using $O((t+2)^{2/5}(\log(t+2))^C)$ space. Simulation time is unrestricted. General multitape simulation, hierarchy consequences, and bounded-space-halting results are outside these selected statements.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Time-capped and unknown-time one-tape simulation in two-fifths-power space | [OneTapeSpace.lean](../ComparatorChallenges/OneTapeSpace.lean) |