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.

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)