# Exponential semidefinite complexity of perfect matching

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Exponential PSD rank of positively shifted matching matrices](../../preprints/Exponential-PSD-rank-of-positively-shifted-matching-matrices-October-5-2026/shifted-matching-psd.pdf)

## Scope

The paper proves exponential PSD-rank lower bounds for positively shifted matching matrices. The linked formalization records the related superpolynomial lower bounds: for every fixed $C>0$, the PSD rank of the selected perfect-matching slack matrix exceeds $n^C$ for all sufficiently large even $n$. Every exact affine semidefinite lift of the perfect-matching polytope likewise requires matrix size greater than $n^C$.

These selected statements give superpolynomial growth. They do not state the paper's exponential bound for every fixed positive shift.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Superpolynomial lower bound for affine semidefinite lifts | [MatchingAffineLift.lean](../ComparatorChallenges/MatchingAffineLift.lean) |
| Superpolynomial PSD rank for the perfect-matching slack matrix | [MatchingPSD.lean](../ComparatorChallenges/MatchingPSD.lean) |