This repository contains the code accompanying the paper "The Four-Color Ramsey Multiplicity of Triangles" by Aldo Kiem, Sebastian Pokutta, and Christoph Spiegel (available at arXiv:2312.08049).
The certificates certificate_23.yaml and certificate_24.yaml in the folder certificate contains the rational entries of the solution matrices. They are stored in the format {t: [[F1, F2, q], ... ], ...} where t is a type and F1 and F2 are two flags over t and q is the rational entry. The types and flags are encoded with a string representation. As an example, consider c.2.4.5.4.9k5e. The prefix c indicates that the object is a coloring of a complete graph. In succession, 2 denotes the uniformity, 4 the number of colors, 5 the number of vertices and 4 that the first four vertices of the coloring form a type. The suffix 9k5e is a base 36 string representation, using all digits and letters, of the list of edge colors. The folder certificate also contains the files known_zevs_23.yaml and known_zevs_24.yaml which contain a basis of the zero eigenvector space of the solutions.
A script to verify the certificates is provided in verify.py. It requires Python version 3.7 or higher as well as an installation of sage, the python libraries tqdm and numpy, and a yaml parser. To run the verification, type python verify.py in the terminal. An optional flag is -dm that disables multiprocessing. The script will ask whether you want to verify Theorem 2.3 or 2.4. You can also specify goodman or cummingsetal to test the script by verifying two computationally simpler statements.
The script first generates the relevant data for each coloring G on the correct number of vertices needed to verify the certificate, giving us the constraint matrices D for the SDP corresponding to G. It then takes the Frobenius product X.D of our solution X with D to verify the respective lower bounds. In the case of Theorem 2.3 (and for cummingsetal), it also verifies that the conditions for our stability result are met.
The matrices of the certificate are stored directly and not as an LDL-decomposition, which would make verification of positive semidefiniteness easier. This is simply to space constraints: stored as described above, the certificate for Theorem 2.3 takes up only 25M, while the LDL decomposition requires 3.7GB. In order to verify the positive semidefiniteness of the matrices we therefore included two checks. The first is a fast numerical check that verifies that the provided zero eigenvectors are in fact zero eigenvectors as well as linearly independent and then verifies that up to a tolerance of 1e-6 no additional eigenvectors can be found numerically. The second is a full algebraic check that relies on the block diagonalization described in the paper and takes around one hour for Theorem 2.4 and around one day for Theorem 2.3.