Optimal Equivariant Matchings on the 6-Cube: With an Application to the King Wen Sequence

TL;DR

This paper characterizes optimal equivariant matchings on the 6-cube, identifies a unique minimal-cost matching with a simple rule, and shows its isomorphism to the King Wen sequence, verified in Lean 4.

Contribution

It provides a complete characterization of equivariant matchings on the 6-cube and links a mathematical optimal matching to the historical King Wen sequence.

Findings

Unique K_4-equivariant matching with minimal cost 120.

Reverse-priority rule determines the optimal matching.

King Wen sequence is isomorphic to the optimal matching.

Abstract

We characterize perfect matchings on the Boolean hypercube {0,1}^n that are equivariant under the Klein four-group K_4 generated by bitwise complement and reversal. For n = 6, we prove there exists a unique K_4-equivariant matching minimizing total Hamming cost among matchings using only comp or rev pairings, achieving cost 120 versus 192 for the complement-only matching. The optimal matching is determined by a simple "reverse-priority rule": pair each element with its reversal unless it is a palindrome, in which case pair with its complement. We verify that the historically significant King Wen sequence of the I Ching is isomorphic to this optimal matching. Notably, allowing comp(rev) pairings yields lower cost (96), but the King Wen sequence follows the structurally simpler rule. All results are formally verified in Lean 4 with the Mathlib library.