31.1. The Mathlib correspondence🔗

HexPermGroupMathlib identifies the checked array representation with Equiv.Perm (Fin n) and transports membership, order, stabilizers, and finite actions to Mathlib. All producers and certificate checkers remain in the Mathlib-free HexPermGroup library.