Placement Tuples and the Disconnected-Spanning Staged Target

The Tutte/Kocay extraction (strategy note R1, checklist §4) proceeds through tuples of placements: for a family D i of patterns, a tuple of injective homomorphisms D i →g G. This module provides the tuple layer over Reconstruction.HomCount:

• injTupleCount — the number of placement tuples, with the product formula injTupleCount_eq_prod and its deck-invariance SameDeck.injTupleCount_eq (each pattern on < |V| vertices);
• DisjointSpanningTupleCountReconstructible — the staged target: the number of pairwise-vertex-disjoint spanning placement tuples is deck-determined. When the pattern sizes sum to exactly |V|, a spanning tuple is automatically pairwise disjoint, and a pairwise-disjoint tuple of the components of a disconnected graph D is exactly an injective homomorphism placement of D itself — this is the vertex-disjointness collapse that makes all disconnected-spanning-subgraph counts reconstructible in one step, the engine of Tutte's theorem.

References

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

def SimpleGraph.injTupleCount {V : Type u_1} [Fintype V] [DecidableEq V] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {W : ι → Type u_3} [(i : ι) → Fintype (W i)] (D : (i : ι) → SimpleGraph (W i)) (G : SimpleGraph V) : ℕ

The number of placement tuples of the family D: independent choices of an injective homomorphism copy of each pattern.

Equations

• SimpleGraph.injTupleCount D G = Fintype.card ((i : ι) → { f : D i →g G // Function.Injective ⇑f })

theorem SimpleGraph.injTupleCount_eq_prod {V : Type u_1} [Fintype V] [DecidableEq V] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {W : ι → Type u_3} [(i : ι) → Fintype (W i)] (D : (i : ι) → SimpleGraph (W i)) (G : SimpleGraph V) : injTupleCount D G = ∏ i : ι, (D i).injHomCount G

Placement tuples are counted by the product of the individual placement counts.

theorem SimpleGraph.SameDeck.injTupleCount_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) (D : (i : ι) → SimpleGraph (W i)) (hcard : ∀ (i : ι), Fintype.card (W i) < Fintype.card V) : injTupleCount D G = injTupleCount D H

Placement-tuple counts are reconstructible for pattern families on < |V| vertices: immediate from SameDeck.injHomCount_eq and the product formula.

The vertex-disjointness collapse

theorem SimpleGraph.pairwise_disjoint_iff_biUnion_eq_univ {V : Type u_1} [DecidableEq V] {ι : Type u_2} [Fintype ι] [Fintype V] (r : ι → Finset V) (hsum : ∑ i : ι, (r i).card = Fintype.card V) : (Pairwise fun (i j : ι) => Disjoint (r i) (r j)) ↔ Finset.univ.biUnion r = Finset.univ

The collapse, abstractly. A family of finsets whose cardinalities sum to |V| covers the whole vertex set iff it is pairwise disjoint: the union of the family has at most ∑ |r i| elements, with equality exactly in the disjoint case, so at total size |V| covering and disjointness coincide. All arithmetic is kept additive so that omega discharges it.

theorem SimpleGraph.tuple_pairwise_disjoint_iff_spanning {V : Type u_1} [Fintype V] [DecidableEq V] {ι : Type u_2} [Fintype ι] {W : ι → Type u_3} [(i : ι) → Fintype (W i)] {G : SimpleGraph V} (D : (i : ι) → SimpleGraph (W i)) (hsum : ∑ i : ι, Fintype.card (W i) = Fintype.card V) (t : (i : ι) → { f : D i →g G // Function.Injective ⇑f }) : (Pairwise fun (i j : ι) => Disjoint (Set.range ⇑↑(t i)) (Set.range ⇑↑(t j))) ↔ (Finset.univ.biUnion fun (i : ι) => Finset.image (⇑↑(t i)) Finset.univ) = Finset.univ

The vertex-disjointness collapse for placement tuples. When the pattern sizes sum to exactly |V|, a placement tuple is pairwise vertex-disjoint iff its images cover every vertex. This closes the combinatorial half of DisjointSpanningTupleCountReconstructible: the disjoint-tuple count is the spanning-tuple count, whose deck-invariance is the remaining (regrouping) half.

def SimpleGraph.DisjointSpanningTupleCountReconstructible : Prop

Staged target (the vertex-disjointness collapse). For a pattern family whose sizes sum to exactly |V| (each pattern smaller than the host), the number of pairwise-vertex-disjoint placement tuples — equivalently, of spanning placement tuples, since total size |V| forces disjoint images to cover and covering images to be disjoint — is deck-reconstructible.

Taking the family to be the components of a disconnected graph D on |V| vertices, a pairwise-disjoint tuple is exactly an injective placement of D itself, so this target yields Kocay's theorem that all disconnected spanning subgraph counts are reconstructible — the engine of Tutte's characteristic-polynomial and Hamiltonian-count reconstruction. The intended proof: partition all tuples (SameDeck.injTupleCount_eq) by the union of their images and regroup by GraphIsoClass as in Reconstruction.KocayHost; the full-vertex-set fiber is this count. 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.