The Full-Support Walk Sector is the Hamiltonian Sector

Reconstruction.SupportCount reduced the constant coefficient of the characteristic polynomial to the full-support closed-walk count at length n = |V|. This module identifies that sector combinatorially: a rooted closed walk of length n visiting all n vertices has no room to repeat a vertex, so it traverses a Hamiltonian cycle, and conversely every injective homomorphism cycleGraph n →g G unrolls to such a walk. Hence

• fullSupportClosedWalkCount_card_eq_hamiltonianHomCount — G.fullSupportClosedWalkCount |V| = G.hamiltonianHomCount, where hamiltonianHomCount counts the injective graph homomorphisms cycleGraph |V| →g G (each Hamiltonian cycle contributes exactly 2·|V| of them: a starting vertex and a direction);
• SameDeck.charPoly_coeff_zero_eq_of_hamiltonianHomCount_eq — the constant coefficient of the characteristic polynomial follows from agreement of the Hamiltonian homomorphism counts.

Together with SameDeck.properSupportClosedWalkCount_eq, the remaining content of Tutte's constant-term reconstruction (charPoly_coeff_zero_eq) is exactly the deck-reconstructibility of the Hamiltonian-cycle count — Tutte's 1979 theorem, classically proved via Kocay's disconnected-spanning- subgraph counting, which is the project's next staged target.

References

• Tutte, W. T. (1979). "All the king's horses".
• Kocay, W. L. (1981). "Some new methods in reconstruction theory".
• Bondy, J. A. (1991). "A graph reconstructor's manual" (§ Tutte's theorems).

Walks from vertex sequences

def SimpleGraph.walkOfFn {V : Type u_1} (G : SimpleGraph V) (k : ℕ) (g : ℕ → V) : (∀ i < k, G.Adj (g i) (g (i + 1))) → G.Walk (g 0) (g k)

Build a walk from a vertex sequence whose consecutive values are adjacent.

Equations

• G.walkOfFn 0 x x_1 = SimpleGraph.Walk.nil
• G.walkOfFn k.succ x x_1 = SimpleGraph.Walk.cons ⋯ (G.walkOfFn k (fun (i : ℕ) => x (i + 1)) ⋯)

@[simp]

theorem SimpleGraph.walkOfFn_length {V : Type u_1} (G : SimpleGraph V) (k : ℕ) (g : ℕ → V) (h : ∀ i < k, G.Adj (g i) (g (i + 1))) : (G.walkOfFn k g h).length = k

theorem SimpleGraph.walkOfFn_getVert {V : Type u_1} (G : SimpleGraph V) (k : ℕ) (g : ℕ → V) (h : ∀ i < k, G.Adj (g i) (g (i + 1))) (i : ℕ) : i ≤ k → (G.walkOfFn k g h).getVert i = g i

Walks are determined by their vertex sequences

Cycle-graph adjacency bookkeeping

Unrolling an injective homomorphism to a rooted closed walk

The Hamiltonian homomorphism count

noncomputable instance SimpleGraph.instFintypeHomFinCycleGraph_reconstruction {V : Type u_1} [Fintype V] (G : SimpleGraph V) {n : ℕ} : Fintype (cycleGraph n →g G)

Equations

• G.instFintypeHomFinCycleGraph_reconstruction = Fintype.ofInjective (fun (f : SimpleGraph.cycleGraph n →g G) => ⇑f) ⋯

def SimpleGraph.hamiltonianHomCount {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) : ℕ

The number of injective graph homomorphisms cycleGraph |V| →g G. An injective homomorphism from the |V|-cycle is precisely a Hamiltonian cycle traversal: each Hamiltonian cycle of G contributes exactly 2·|V| of them (a choice of starting vertex and of direction). The deck-reconstructibility of this count is Tutte's theorem and is the single remaining ingredient of the constant-coefficient reconstruction.

Equations

• G.hamiltonianHomCount = Fintype.card { f : SimpleGraph.cycleGraph (Fintype.card V) →g G // Function.Injective ⇑f }

theorem SimpleGraph.fullSupportClosedWalkCount_card_eq_hamiltonianHomCount {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hV : 3 ≤ Fintype.card V) : G.fullSupportClosedWalkCount (Fintype.card V) = G.hamiltonianHomCount

The full-support sector is the Hamiltonian sector. A rooted closed walk of length |V| with full support traverses a Hamiltonian cycle: its |V| + 1 vertex slots cover all |V| vertices with the single repetition getVert 0 = getVert |V|, so the first |V| slots are pairwise distinct and consecutive slots are adjacent. Conversely every injective homomorphism from cycleGraph |V| unrolls to such a walk.

theorem SimpleGraph.SameDeck.charPoly_coeff_zero_eq_of_hamiltonianHomCount_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) (hham : G.hamiltonianHomCount = H.hamiltonianHomCount) : (G.charPoly ℤ).coeff 0 = (H.charPoly ℤ).coeff 0

Conditional constant-term reconstruction from the Hamiltonian count alone: with the proper-support sector discharged by Kelly counting (SameDeck.properSupportClosedWalkCount_eq) and the full-support sector identified as the Hamiltonian sector (fullSupportClosedWalkCount_card_eq_hamiltonianHomCount), the constant coefficient of the characteristic polynomial follows from agreement of the Hamiltonian homomorphism counts. The hypothesis hham is exactly Tutte's theorem (1979) that the number of Hamiltonian cycles is reconstructible.

def SimpleGraph.HamiltonianHomCountReconstructible : Prop

Staged target (Tutte 1979). The number of Hamiltonian cycles — here, of injective homomorphisms from the |V|-cycle — is reconstructible from the deck. Proving this (via Kocay's disconnected-spanning-subgraph counting, building on Reconstruction.Kocay) closes SameDeck.charPoly_coeff_zero_eq and with it the full characteristic polynomial. Stated as a Prop-valued definition per the project's staged- target convention.

Equations

• One or more equations did not get rendered due to their size.

theorem SimpleGraph.SameDeck.charPoly_eq_of_hamiltonianHomCount_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) (hham : G.hamiltonianHomCount = H.hamiltonianHomCount) : G.charPoly ℤ = H.charPoly ℤ

The full characteristic polynomial from the Hamiltonian count alone: non-constant coefficients are unconditionally reconstructible (Spectral.lean), and the constant term follows from the Hamiltonian homomorphism counts.

theorem SimpleGraph.charPoly_eq_of_hamiltonianHomCountReconstructible (hrec : HamiltonianHomCountReconstructible) {V : Type} [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 staged target suffices: if the Hamiltonian homomorphism count is deck-reconstructible (Tutte 1979), then same-deck graphs on at least three vertices have equal characteristic polynomials. This makes the sufficiency claim of HamiltonianHomCountReconstructible a theorem rather than prose: closing the staged target closes SameDeck.charPoly_coeff_zero_eq and the full Tutte characteristic-polynomial reconstruction.