Source and verification

This article explains family 178 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.

๐Ÿท๏ธ The exact spectral threshold

For a simple -regular graph , the adjacency matrix has eigenvalue on the constant vector. The remaining spectrum is the restriction to , the vectors whose coordinates sum to zero. A two-sided Ramanujan bound requires

The right side is the spectral radius of the infinite -regular tree and is asymptotically optimal for large graphs of fixed degree. Both spectral ends matter. A bipartite regular graph has eigenvalue , which lies in and violates this convention for .

Manuscript claim

For every fixed integer , a deterministic algorithm produces, at every sufficiently large even order , a simple -regular graph whose nonconstant eigenvalues satisfy

It outputs the full adjacency list in bit operations. The size threshold and exponent may depend on . (OpenAI, 2026)

This is not a complexity bound polynomial jointly in and , nor a local adjacency-query algorithm. It asserts even orders; rounding an arbitrary sufficiently large target size upward gives a graph with either or vertices.

๐Ÿท๏ธ Expansion and elementary spectral consequences

The strict bound forces connectedness. If there were two components, a nonconstant vector constant on each component could be chosen orthogonal to , giving another eigenvalue . It also excludes bipartiteness by the eigenvalue observation.

For vertex subsets , write and decompose their indicator vectors into constant and mean-zero parts. The spectral bound gives

Thus edge counts are close to the uniform-density prediction. The left side counts directed incidences when overlap, so the formula should not be interpreted as an unordered internal-edge count without the appropriate factor two.

Near-Ramanujan constructions allow a fixed positive error beyond the tree threshold. The manuscript must remove that error while preserving simplicity, regularity, and the exact number of vertices.

๐Ÿท๏ธ Pairing half-edges with spectral information

Give every vertex labeled stubs; pairing stubs creates edges. The algorithm chooses successive pairings using nonnegative statistics and the method of conditional expectations. Each statistic is discounted by its own controlled growth factor, so one choice can preserve several estimates simultaneously.

Besides spectral confinement, the proof retains entrywise information about inverse matrices and weighted nonbacktracking paths, which never immediately reverse an edge. A cleanup stage pairs nearby unresolved stubs until the remaining boundary vertices are well separated from one another and from short returns.

Low-rank inverse update formulas then control completion of the pairing. The order of estimates matters: squared row energies are reduced before they are used to improve individual entry bounds. The result is a simple regular graph with spectrum inside a narrow neighborhood of the target interval and with the local data needed for repair.

๐Ÿท๏ธ Repairing both spectral edges

Set and , with the fixed . The intermediate graph has spectral excess only of order . For an orthonormal nonconstant eigenbasis , define signed gaps for .

The source controls local mass near either edge:

Summing over vertices shows that only modes lie within distance of an edge. Thus only a comparatively small subspace needs a positive correction.

A valid edge switch replaces by , with four distinct endpoints and absent new edges. Vertex-disjoint valid switches preserve the required graph constraints. Their spectral effect depends on local eigenvector mass, so a global norm estimate alone cannot choose useful switches.

The proof also controls two-by-two endpoint blocks of a truncated inverse on the bulk modes. It does not assume that the full inverse at the tree edge exists. Eliminating the bulk by a Schur complement leaves a quadratic-form problem on near-edge modes. A small bias in the switch distribution gives positive mean correction to the closest modes at both signs, and local mass bounds control fluctuations. The remaining modes retain enough positive slack.

๐Ÿท๏ธ Exact certification and computational scope

The existence of successful switches is followed by a finite deterministic search. If the columns of a rational matrix form a basis of , the final certificate is positive definiteness of the rational matrix

This exactly expresses strict containment of every nonconstant eigenvalue between the two tree edges. Numerical eigenvalues rounded near the threshold would not be an equivalent certificate.

The manuscript proves that its polynomial search contains a passing candidate and analyzes bit precision throughout. These notes do not implement that construction or certify a generated graph. The statement also does not resolve the separate conjecture that every regular graph has a two-lift with the corresponding two-sided bound on new eigenvalues.

๐Ÿท๏ธ Key steps and proof outlines

Eliminate only the bulk, where inversion is legitimate

The repair theorem starts with the three quantitative outputs of the pairing construction: spectral confinement within of both tree edges, local spectral mass bounded by , and typical two-endpoint bulk inverse blocks. Set , , , and use switches. (OpenAI, 2026)

For a switch replacing by , write and . For sign , the precision matrix changes by . Concatenate these columns and blocks for all switches.

Split nonconstant eigenmodes into a near space and a bulk with signed slack at least a cutoff . The old bulk precision is positive definite. With its inverse extended by zero on the near space, define

The ideal two-by-two block of is

with determinant and one eigenvalue of each sign. Closeness to these blocks preserves inertia. Comparing the two Schur complements of the corresponding block matrix proves that the updated bulk is positive definite. Its elimination leaves the exact near matrix

This remains valid when some old near slacks are negative. Inverting the full old precision at the tree edge would not be justified.

Uniform switches cannot repair a negative slack

Let be the inverse ideal block, and for an oriented edge put . Regularity and eigenvector orthogonality imply

For two independent uniform oriented edges, the mean ideal near correction has diagonal entry . Summing switches merely multiplies the old slack by , which preserves its sign. A bias is genuinely necessary.

The source tilts the pair law using cross-edge correlations of the modes with slack below a cutoff in . Local spectral mass makes this density a positive perturbation. Its conditional mean is one when either edge is fixed, so both edge marginals remain uniform. The new mean correction on each targeted mode includes a positive multiple of

where is the positive matrix above. Its size after draws is comparable with . It dominates the possible negative slack. Untargeted near modes already have slack at least and keep a positive margin. The same tilt includes both signs.

Local mass pays for errors and valid switches

Condition on typical original edges for the fixed bulk cutoffs. This loses probability . The local projector estimate bounds one near correction by , so the total conditioning error is . Second moments similarly control the centered near sum and bulk inverse error. After sandwiching by , the latter also contributes to the near matrix.

Endpoint collisions or already-present proposed edges have total probability . Hence a successful collection is vertex-disjoint and preserves simplicity, degrees, and vertex count. The mean positive margin survives every error, proving strict positivity of both signed precisions.

Pairwise independence gives a polynomial search space

Only pairwise independence between switch draws is needed for these second-moment and collision estimates. Approximate the finite pair law by assigning outcomes to residues modulo a polynomial-size prime . Enumerate the seeds and use residues for draw . For distinct , the map to their two residues is invertible, giving exactly uniform independent pairs.

The proof guarantees a passing seed. Each candidate is tested by exact rational positivity of for a contrast basis of . Thus approximate projectors choose a finite search law, while exact arithmetic certifies the final strict threshold. The preceding pairing and local inverse estimates remain essential inputs to this repair argument.

See Also

๐Ÿท๏ธ Manuscripts and verification scope

No family scope page was present at lean/docs/178.md in the pinned snapshot. This does not establish that all related formalization code is absent. 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. Deterministic nonbipartite Ramanujan graphs in every fixed degree.