8 Equivalence with the constant and singleton laws

85 laws have been shown to be equivalent to the constant law (Definition 2.20), and 815 laws have been shown to be equivalent to the singleton law (Definition 2.2).

These are the laws up to 4 operations that follow from diagonalization of Definition 2.2 and Definition 2.20.

To formalize these in Lean, a search was run on the list of equations to discover diagonalizations of these two specific laws: equations of the form \(x = R\) where \(R\) doesn’t include \(x\), and equations of the form \(x \circ y = R\) where \(R\) doesn’t include \(x\) or \(y\).

The proofs themselves all look alike, and correspond exactly to the two steps described in the proof of Theorem 4.6. The Lean proofs were generated semi-manually, using search-and-replace starting from the output of grep that found the diagonalized laws.

In the case of the constant law, Definition 2.16 (\(x \circ x = y \circ z\)) wasn’t detected using this method. It was added manually to the file with the existing proof from the sub-graph project.