I Ching is the unique optimal matching on {0,1}⁶

Stream: general

[Alejandro Radisic]

Hello, weird post here

I formalized a proof that the I Ching's King Wen sequence (the traditional pairing of 64 hexagrams) is the unique K₄-equivariant perfect matching on {0,1}⁶ minimizing total Hamming distance.

Used Mathlib, mostly decide/native_decide for the computational parts. AI-assisted throughout.

Paper + Lean code: https://zenodo.org/records/18210163
GitHub: https://github.com/alerad/iching_

Would appreciate any kind of feedback. Also looking for arXiv endorsement (math.CO) if anyone's able to help.
A member of the community has endorsed me. Thanks a lot to everyone, and thanks for the feedback!

Paper on Arxiv: https://arxiv.org/abs/2601.07175

[Bbbbbbbbba]

Does a matching containing {(001111, 000011), (110000, 111100)} satisfy the K₄-equivariant rule?

[Matt Diamond]

I think you could have saved yourself a little bit of work by using docs#BitVec for the Hexagram type and Bool instead of Fin 2

[Alejandro Radisic]

Yes, it's K₄-equivariant. Applying C, R, or CR to either pair gives the other pair (or itself), so the matching is closed under the group action

That said, you've spotted something, on this orbit the CR-pairing has cost 4 vs 8 for the R-pairing. My writeup only considered C/R matchings, so the global optimality claim needs a scope fix. Thanks for the catch!

[Li, Xinze (Moqian)]

Thanks for sharing your project, Alejandro! Wonderful discussion and amazing how much you've learned to formalize this.

Just explored your code and added some additional content here: https://github.com/Xinze-Li-Bryan/iching_

[Li, Xinze (Moqian)]

also a visualization video: https://youtu.be/4JIzo7qZeaw?si=d0paNz63lTHIh5FB