Optimal Equivariant Matchings on the 6-Cube with an Application to the King Wen Sequence
Alejandro Radisic
math.GM
Jan 12, 2026 · v1
TL;DR
Checks finite orbit counts and case distinctions for equivariant matchings on the 6-cube in Lean 4.
Abstract
We study equivariant perfect matchings on the Boolean hypercube $\B^6$ under the Klein four-group $K_4 = \langle \comp, \rev \rangle$ generated by bitwise complement and reversal. Among matchings using only $\comp$ or $\rev$ pairings, there is a unique Hamming-cost minimizer, given by a simple ``reverse-priority rule'': pair each element with its reversal unless it is a palindrome, in which case pair it with its complement. This matching has total Hamming cost 120, compared to 192 for the complement-only matching. The historically significant King Wen sequence of the I Ching realizes precisely this matching. Pure Hamming minimization over the full $K_4$ action is different: allowing $\comp \circ \rev$ lowers the cost to 96. The King Wen rule is recovered, however, as the unique Hamming-weight-preserving optimum: it minimizes failures of Hamming-weight preservation before Hamming distance, and it is stable for the weighted energy $α|Δw|+βd_H$ throughout the open region $α>β$. The finite orbit counts and case distinctions are checked in Lean~4.
Problem
What is the minimum-cost equivariant perfect matching on the 6-dimensional Boolean hypercube under the Klein four-group generated by bitwise complement and reversal, and does the ancient King Wen sequence of the I Ching realize such a matching?
Approach
The paper studies equivariant perfect matchings on B^6 under K_4 = <comp, rev>. Among matchings using only complement or reversal pairings, it identifies a unique Hamming-cost minimizer via a reverse-priority rule: pair each element with its reversal unless it is a palindrome, in which case pair it with its complement. The optimality proof and the connection to the King Wen sequence are verified in Lean.
Results
The unique minimum-cost K_4-equivariant matching has total Hamming cost 120, compared to 192 for complement-only. The King Wen sequence of the I Ching realizes precisely this optimal matching. The Lean formalization verifies both the optimality and the King Wen correspondence.