Reconstruction Conjecture — Spectral Graph Theory

We develop spectral graph theory tools for the reconstruction conjecture. The central result is the derivative formula for graph characteristic polynomials:

$$\varphi'(G, x) = \sum_v \varphi(G - v, x)$$

where $\varphi(G, x) = \det(xI - A_G)$ is the characteristic polynomial of the adjacency matrix. This implies that if two graphs have the same deck, they share the same characteristic polynomial derivative — and therefore agree on all non-constant coefficients.

Main definitions

• SimpleGraph.charPoly — characteristic polynomial of a graph

Main results

• SimpleGraph.adjMatrix_induce — adjacency matrix of induced subgraph = principal submatrix
• SimpleGraph.charPoly_deleteVert — charPoly(G - v) = charpoly of principal submatrix
• SimpleGraph.charPoly_eq_of_iso — isomorphic graphs have equal characteristic polynomials
• SimpleGraph.charPoly_derivative_eq_sum — derivative formula
• SimpleGraph.SameDeck.charPoly_derivative_eq — same deck → same char. poly. derivative
• SimpleGraph.SameDeck.charPoly_coeff_eq — same deck → same non-constant coefficients

References

• Kelly, P. J. (1942). "On isometric transformations".
• Tutte, W. T. (1979). "All the king's horses".
• Schwenk, A. J. (1979). "Spectral reconstruction problems".

Phase 1: Foundation — Graph-Matrix Bridge

theorem SimpleGraph.adjMatrix_induce {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : Set V) [DecidablePred fun (x : V) => x ∈ s] (α : Type u_2) [Zero α] [One α] : adjMatrix α (induce s G) = (adjMatrix α G).submatrix Subtype.val Subtype.val

The adjacency matrix of G.induce s equals the principal submatrix of G.adjMatrix indexed by s. This bridges graph-theoretic vertex deletion and matrix-theoretic principal submatrices.

noncomputable def SimpleGraph.charPoly {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [CommRing R] : Polynomial R

The characteristic polynomial of a graph, defined as the characteristic polynomial of its adjacency matrix: charPoly G R = det(XI - A_G).

Equations

• G.charPoly R = (SimpleGraph.adjMatrix R G).charpoly

theorem SimpleGraph.charPoly_deleteVert {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) (R : Type u_2) [CommRing R] : (G.deleteVert v).charPoly R = ((adjMatrix R G).submatrix Subtype.val Subtype.val).charpoly

The characteristic polynomial of G.deleteVert v equals the characteristic polynomial of the principal submatrix of G.adjMatrix obtained by deleting row and column v.

theorem SimpleGraph.charPoly_eq_of_iso {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {W : Type u_2} [Fintype W] [DecidableEq W] {H : SimpleGraph W} [DecidableRel H.Adj] (φ : G ≃g H) (R : Type u_3) [CommRing R] : G.charPoly R = H.charPoly R

Isomorphic graphs have equal characteristic polynomials. The proof goes through matrix reindexing: a graph isomorphism φ : G ≃g H yields a permutation of indices that conjugates the adjacency matrix.

Phase 2: The Derivative Formula

Phase 2a: Charmatrix entry derivatives

theorem SimpleGraph.derivative_charmatrix_apply_eq {n : Type u_2} [Fintype n] [DecidableEq n] {R : Type u_3} [CommRing R] (M : Matrix n n R) (i : n) : Polynomial.derivative (M.charmatrix i i) = 1

theorem SimpleGraph.derivative_charmatrix_apply_ne {n : Type u_2} [Fintype n] [DecidableEq n] {R : Type u_3} [CommRing R] (M : Matrix n n R) {i j : n} (h : i ≠ j) : Polynomial.derivative (M.charmatrix i j) = 0

Phase 2b: Charmatrix-submatrix bridge

theorem SimpleGraph.charmatrix_submatrix {n : Type u_2} [Fintype n] [DecidableEq n] {R : Type u_3} [CommRing R] {l : Type u_4} [Fintype l] [DecidableEq l] (M : Matrix n n R) (f : l → n) (hf : Function.Injective f) : (M.submatrix f f).charmatrix = M.charmatrix.submatrix f f

Phase 2c: Derivative of determinant for charmatrices

theorem SimpleGraph.derivative_det_charmatrix {n : Type u_2} [Fintype n] [DecidableEq n] {R : Type u_3} [CommRing R] (M : Matrix n n R) : Polynomial.derivative M.charmatrix.det = ∑ k : n, (M.charmatrix.submatrix Subtype.val Subtype.val).det

The derivative of the determinant of a charmatrix equals the sum of determinants of its principal submatrices. This is the core linear-algebra fact behind the derivative formula for graph characteristic polynomials.

Phase 2d: Assembly — the graph-theoretic derivative formula

theorem SimpleGraph.charPoly_derivative_eq_sum {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_3) [CommRing R] : Polynomial.derivative (G.charPoly R) = ∑ v : V, (G.deleteVert v).charPoly R

The derivative formula for graph characteristic polynomials.

The derivative of the characteristic polynomial of G equals the sum of characteristic polynomials of all vertex-deleted subgraphs:

$$\varphi'(G, x) = \sum_{v \in V} \varphi(G - v, x)$$

This is a consequence of the Leibniz formula for the determinant and the product rule for polynomial differentiation. The key insight is that differentiating det(xI - A) via the Leibniz expansion yields, for each diagonal position v, the determinant of the (v,v)-cofactor of the charmatrix, which equals charPoly(G - v).

Phase 3: Reconstructibility Corollaries

theorem SimpleGraph.SameDeck.charPoly_derivative_eq {V : Type u_1} [Fintype V] [DecidableEq V] {G H : SimpleGraph V} [DecidableRel G.Adj] [DecidableRel H.Adj] (h : G.SameDeck H) (R : Type u_2) [CommRing R] : Polynomial.derivative (G.charPoly R) = Polynomial.derivative (H.charPoly R)

The characteristic polynomial derivative is reconstructible.

If two graphs have the same deck, they have the same characteristic polynomial derivative. This follows from the derivative formula and the fact that isomorphic graphs have equal characteristic polynomials.

theorem SimpleGraph.SameDeck.charPoly_coeff_eq {V : Type u_1} [Fintype V] [DecidableEq V] {G H : SimpleGraph V} [DecidableRel G.Adj] [DecidableRel H.Adj] (h : G.SameDeck H) (R : Type u_2) [CommRing R] [IsDomain R] [CharZero R] {k : ℕ} (hk : 1 ≤ k) : (G.charPoly R).coeff k = (H.charPoly R).coeff k

Non-constant coefficients of the characteristic polynomial are reconstructible.

If two graphs have the same deck, all coefficients of their characteristic polynomials of degree ≥ 1 agree. Since charPoly is monic of degree |V|, the derivative determines all coefficients of degree ≥ 1; only the constant term (-1)^n det(A) is not immediately recovered.

(The constant term IS recoverable via Tutte's deeper theorem using Kelly's Lemma and the Sachs coefficient theorem, but that requires significantly more machinery.)