OAI.PerfectMatchingPSD.main

The theorem states that the defined proposition MainClaim holds. Edges on vertex set {0,…,n−1} are pairs (a,b) with a<b, and a perfect matching is a set of edges such that every vertex lies in exactly one chosen edge. The rows are indexed by all edges together with all odd-cardinality vertex subsets U. For a perfect matching M, the slack of an edge row e is 1 if e∈M and 0 otherwise, while the slack of an odd-set row U is the number of edges of M crossing U (exactly one endpoint in U) minus 1. HasFactorization(n,r) says there exist real symmetric positive semidefinite r×r matrices A_i for every row i and B_M for every perfect matching M, with no equivariance or rank-one restriction, such that slack(i,M)=trace(A_i B_M) for all rows i and matchings M. psdRank(n) is the least positive r admitting such a factorization, taken as an infimum over naturals, so it is 0 if none exists. MainClaim asserts that for every real C>0 there is n₀≥4 such that for all even n≥n₀, n^C<psdRank(n), where n^C is real exponentiation; thus the PSD rank of this slack matrix exceeds every fixed polynomial in n eventually.