Amazing work to both of you! I’m so excited to see that my “proof sketches” panned out! I’ve updated https://www.sligocki.com/2023/02/05/shift-overflow.html to link here.
Great work, but I think this needs a bit of a caveat. We don’t have a formal proof for most TMs IIUC. Most notably we don’t have a formal proof for the FAR decider, right? IIUC, the true statement is something like: among the “holdout” machines in The 30 to 34 CTL holdouts from BB(5) unproven by general deciders, only Skelet #17 is missing a formal proof.