I have allowed myself to translate @YCor's proof into the language of group theory. Doing so, I clarified some (probably minor) issues. The result is given in the second half of this arxiv paper: https://arxiv.org/pdf/2405.02992

I have allowed myself to translate @YCor's proof into the language of group theory. Doing so, I clarified some (probably minor) issues. The result is given in the second half of this arxiv paper: https://arxiv.org/abs/2405.02992