Kocay's Lemma, Deck Form: Host Cover Counts are Reconstructible

This module proves the deck-level form of Kocay's lemma: for every finite family F = (F i) of pattern graphs, each on fewer vertices than the host, the number of ways to cover the entire host by induced copies of the F i is reconstructible (SameDeck.coverTypeCount_eq).

This is the keystone of the Tutte/Kocay programme (target R1 of research/attacks/strategy-2026-06.md): in the induced-copy world the Kocay identity ∏ᵢ s(Fᵢ, G) = ∑_U c(F, G[U]) has exactly one summand that Kelly's Lemma cannot see — the full-vertex-set term c(F, G). The product on the left is reconstructible (SameDeck.subgraphCount_prod_eq), and every proper summand regroups by the isomorphism class of G[U] into Kelly-weighted class sums via the GraphIsoClass engine of Reconstruction.SupportCount. The host term is therefore deck-determined.

Downstream (per the strategy note), host cover counts for path/cycle families are the raw material from which the disconnected-spanning-subgraph counts and ultimately the Hamiltonian count (HamiltonianHomCountReconstructible, Tutte 1979) are to be extracted.

References

• Kocay, W. L. (1981). "Some new methods in reconstruction theory".
• Tutte, W. T. (1979). "All the king's horses".
• Stark, P. (2025). "Generalization and power of Kocay's lemma in graph reconstruction". arXiv:2509.02604.

theorem SimpleGraph.sum_coverTypeCount_induce_eq {V : Type u_1} [Fintype V] [DecidableEq V] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {W : ι → Type u_3} [(i : ι) → Fintype (W i)] (G : SimpleGraph V) (F : (i : ι) → SimpleGraph (W i)) (m : ℕ) : ∑ U ∈ Finset.powersetCard m Finset.univ, coverTypeCount F (induce (↑U) G) = ∑ q : GraphIsoClass m, (Quotient.out q).subgraphCount G * coverTypeCount F (Quotient.out q)

Regrouping host-subset cover counts by isomorphism class. The total cover count 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 cover count of q. The clone of sum_fullSupport_induce_eq with the iso-invariant coverTypeCount F in place of the walk count.

theorem SimpleGraph.prod_subgraphCount_eq_coverTypeCount_add {V : Type u_1} [Fintype V] [DecidableEq V] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {W : ι → Type u_3} [(i : ι) → Fintype (W i)] (G : SimpleGraph V) (F : (i : ι) → SimpleGraph (W i)) : ∏ i : ι, (F i).subgraphCount G = coverTypeCount F G + ∑ m ∈ Finset.range (Fintype.card V), ∑ q : GraphIsoClass m, (Quotient.out q).subgraphCount G * coverTypeCount F (Quotient.out q)

Kocay's identity, host-isolated form. The product of the Kelly counts splits as the host cover count plus Kelly-weighted class sums over all proper sizes. Every term of the double sum is deck-reconstructible, so this isolates the host term.

theorem SimpleGraph.SameDeck.coverTypeCount_eq {V : Type u_1} [Fintype V] [DecidableEq V] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {W : ι → Type u_3} [(i : ι) → Fintype (W i)] {G H : SimpleGraph V} (h : G.SameDeck H) (F : (i : ι) → SimpleGraph (W i)) (hcard : ∀ (i : ι), Fintype.card (W i) < Fintype.card V) : coverTypeCount F G = coverTypeCount F H

Kocay's lemma, deck form: host cover counts are reconstructible. For every finite family of patterns, each on fewer vertices than the host, same-deck graphs admit the same number of indexed coverings of their full vertex set by induced copies of the patterns.

This strictly extends SameDeck.subgraphCount_prod_eq: the product of Kelly counts is the sum of cover counts over all vertex subsets, and this theorem pins the one summand (the full subset) that Kelly's Lemma cannot reach. It is the entry point for the Tutte/Kocay extraction of spanning-structure counts (disconnected spanning subgraphs, and ultimately the Hamiltonian count).