Reconstruction Conjecture — Full Characteristic Polynomial

The full characteristic polynomial (including the constant term) is a reconstructible graph invariant.

Main results

• SimpleGraph.SameDeck.charPoly_coeff_zero_eq_of_trace_card_eq — the constant term follows from equality of the top trace tr(A^|V|).
• SimpleGraph.SameDeck.charPoly_coeff_zero_eq_of_support_counts_eq — the constant term follows from equality of the proper-support and full-support top-length closed-walk counts.
• SimpleGraph.SameDeck.charPoly_coeff_zero_eq — the constant term is reconstructible
• SimpleGraph.SameDeck.charPoly_eq — the full characteristic polynomial is reconstructible

Proof outline

From Spectral.lean, we know all non-constant coefficients (c_1, ..., c_{n-1}) are reconstructible. The constant term c_0 = (-1)^n det(A_G) requires additional machinery.

Strategy for c_0

The Cayley–Hamilton trace identity (Newton.lean) gives:

tr(A^n) + c_{n-1} tr(A^{n-1}) + ⋯ + c_1 tr(A) + n · c_0 = 0

This determines c_0 if we know tr(A^k) for all k = 1, ..., n and c_1, ..., c_{n-1}. From TraceReconstruction.lean, traces are reconstructible for k < n. The trace tr(A^n) is not directly covered by Kelly's Lemma, but can be recovered by additional arguments (e.g., the Sachs coefficient formula or walk decomposition over components).

References

• Schwenk, A. J. (1979). "Spectral reconstruction problems".
• Tutte, W. T. (1979). "All the king's horses".

theorem SimpleGraph.SameDeck.charPoly_coeff_zero_eq_of_trace_card_eq {V : Type u_1} [Fintype V] [DecidableEq V] {G H : SimpleGraph V} [DecidableRel G.Adj] [DecidableRel H.Adj] (h : G.SameDeck H) (hV : 3 ≤ Fintype.card V) (htrace : (adjMatrix ℤ G ^ Fintype.card V).trace = (adjMatrix ℤ H ^ Fintype.card V).trace) : (G.charPoly ℤ).coeff 0 = (H.charPoly ℤ).coeff 0

Conditional constant-term reconstruction from the missing top trace.

The Cayley-Hamilton trace identity says ∑ i, c_i tr(A^i) = 0. All non-constant coefficients are already reconstructible, and traces of powers < |V| are reconstructible by SameDeck.trace_adjMatrix_pow_eq. Therefore the constant coefficient follows as soon as the remaining top trace tr(A^|V|) is known to agree.

theorem SimpleGraph.SameDeck.charPoly_coeff_zero_eq_of_support_counts_eq {V : Type u_1} [Fintype V] [DecidableEq V] {G H : SimpleGraph V} [DecidableRel G.Adj] [DecidableRel H.Adj] (h : G.SameDeck H) (hV : 3 ≤ Fintype.card V) (hproper : G.properSupportClosedWalkCount (Fintype.card V) = H.properSupportClosedWalkCount (Fintype.card V)) (hfull : G.fullSupportClosedWalkCount (Fintype.card V) = H.fullSupportClosedWalkCount (Fintype.card V)) : (G.charPoly ℤ).coeff 0 = (H.charPoly ℤ).coeff 0

Conditional constant-term reconstruction from the support split of the missing top trace.

The remaining top trace is the sum of closed walks with proper support and closed walks with full support. Thus the constant term follows from equality of those two support-count pieces.

theorem SimpleGraph.SameDeck.charPoly_coeff_zero_eq {V : Type u_1} [Fintype V] [DecidableEq V] {G H : SimpleGraph V} [DecidableRel G.Adj] [DecidableRel H.Adj] (h : G.SameDeck H) (hV : 3 ≤ Fintype.card V) : (G.charPoly ℤ).coeff 0 = (H.charPoly ℤ).coeff 0

The constant term of the characteristic polynomial is reconstructible.

The constant term c_0 = (-1)^n det(A) is determined by the Cayley–Hamilton trace identity: n · c_0 = -(tr(A^n) + c_{n-1} tr(A^{n-1}) + ⋯ + c_1 tr(A)). All terms on the right are reconstructible: c_1, ..., c_{n-1} from the derivative formula (Spectral.lean) and tr(A^k) from walk counting (TraceReconstruction.lean).

theorem SimpleGraph.SameDeck.charPoly_eq {V : Type u_1} [Fintype V] [DecidableEq V] {G H : SimpleGraph V} [DecidableRel G.Adj] [DecidableRel H.Adj] (h : G.SameDeck H) (hV : 3 ≤ Fintype.card V) : G.charPoly ℤ = H.charPoly ℤ

The full characteristic polynomial is reconstructible.

If two graphs on ≥ 3 vertices have the same deck, their characteristic polynomials (over any integral domain of characteristic zero) are equal.

The proof combines:

1. Non-constant coefficients from the derivative formula (charPoly_coeff_eq)
2. The constant term from trace reconstruction and Cayley–Hamilton (charPoly_coeff_zero_eq)