Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-28
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.

For an (n,d,λ)-graph with λ<d, every nontrivial cut has many crossing edges

Statement

Let G be an (n,d,λ)-graph with adjacency matrix A. For every nonempty proper subset SV(G), writing e(S,V(G)S) for the number of edges crossing the cut, one has

e(S,V(G)S)(dλ)S(nS)n.

In particular, if λ<d, then G is connected.

Facts & Assumptions

Given: An (n,d,λ)-graph G and a nonempty proper subset SV(G).

[F1]

In an (n,d,λ)-graph, the graph is d-regular and its second-largest adjacency eigenvalue is at most λ (An (n,d,λ)-graph and an expander).

[L1]

Courant-Fischer characterises the second-largest eigenvalue as a max-min Rayleigh quotient, so every nonzero vector orthogonal to the all-ones eigenvector has Rayleigh quotient at most λ2 (Courant-Fischer min-max principle for self-adjoint endomorphisms on finite-dimensional real inner product spaces, The Rayleigh quotient of a nonzero vector for a self-adjoint endomorphism).

Proof

technique · direct
1.1

Let 1S be the indicator vector of S, and put x:=1SSn1. Then x0 because S is nonempty and proper, and x is orthogonal to 1. Since G is d-regular by [F1], the vector 1 is an adjacency eigenvector with eigenvalue d, so [L1] gives xTAxλxTx.

F1L1algebra
2.1

A direct computation gives xTx=S(nS)n and xTAx=dS(nS)ne(S,V(G)S), because 1STA1S counts twice the edges internal to S, while 1STA1=dS. Substituting these expressions into step 1.1 yields dS(nS)ne(S,V(G)S)λS(nS)n, which rearranges to the claimed cut bound.

step 1.1F1algebra
3.1

If λ<d and G were disconnected, [L2] would provide a connected component C with CV(G) and e(C,V(G)C)=0. But step 2.1 would then force 0(dλ)C(nC)n>0, a contradiction. So G is connected.

step 2.1L2
4.1

Step 2.1 gives the edge-expansion inequality, and step 3.1 gives the connectedness consequence.

step 2.1step 3.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

15 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources