Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07
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.

Constant vector is a top eigenvector

Statement

For a finite d-regular adjacency-slot multigraph, M1=1, every eigenvalue of M lies in [−1,1], and 1⊥ is invariant. The multiplicity of eigenvalue 1 equals the number of connected components. For a connected graph, −1 is an eigenvalue if and only if its positive slots join opposite parts of a bipartition, so in particular it has no loop slots.

Facts & Assumptions

Given: the objects and hypotheses in the statement above.

[F1]

A finite d-regular adjacency-slot multigraph on V={1,…,n}, with n≥1 and integer d>0, is a symmetric matrix A∈Z≥0n×n with every row sum d. Auv counts slots from u to v; diagonal entries count loop slots. Its normalized adjacency is M=A/d. We use ⟨f,g⟩=n−1∑vf(v)g(v)‾ unless an unnormalized inner product is explicitly specified. An adjacency list records the d destinations per vertex, including repetitions. An ordinary undirected edge has two incidence slots paired by reversal; an ordinary loop has two slots at the same vertex. Such a representation requires even diagonal entries. Any symmetric integer matrix can be converted to it by doubling every slot. Uniform directed-slot sampling chooses one of the nd slots; for a reverse-paired graph it induces the uniform distribution on its nd/2 ordinary edges. Connectivity uses positive off-diagonal entries. When n=1, the mean-zero subspace is {0}. (Regular multigraph and normalized adjacency).

[F2]

Let V be a finite-dimensional real inner product space and let T:V→V be self-adjoint. Then V has an orthonormal basis consisting of eigenvectors of T. (Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis).

Proof

1.1F1F2

The row sums give M1=1; symmetry gives ⟨Mf,1⟩=⟨f,1⟩. The real spectral theorem applies since M is a symmetric endomorphism of a finite-dimensional real inner product space. If Mf=μf and ∣f(v)∣ is maximal and nonzero, then ∣μ∣ ∣f(v)∣≤∑uMvu∣f(u)∣≤∣f(v)∣, proving the interval bound.

2.1step 1.1algebra

Expansion of the squares gives ⟨f,(I−M)f⟩=(2nd)−1∑u,vAuv(f(u)−f(v))2. Its zero vectors are exactly functions constant on each connected component. Thus the eigenspace for eigenvalue one has dimension the component count; the spectral theorem identifies this with multiplicity.

3.1step 1.1algebra∎

Similarly ⟨f,(I+M)f⟩=(2nd)−1∑u,vAuv(f(u)+f(v))2. For a nonzero −1 eigenvector all positive slots force f(v)=−f(u). Connectivity propagates one nonzero absolute value to every vertex, excludes loops, and partitions the vertices by sign. Conversely on such a bipartition the vector taking values +1,−1 has Mf=−f. At n=1 positive degree forces loops and M=[1], so no −1 eigenvalue occurs and the mean-zero space is zero.

Depends on

Used by

Dependency tree · two levels

5 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