A classification of solvable spinning-switches puzzles

Spinning-switches puzzles ask for a predetermined sequence of moves that works despite hidden permutations of the switches. Kagey formulated the problem using a finite group of switch states and a permutation group of positions, proved solvability when both groups are $p$-groups for one prime $p$, and classified the case of abelian switch groups. We prove the converse without an abelian hypothesis: for nontrivial finite groups $G$ and $H$, with $H$ acting faithfully on a finite set $\Omega$, a surjective strategy for $G\wr_\Omega H$ exists exactly when $G$ and $H$ are $p$-groups for the same prime. This answers Kagey's Open Question 31. The necessity proof restricts the adversary to a prime-order element and tracks excluded configurations by cosets of prime-power subgroups. We also give a central-series proof of the known sufficient condition. The classification and its consequences for $S_3\wr C_2$ and $A_4\wr C_3$ are formalized in Lean. This work has not yet been reviewed by experts. The proofs, the Lean formalization and the text were produced by AI models (from OpenAI and Anthropic), working under the author's direction.

Computer-assisted; not yet reviewed by experts. Produced by AI models under the author's direction.