Proper-Support Closed-Walk Counts are Reconstructible

This module closes the proper-support half of the top-trace programme from Reconstruction.TopTrace. The trace of A^k counts rooted closed walks of length k; the walks whose support misses at least one vertex are confined to a proper induced subgraph, and Kelly's Lemma reconstructs how many induced subgraphs of each isomorphism type G has. Grouping exact supports by isomorphism type therefore makes the whole proper-support count a function of deck data:

• a rooted closed walk with support exactly U is a full-support rooted closed walk of the induced graph G[U] (exactSupportClosedWalkCount_eq_fullSupport_induce);
• the full-support count is a graph-isomorphism invariant (fullSupportClosedWalkCount_eq_of_iso);
• summing over all m-element subsets and regrouping by the isomorphism class of the induced subgraph turns the sum into ∑ classes q, s(q, G) * fullCount(q) (sum_fullSupport_induce_eq), where s(q, G) is the Kelly subgraph count;
• Kelly's Lemma (SameDeck.subgraphCount_eq) matches s(q, G) = s(q, H) for every class on m < |V| vertices, hence SameDeck.properSupportClosedWalkCount_eq.

Combined with charPoly_coeff_zero_eq_of_support_counts_eq, the remaining content of the constant-coefficient (Tutte) reconstruction is exactly the full-support count — the Hamiltonian-cycle sector.

References

• Kelly, P. J. (1942). "On isometric transformations".
• Tutte, W. T. (1979). "All the king's horses".
• Kocay, W. L. (1981). "Some new methods in reconstruction theory".

List/Finset support bookkeeping

The full-support count is an isomorphism invariant

theorem SimpleGraph.fullSupportClosedWalkCount_eq_of_iso {V₁ : Type u_2} {V₂ : Type u_3} [Fintype V₁] [DecidableEq V₁] [Fintype V₂] [DecidableEq V₂] {G₁ : SimpleGraph V₁} {G₂ : SimpleGraph V₂} [DecidableRel G₁.Adj] [DecidableRel G₂.Adj] (φ : G₁ ≃g G₂) (k : ℕ) : G₁.fullSupportClosedWalkCount k = G₂.fullSupportClosedWalkCount k

The full-support rooted-closed-walk count is a graph-isomorphism invariant.

Exact-support walks are full-support walks of the induced subgraph

theorem SimpleGraph.exactSupportClosedWalkCount_eq_fullSupport_induce {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (k : ℕ) (U : Finset V) : G.exactSupportClosedWalkCount k U = (induce (↑U) G).fullSupportClosedWalkCount k

A rooted closed walk of G with support exactly U is the same thing as a full-support rooted closed walk of the induced subgraph G[U]. The counting map pushes a walk of G[U] forward along the inclusion (Walk.map); surjectivity onto the exact-support walks is Walk.induce + Walk.map_induce.

Isomorphism classes of graphs on m labelled vertices

def SimpleGraph.graphIsoSetoid (m : ℕ) : Setoid (SimpleGraph (Fin m))

Graph isomorphism, as a setoid on the simple graphs over Fin m.

Equations

• SimpleGraph.graphIsoSetoid m = { r := fun (F F' : SimpleGraph (Fin m)) => Nonempty (F ≃g F'), iseqv := ⋯ }

def SimpleGraph.GraphIsoClass (m : ℕ) : Type

Isomorphism classes of simple graphs on m labelled vertices. The proper-support regrouping sums over this (finite) index.

Equations

• SimpleGraph.GraphIsoClass m = Quotient (SimpleGraph.graphIsoSetoid m)

noncomputable instance SimpleGraph.instFintypeGraphIsoClass (m : ℕ) : Fintype (GraphIsoClass m)

Equations

• SimpleGraph.instFintypeGraphIsoClass m = Quotient.fintype (SimpleGraph.graphIsoSetoid m)

theorem SimpleGraph.graphIsoClass_mk_eq_mk {m : ℕ} {F F' : SimpleGraph (Fin m)} : ⟦F⟧ = ⟦F'⟧ ↔ Nonempty (F ≃g F')

Two graphs on Fin m represent the same class iff they are isomorphic.

def SimpleGraph.inducedFinGraph {V : Type u_1} (G : SimpleGraph V) {m : ℕ} (U : Finset V) (h : U.card = m) : SimpleGraph (Fin m)

The graph induced on an m-element vertex subset, transported to Fin m along an arbitrary equivalence. Only its isomorphism class is ever used.

Equations

• G.inducedFinGraph U h = SimpleGraph.comap (⇑((finCongr ⋯).symm.trans (Fintype.equivFin ↑↑U).symm)) (SimpleGraph.induce (↑U) G)

def SimpleGraph.inducedFinGraphIso {V : Type u_1} (G : SimpleGraph V) {m : ℕ} (U : Finset V) (h : U.card = m) : G.inducedFinGraph U h ≃g induce (↑U) G

The transported graph is isomorphic to the induced subgraph it came from.

Equations

• G.inducedFinGraphIso U h = { toEquiv := (finCongr ⋯).symm.trans (Fintype.equivFin ↑↑U).symm, map_rel_iff' := ⋯ }

def SimpleGraph.inducedIsoClass {V : Type u_1} (G : SimpleGraph V) (m : ℕ) (U : Finset V) : GraphIsoClass m

The isomorphism class of the subgraph induced on U, as a point of GraphIsoClass m (junk value if U does not have m elements).

Equations

• G.inducedIsoClass m U = if h : U.card = m then ⟦G.inducedFinGraph U h⟧ else ⟦⊥⟧

theorem SimpleGraph.filter_inducedIsoClass_eq_copyFinset {V : Type u_1} [Fintype V] (G : SimpleGraph V) (m : ℕ) (q : GraphIsoClass m) : {U ∈ Finset.powersetCard m Finset.univ | G.inducedIsoClass m U = q} = (Quotient.out q).copyFinset G

The fiber of inducedIsoClass over a class q is exactly Kelly's copyFinset of any representative of q: the m-subsets whose induced subgraph realizes the class.

theorem SimpleGraph.sum_fullSupport_induce_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (k m : ℕ) : ∑ U ∈ Finset.powersetCard m Finset.univ, (induce (↑U) G).fullSupportClosedWalkCount k = ∑ q : GraphIsoClass m, (Quotient.out q).subgraphCount G * (Quotient.out q).fullSupportClosedWalkCount k

Regrouping by isomorphism class. The total number of full-support rooted closed walks over all m-element induced subgraphs is the sum, over isomorphism classes q of graphs on m vertices, of the Kelly subgraph count of q times the full-support walk count of q. This is the bridge from walk counts to deck-reconstructible data.

theorem SimpleGraph.properSupport_eq_sum_isoClasses {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (k : ℕ) : G.properSupportClosedWalkCount k = ∑ m ∈ Finset.range (Fintype.card V), ∑ q : GraphIsoClass m, (Quotient.out q).subgraphCount G * (Quotient.out q).fullSupportClosedWalkCount k

The proper-support closed-walk count, regrouped as a Kelly-weighted sum over isomorphism classes of induced subgraphs of each size m < |V|. Every term on the right is deck-reconstructible.

theorem SimpleGraph.SameDeck.properSupportClosedWalkCount_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) (k : ℕ) : G.properSupportClosedWalkCount k = H.properSupportClosedWalkCount k

The proper-support closed-walk count is reconstructible. Same-deck graphs have, for every length k, the same number of rooted closed k-walks whose support misses at least one vertex: regroup by exact support, identify each sector with full-support walks of the induced subgraph, group by isomorphism class, and apply Kelly's Lemma to each class. This discharges the proper-support hypothesis of SameDeck.charPoly_coeff_zero_eq_of_support_counts_eq; the full-support (Hamiltonian) sector is the only remaining obstacle to the constant coefficient.