we-solve (beta)

Math-2604 · mathematics · Combinatorics

Deterministic nonbipartite Ramanujan graphs in every fixed degree

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For each fixed integer $d>=3$, is there a deterministic polynomial-time algorithm that, for every sufficiently large even n, constructs a simple connected nonbipartite d-regular graph on n vertices with all nontrivial adjacency eigenvalues of absolute value at most 2 sqrt(d-1)?

Short English statement

For each fixed integer $d>=3$, is there a deterministic polynomial-time algorithm that, for every sufficiently large even n, constructs a simple connected nonbipartite d-regular graph on n vertices with all nontrivial adjacency eigenvalues of absolute value at most 2 sqrt(d-1)?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2604-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2604

The algorithmic theorem matches every sufficiently large even order at each fixed degree, with deterministic polynomial bit complexity. Its strict nontrivial eigenvalue inequalities imply the requested non-strict Ramanujan condition as well as connectedness and nonbipartiteness.

Deterministic nonbipartite Ramanujan graphs in every fixed degree

OpenAI's claim

Deterministic nonbipartite Ramanujan graphs: For each fixed $d\ge3$, the claimed deterministic polynomial-time construction gives a simple nonbipartite $d$-regular graph at every sufficiently large even order. All nonconstant eigenvalues lie strictly inside the tree spectral interval.

Mathematical statement of the claimed result

Mathematical claim 1.
For every fixed integer $d\ge3$ there are $n_0(d),k_d$ and a deterministic algorithm which, on every even $n\ge n_0(d)$, outputs an adjacency list using $O_d(n^{k_d})$ bit operations. Its $n$-vertex graph $G$ is simple and has degree $d$ at every vertex. The asserted adjacency eigenvalue condition is \[-2\sqrt{d-1}<\lambda<2\sqrt{d-1}\quad\text{for every eigenvalue of }A_G|_{\mathbf1^\perp}.\] These strict inequalities imply that $G$ is connected and nonbipartite, and in particular imply the requested non-strict Ramanujan bound.

Outline of the argument

Deterministic nonbipartite Ramanujan graphs: Partial stub pairings are assigned matrix pencils whose inverses admit path expansions. Resolving one pair has an explicit low-rank update, allowing positivity to be maintained for both spectral signs. The exposure rule is implemented with finite arithmetic and simplicity constraints, producing a complete pairing and its adjacency list with the required two-sided spectral control.

Formal verification

Deterministic nonbipartite Ramanujan graphs: The pinned catalogue lists no Lean formalization for this result.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources

Go to contribution →