Reconstruction Conjecture — Trace Reconstructibility

The trace of powers of the adjacency matrix is a reconstructible invariant for powers less than the number of vertices.

Main results

• SimpleGraph.SameDeck.trace_adjMatrix_pow_eq — tr(A_G^k) = tr(A_H^k) for k < |V|

Proof outline

By strong induction on k, using Newton's identity (Newton.lean):

tr(A^k) + ∑_{j=1}^{k-1} c_{N-j} · tr(A^{k-j}) + k · c_{N-k} = 0

For k = 0: both traces equal |V| (trace of the identity matrix).

For 1 ≤ k < |V|: the characteristic polynomial coefficients c_1, ..., c_{N-1} are reconstructible (charPoly_coeff_eq), and the lower-order traces are reconstructible by the induction hypothesis. Newton's identity then determines tr(A^k) uniquely.

References

• Schwenk, A. J. (1979). "Spectral reconstruction problems".
• Newton, I. (1707). Arithmetica Universalis.

noncomputable def SimpleGraph.closedWalkCount {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (k : ℕ) : ℤ

The trace of the k-th power of the adjacency matrix counts closed walks of length k. This is the diagonal sum ∑_v (A^k)_{vv}.

Equations

• G.closedWalkCount k = (SimpleGraph.adjMatrix ℤ G ^ k).trace

theorem SimpleGraph.SameDeck.trace_adjMatrix_pow_eq {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {H : SimpleGraph V} [DecidableRel H.Adj] (h : G.SameDeck H) (_hV : 3 ≤ Fintype.card V) {k : ℕ} (hk : k < Fintype.card V) : (adjMatrix ℤ G ^ k).trace = (adjMatrix ℤ H ^ k).trace

Traces of adjacency matrix powers are reconstructible for powers < |V|.

tr(A_G^k) = tr(A_H^k) for all k < |V|. The proof uses Newton's identity to express tr(A^k) in terms of characteristic polynomial coefficients (reconstructible by charPoly_coeff_eq) and lower-order traces (reconstructible by the induction hypothesis).