Top-Trace Closed-Walk Support Split

This module isolates the missing k = |V| trace in the characteristic-polynomial argument. The trace of A^k is the number of rooted closed walks of length k; for k = |V|, we split those walks into two sectors:

• walks whose support is a proper subset of the vertex set;
• walks whose support has full cardinality.

The proper-support sector is further expanded as a sum over exact vertex supports. This is the Lean-shaped version of the next campaign: regroup the proper-support sum by induced-subgraph isomorphism type and use Kelly's Lemma, then handle the full-support/Hamilton-cycle sector by Kocay-style counting.

Main results

• SimpleGraph.trace_adjMatrix_pow_eq_rootedClosedWalkCount
• SimpleGraph.rootedClosedWalkCount_eq_proper_add_full
• SimpleGraph.properSupportClosedWalkCount_eq_sum_exactSupport
• SimpleGraph.trace_adjMatrix_card_eq_of_support_counts_eq

References

• Kocay, W. L. (1981). "Some new methods in reconstruction theory".
• Tutte, W. T. (1979). "All the king's horses".

@[reducible, inline]

abbrev SimpleGraph.RootedClosedWalk {V : Type u_1} (G : SimpleGraph V) (k : ℕ) : Type u_1

A rooted closed walk of length k, packaged as a root together with the walk.

This is the finite type whose cardinality is the trace of the kth adjacency matrix power. The packaging keeps the root explicit, which is useful for splitting the trace by vertex support.

Equations

• G.RootedClosedWalk k = ((v : V) × { p : G.Walk v v // p.length = k })

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

The number of rooted closed walks of length k.

Equations

• G.rootedClosedWalkCount k = Fintype.card (G.RootedClosedWalk k)

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

The number of rooted closed walks of length k whose support is not all of V.

Equations

• G.properSupportClosedWalkCount k = {wp : G.RootedClosedWalk k | (↑wp.snd).support.toFinset.card < Fintype.card V}.card

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

The number of rooted closed walks of length k whose support has full cardinality.

Equations

• G.fullSupportClosedWalkCount k = {wp : G.RootedClosedWalk k | (↑wp.snd).support.toFinset.card = Fintype.card V}.card

def SimpleGraph.exactSupportClosedWalkCount {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (k : ℕ) (U : Finset V) : ℕ

Rooted closed walks of length k with exactly the vertex support U.

Equations

• G.exactSupportClosedWalkCount k U = {wp : G.RootedClosedWalk k | (↑wp.snd).support.toFinset = U}.card

theorem SimpleGraph.support_toFinset_eq_univ_of_card_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) {k : ℕ} (wp : G.RootedClosedWalk k) (hcard : (↑wp.snd).support.toFinset.card = Fintype.card V) : (↑wp.snd).support.toFinset = Finset.univ

A support whose cardinality is |V| is the whole vertex set.

theorem SimpleGraph.rootedClosedWalkCount_eq_proper_add_full {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (k : ℕ) : G.rootedClosedWalkCount k = G.properSupportClosedWalkCount k + G.fullSupportClosedWalkCount k

Every rooted closed walk has either proper support or full support.

theorem SimpleGraph.properSupportClosedWalkCount_eq_sum_exactSupport {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (k : ℕ) : G.properSupportClosedWalkCount k = ∑ U ∈ Finset.univ.powerset with U.card < Fintype.card V, G.exactSupportClosedWalkCount k U

The proper-support part of the trace is the sum over exact proper supports.

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

The full-support part is the exact-support count for univ.

theorem SimpleGraph.trace_adjMatrix_pow_eq_rootedClosedWalkCount {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (k : ℕ) : (adjMatrix ℤ G ^ k).trace = ↑(G.rootedClosedWalkCount k)

The closed-walk count is the trace of the corresponding adjacency-matrix power.

theorem SimpleGraph.trace_adjMatrix_pow_eq_proper_add_full {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (k : ℕ) : (adjMatrix ℤ G ^ k).trace = ↑(G.properSupportClosedWalkCount k) + ↑(G.fullSupportClosedWalkCount k)

theorem SimpleGraph.trace_adjMatrix_card_eq_of_support_counts_eq {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {H : SimpleGraph V} [DecidableRel H.Adj] (hproper : G.properSupportClosedWalkCount (Fintype.card V) = H.properSupportClosedWalkCount (Fintype.card V)) (hfull : G.fullSupportClosedWalkCount (Fintype.card V) = H.fullSupportClosedWalkCount (Fintype.card V)) : (adjMatrix ℤ G ^ Fintype.card V).trace = (adjMatrix ℤ H ^ Fintype.card V).trace

The top trace is reduced to the two support-count subgoals.