TheoremStatement: AI-adaptedProof: Literature-sourced

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Bipartite Ramanujan existence and the centered spectrum

Statement

For every integer $d \geq 3$ there is a sequence of finite simple $d$ -regular bipartite graphs whose vertex counts tend to infinity and whose adjacency eigenvalues other than the source's trivial values $d$ and $- d$ lie in $[- 2 \sqrt{d - 1}, 2 \sqrt{d - 1}]$ . Here bipartite means that the vertices have two parts and every edge joins different parts; $d$ -regular means that each vertex has exactly $d$ neighbors. The adjacency matrix $A$ has entry one at adjacent pairs and zero elsewhere.

For each such graph, with $n$ vertices and all-ones matrix $J$ , the centered adjacency norm satisfies $∥ A - (d / n) J ∥_{o p} \geq d > 2 \sqrt{d - 1}$ . Thus the existence theorem with both trivial values excluded does not itself provide the centered absolute-spectrum bound $∥ A - (d / n) J ∥_{o p} \leq 2 \sqrt{d - 1}$ .

External input

The existence and nontrivial-eigenvalue bound in the first paragraph are imported from Marcus, Spielman and Srivastava, Section 2.1 and Theorem 5.5. Their proof starts with a complete bipartite graph and obtains graphs of twice the preceding order; the cited interlacing and lifting machinery is not reconstructed here.

Facts & Assumptions

Given: An integer $d \geq 3$ and a graph supplied by the external input, with bipartition $V = L ⊔ R$ .

Goal: Establish the stated comparison with the centered adjacency norm.

[F1]

The imported theorem supplies the graphs and their nontrivial spectral bound, with both $d$ and $- d$ designated trivial in the bipartite case.

[F2]

For a finite simple graph, adjacency is represented by its symmetric zero-diagonal $0$ – $1$ matrix; its row sums are its vertex degrees (Finite symmetric networks and loop removal).

[F3]

For a symmetric nonnegative matrix with constant row sum $d > 0$ , the centered operator $A - (d / n) J$ agrees with $A$ on the vectors of coordinate sum zero, and its norm is the norm of that restriction (Regular adjacency spectra and normalized expansion).

Proof

1.1givenF2algebra

Counting edges from the two sides gives $d ∣ L ∣ = d ∣ R ∣$ , so $∣ L ∣ = ∣ R ∣$ . Define $v$ to be $1$ on $L$ and $- 1$ on $R$ . It is nonzero and has coordinate sum zero. Each neighbor of a vertex lies in the opposite part, and every vertex has $d$ neighbors; therefore $A v = - d v$ .

2.1F1F3step 1.1algebra∎

By [F3], $(A - (d / n) J) v = A v = - d v$ . The definition of operator norm applied to this nonzero vector gives $∥ A - (d / n) J ∥_{o p} \geq d$ . Since $d \geq 3$ , $(d - 2)^{2} > 0$ , and hence $d^{2} > 4 (d - 1)$ , which gives $d > 2 \sqrt{d - 1}$ . Together with the imported existence statement [F1], this proves the claim and the stated limitation of the bipartite convention.

Depends on

Used by · 1

Asymptotic optimality and existence background for Ramanujan graphs

Dependency tree · 2 levels

Each result is drawn at its shortest distance from this item. Arrows run from prerequisites to the items that use them; this item has a heavier outline. External source nodes link directly to the cited text. The view shows up to two dependency steps; open a prerequisite to continue.

External dependencies

Interlacing families I: Bipartite Ramanujan graphs of all degrees · Section 2.1, printed p. 308; Theorem 5.5 and its proof, printed p. 316

For every integer d at least 3 there is an infinite sequence of d-regular bipartite Ramanujan graphs. In the source convention the eigenvalues d and, for a bipartite graph, -d are trivial; every nontrivial eigenvalue lies between -2 sqrt(d-1) and 2 sqrt(d-1). The proof produces successive graphs with twice as many vertices.

Hypotheses: An integer d at least 3; finite d-regular bipartite graphs, with Ramanujan defined using the source's trivial-eigenvalue convention.

Reading limits: Read Section 2.1 and the statement and proof paragraph of Theorem 5.5. The interlacing-polynomial, signing and 2-lift machinery used by the source was not reconstructed or independently verified. The centered-spectrum comparison below is a local deduction, not a claim attributed to the source.

Sources

Interlacing families I: Bipartite Ramanujan graphs of all degrees · Section 2.1, printed p. 308; Theorem 5.5 and its proof, printed p. 316