Data for verifying the DMS condition for the hard-core model on the square lattice:

Here is the description of the branching matrix M6 that avoids cycles of length less or equal to six.

Here is the description of the branching matrix M8 that avoids cycles of length less or equal to eight.

Here is the corresponding lambda, S, c, and lower/upper bounds of alpha needed in the DMSc < c condition.

Data for verifying the LP condition for the hard-core model on the square lattice:

Here is the description of the 162-type reduced matrix Mr of M8 that avoids cycles of length less or equal to eight.

Here are the piecewise linear functions found by the LP for each type of the above matrix M_r. This file has huge lines and is supposed to only be read by computers. Here is the format of the file:

There are 153 lines in total. Each of the first 151 lines contains the subintervals for each NON-transient type of the above matrix. The subintevals are given as "[a,b]". The 152nd line is a single line containing the piecewise linear functions corresponding to the subintervals. They appear in the same order as the subintervals, i.e., the first two numbers are for the coefficients of the linear function that is in the first subinterval for type 5 (the first line of the file) and so on. The last line is the objective value of the linear program.

This is the PDF file containing the polynomials from the proof of Lemma 6.