Reasoning about planar diagrams is error-prone for both humans and computers, and has led to incorrect statements in publications. In particular, an orientation-preserving mapping is not always determined by how it acts on triples of elements.

The authors formalize orientation-preserving mappings in the Lean proof assistant. They encode cyclic order preservation on finite sets and verify properties that have previously led to errors in published work, using Lean to ensure correctness of claims about when mappings on planar diagrams are or are not determined by their action on triples.

The formalization confirms that orientation-preserving mappings are not in general determined by their action on triples, providing a machine-checked counterexample to an assumption that has caused errors in prior publications.