Have you considered looking at this in ram model rather than multi tape? it makes things a lot simpler

For one thing, the RAM model isn't fine-grained equivalent to MTTM (an example is https://en.wikipedia.org/wiki/Counting_sort which is linear-time on RAM but not MTTM). So, the result might not be the same. But also, Mathlib lacks a RAM machine implementation. So any proof would rest on a custom definition stack which would make it difficult to audit.

	▲	adgjlsfhk1 2 hours ago \| parent [-]
		yeah in ram models, this turn into O(n^1-kappa) , but otherwise the result is pretty similar (but you can drop the bit network part since matrix transposition is easy in RAM)