This page contains supplementary materials for the paper "A Gramian description of the degree 4 generalized elliptope."
We claim in the paper that certain linear inequalities holding over the cut polytope admit degree 4 sum-of-squares proofs. The coefficients in these inequalities correspond to the sign pattern of a maximal equiangular tight frame (ETF). Verifying this claim amounts to producing a large matrix satisfying certain linear constraints, and showing that it is positive semidefinite. The following script produces this matrix and validates that it satisfies the necessary linear and positive semidefiniteness constraints symbolically using SageMath.
(Conveniently, the ETF may be constructed indirectly using the correspondence between ETFs and strongly regular graphs (SRGs) and the SRG library built into SageMath.)