Source and verification

This article explains family 126 of the October 6, 2026 OpenAI collection. Research conclusions are attributed to its manuscripts. The review covers statements, introductions, and selected proof mechanisms; it is not an independent verification of the complete proofs.

🏷️ Matching polytopes and semidefinite lifts

For even , a perfect matching of the complete graph pairs every vertex exactly once. Let be the set of these matchings. Its incidence vector has one coordinate for each edge. The perfect-matching polytope is

A real symmetric matrix is positive semidefinite, written , when for every real vector . A semidefinite lift of size represents as an affine image of an affine slice of the cone of PSD matrices.

The size here is the matrix dimension , not the number of scalar entries. Auxiliary coordinates may make a convex set simpler to describe, so a large list of inequalities in the original coordinates does not by itself prove that every lift is large.

This is a formulation-complexity question. An algorithm can construct or optimize a matching without storing one small semidefinite description of the entire matching polytope.

🏷️ Odd-cut slack matrices

For an odd vertex set , let consist of edges with exactly one endpoint in . Every matching crosses this cut an odd positive number of times: internal matching edges cover an even number of vertices of , leaving an odd number matched outside.

The odd-cut inequality is therefore . Its slack at is . The manuscript studies the shifted matrix

For example, with and , a matching can cross the cut once or three times. Its shifted entry is respectively or . For , even the formerly zero slack entries are positive.

The real PSD rank of a nonnegative matrix is the least admitting factors with

The factor entries may be arbitrary real numbers. There is no symmetry, sparsity, equivariance, or bounded-precision assumption. All matrix entries must be reproduced exactly.

🏷️ The shifted lower bound and its endpoint

Manuscript statement

There is an absolute such that, for every fixed , all sufficiently large even satisfy

The threshold may depend on , but the exponential rate does not. (OpenAI, 2026)

The fixed-shift quantifier matters. It does not directly give the same bound for a shift tending to one with .

At , a polynomial-size factorization is explicit. Use diagonal matrices indexed by the edges of , with diagonal entries and . Their trace product is . Thus

The endpoint cannot be included. A positive shift below one also should not be called an arbitrary approximate SDP formulation: the theorem concerns exact factorization of this particular shifted matrix.

🏷️ Recovering unshifted slacks and exact lifts

Suppose has PSD factors of size . Adjoin one scalar block to each factor:

Their trace pairing is the old entry plus , so

Fixing transfers the exponential lower bound to . Adjoining rows for edge nonnegativity cannot decrease rank. These rows and the odd-cut slacks form a slack matrix for the matching polytope within the affine space of degree equations .

The cone-factorization correspondence then identifies this PSD rank with minimum exact lift size. To apply it to an arbitrary affine lift, the source restricts to the smallest face of the PSD cone containing its feasible section, obtaining the required relative-interior condition without increasing size. Redundant tight inequalities do not circumvent the bound. This supplies the claimed exponential lower bound for all exact affine semidefinite lifts, not only a selected symmetric construction.

🏷️ A positive function separated from low-degree squares

The proof begins with parity constraints on an expanding auxiliary graph. Give each incidence at a vertex a bit, prescribing an odd total sum of vertex parities. If the two incidence bits on every edge agreed, summing all vertex constraints would count every edge bit twice and give even total parity, a contradiction. At least one edge must disagree.

Let count disagreeing edges for an allowed incidence assignment , and define

Then pointwise. The source constructs a linear functional that is nonnegative on squares of functions involving few vertex blocks, but for which .

Such a functional is not expectation under a true probability distribution: a true expectation cannot assign a negative value to a positive function. Its positivity is restricted to a low-degree class. Consequently it rules out representing by sums of those low-degree squares, even though unrestricted squares can represent any nonnegative function on a finite set.

This finite parity construction is used here as a combinatorial and analytic interface. The exposition does not develop the associated formal-logic or group-theoretic background.

🏷️ Encoding the parity obstruction in matching

Replace each auxiliary vertex by a cell of a sufficiently large fixed number of vertices. Incidences use designated terminals, while remaining vertices are paired internally. Restrict cuts so that each internal pair receives equal cut bits and the terminal bits obey the prescribed incidence constraints.

Only auxiliary-edge disagreements cross these restricted cuts. The matching-matrix entry becomes precisely the positive function . Therefore a small factorization of the full matching matrix would induce a factorization suitable for this obstruction.

The proof then needs to turn arbitrary PSD factors into approximately low-degree squares. Arbitrary factors begin with no polynomial-degree control, so the parity functional alone is not yet a rank lower bound.

🏷️ Averaging squares without squaring averages

Let be an averaged row factor. Taking square roots of the original factors produces matrix-valued functions, but

in general. The scalar example with equal probabilities gives left side one and right side zero. Replacing the former by the latter would destroy the exact factorization identity.

Instead, the source keeps an exact decomposition

with rectangular matrix functions and separate branches . Local averaging and an orthogonal splitting inequality concentrate each branch’s Fourier coefficients near a branch-dependent character. Their estimates are independent of the factor dimension.

The controlled quantity is the squared Frobenius norm of a weighted Gram matrix, a fourth-order expression in the Fourier coefficients. This choice survives repeated direct-sum decompositions, even though those decompositions add rows to the rectangular factors. A scalar coefficient estimate that grew with the number of rows would not suffice.

After truncation near the central character , multiply the branch by . Since , this preserves its square while moving retained frequencies to low block degree. The low-degree functional is nonnegative on the resulting sum of squares. The source’s quantitative tail bound makes the truncation error too small to explain the negative value , contradicting a factorization of insufficient size. (OpenAI, 2026)

This last argument requires both the norm controlling the tail and the norm of the separating functional; small unweighted Fourier error by itself would not establish the contradiction. The cell-averaging, splitting, and product estimates are the manuscript’s substantive analytic inputs.

🏷️ Scope of the formalization comparison

The repository’s selected comparator statements record superpolynomial lower bounds for the unshifted matching slack matrix and exact affine lifts: every fixed power is eventually exceeded. They do not state the stronger exponential bound for every fixed positive shift below one.

The article therefore distinguishes the manuscript theorem from that documented formalization scope. It does not infer a local verification of either merely from the presence of comparator links.

🏷️ Key steps and proof outlines

Product averaging must retain a sum of matrix squares

The section “Fourier concentration of squares under product averages” starts with a PSD matrix function satisfying . Write its square root as . To average over one coordinate with probabilities , stack the matrices in separate row blocks. The square of this rectangular stack is exactly

Keeping separate blocks is what eliminates unwanted cross terms. Averaging first and then squaring would introduce cross terms and generally give a different PSD matrix. The source adds an extra block label for as well, making products between different new-coordinate values vanish in the Fourier overlap calculation. (OpenAI, 2026)

A fourth-order potential is insensitive to new row dimensions

Let be the Fourier coefficient at frequency of a branch centered at . Penalize distance from that center using , with chosen subject to , where is the local character count, the local averaging variance bound, and the splitting constant. Concatenate the weighted coefficient matrices horizontally into , and let . Then

The second expression measures overlaps, rather than just coefficient sizes. A scalar variance inequality for each local average extends entrywise to matrix-valued functions with the same constant. Character orthogonality subtracts the common mean when two new frequencies differ, so cross-frequency overlaps gain that small variance factor. The splitting lemma organizes the new frequencies into separate branches and bounds the potential’s increase by a factor at most two per coordinate.

After coordinates, the expected total potential is at most . To recover a trace bound, use . The rank is bounded by the number of concatenated columns, even though stacking has greatly enlarged the row count. This is the reason row-dimension growth does not destroy the estimate.

Concentration becomes low degree after a character shift

The weighted Fourier bound implies that coefficients farther than degree cutoff from their center have total squared mass at most times the weighted budget. Truncate those tails. Multiplying the retained branch by its center character moves every retained frequency within block degree of zero. Since , the branch’s square is unchanged.

The parity functional is nonnegative on these low-degree squares, whereas its value on the target positive function is . To obtain a contradiction one must bound the functional applied to the difference between original and truncated squares. The identity shows why tail norms must be paired with norms of the retained and original factors. The source’s quantitative estimates make the resulting error smaller than when factor size is too small.

The shift parameter is fixed below one, so this negative margin is positive and fixed. At it vanishes, and the explicit diagonal factorization already shows polynomial size. Thus the endpoint exclusion has a visible place in the contradiction, rather than being a technical omission.

See Also

🏷️ Manuscripts and verification scope

The family scope page describes selected formalization coverage. The selected formalization statements are superpolynomial lower bounds for the unshifted slack matrix and exact affine lifts. They are weaker than the manuscript’s exponential claim for every fixed positive shift below one. No Lean build, axiom audit, or manuscript-to-formal-statement equivalence check was performed for these notes.

OpenAI collection provides prerequisites and the reading sequence; coverage register records completed and pending families.

🐻  OpenAI 2026. Exponential PSD rank of positively shifted matching matrices.