There is ongoing AI assisted work on this, and precisely the problematic gap in the theory (around Corollary 3.12).

As of now, a required step appears to definitely be missing, but it's not clear if this is a genuine / unrepairable defect.

https://zen.ac.jp/news/zmcpostevent0331e

https://github.com/lana-agents/iut

https://github.com/LANA-Project/genl