Lemma. The inverse of a facet move [frap-000M]
✍️source

    Let \(P\) be a finite regular abstract polytope of rank \(n\geq 3\), \(H\) a facet and \(\alpha \in \Gamma ^+(H/F_{-1})\) a facet rotation. The facet move \(\mu _{H,\alpha }\) is a permutation of \(\mathcal R(P)\), with

    \[\mu _{H,\alpha }^{-1}=\mu _{H,\alpha ^{-1}}.\]

    This follows directly from the construction in [marchetti2025rubik, Definitions 5--6].

    Proof. 

      An automorphism preserves proper faces and the order relation, so the moving branch remains in \(\mathcal R(P)\). Since \(\widehat \alpha (H)=H\), the condition \(F\leq H\) holds exactly when \(\widehat \alpha (F)\leq H\). Thus the moving and fixed subsets are preserved separately. On the moving subset the extension of \(\alpha ^{-1}\) is \(\widehat \alpha ^{-1}\) by uniqueness, and cancels the first map. On the fixed subset both maps are the identity.

      The general construction combining permutations of complementary subsets is Equiv.Perm.subtypeCongr; its inverse formula is Equiv.Perm.subtypeCongr.symm. Here the predicate is \(F\leq H\), the moving permutation is the restricted shape automorphism and the other permutation is the identity. These declarations supply that general combination; the polytope-specific preservation argument is the proof above.