Stem-block counting for dominating sets

Abstract

Stem blocks group a stem with all its leaf neighbours. The local counting estimate is Lemma 2.6 of Iain Beaton and Ben Cameron, A Tight Upper Bound on the Average Order of Dominating Sets of a Graph, arXiv:2208.10475. Distinct blocks are disjoint, with the two endpoint descriptions of a two-leaf component identified.

Definition 1.1 (Stem block).

$$\forall V\in \mathrm{Type}\left(\right),[\mathrm{Fintype}\left(V\right)][\mathrm{DecidableEq}\left(V\right)]\forall G\in \mathrm{SimpleGraph}\left(V\right),\forall s\in V,\mathrm{stemBlock}\left(G,s\right)=\mathrm{insert}\left(s,\mathrm{leafNeighbors}\left(G,s\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/DominatingSetAverageBoundStem.stemBlock (✓ std3).

Source. Repository-derived.

Commentary.

The block is the stem together with all its leaf neighbours.

Definition 1.2 (Stem substitution).

$$\forall V\in \mathrm{Type}\left(\right),[\mathrm{Fintype}\left(V\right)][\mathrm{DecidableEq}\left(V\right)]\forall G\in \mathrm{SimpleGraph}\left(V\right),\forall s\in V,\forall S\in \mathrm{Finset}\left(V\right),\forall T\in \mathrm{Finset}\left(V\right),\mathrm{stemSwap}\left(G,s,S,T\right)=\mathrm{union}\left(\mathrm{insert}\left(s,\mathrm{sdiff}\left(S,\mathrm{leafNeighbors}\left(G,s\right)\right)\right),T\right)$$

Formalization. D5/S3/Combinatorics/Graph/DominatingSetAverageBoundStem.stemSwap (✓ std3).

Source. Repository-derived.

Commentary.

Replace every selected leaf neighbour by the stem and a chosen subset of its leaves.

Theorem 1.3 (Substitution preserves domination).

$$\forall V\in \mathrm{Type}\left(\right),[\mathrm{Fintype}\left(V\right)][\mathrm{DecidableEq}\left(V\right)]\forall G\in \mathrm{SimpleGraph}\left(V\right),\forall s\in V,\forall S\in \mathrm{Finset}\left(V\right),\forall T\in \mathrm{Finset}\left(V\right),\mathrm{IsDominating}\left(G,S\right)\Rightarrow \mathrm{IsDominating}\left(G,\mathrm{stemSwap}\left(G,s,S,T\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/DominatingSetAverageBoundStem.stemSwap_dominating (✓ std3). ∎

Source. Repository-derived.

Commentary.

The inserted stem dominates all removed leaves. Any other vertex formerly dominated by a removed leaf is its stem.

Definition 1.4 (Distinct stem blocks).

$$\forall V\in \mathrm{Type}\left(\right),[\mathrm{Fintype}\left(V\right)][\mathrm{DecidableEq}\left(V\right)]\forall G\in \mathrm{SimpleGraph}\left(V\right),\mathrm{stemBlocks}\left(G\right)=\mathrm{image}\left(\mathrm{stemBlock}\left(G\right),\{s\in V|\mathrm{Nonempty}\left(\mathrm{leafNeighbors}\left(G,s\right)\right)\}\right)$$

Formalization. D5/S3/Combinatorics/Graph/DominatingSetAverageBoundStem.stemBlocks (✓ std3).

Source. Repository-derived.

Commentary.

Take the image of the stems under the block map. Equal two-vertex blocks occur once.

Theorem 1.5 (Distinct blocks are disjoint).

$$\forall V\in \mathrm{Type}\left(\right),[\mathrm{Fintype}\left(V\right)][\mathrm{DecidableEq}\left(V\right)]\forall G\in \mathrm{SimpleGraph}\left(V\right),\forall B\in \mathrm{Finset}\left(V\right),\forall C\in \mathrm{Finset}\left(V\right),\left(B\in \mathrm{stemBlocks}\left(G\right)\wedge \left(C\in \mathrm{stemBlocks}\left(G\right)\wedge B\ne C\right)\right)\Rightarrow \mathrm{Disjoint}\left(B,C\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/DominatingSetAverageBoundStem.stemBlocks_pairwiseDisjoint (✓ std3). ∎

Source. Repository-derived.

Commentary.

A leaf has only one neighbour. Overlapping blocks either have the same stem or are the same component consisting of two adjacent leaves.

Definition 1.6 (Active dominating-set family).

$$\forall V\in \mathrm{Type}\left(\right),[\mathrm{Fintype}\left(V\right)][\mathrm{DecidableEq}\left(V\right)]\forall G\in \mathrm{SimpleGraph}\left(V\right),\forall s\in V,\mathrm{activeStemFamily}\left(G,s\right)=\{S\in \mathrm{domSets}\left(G\right)|\neg \mathrm{stemBlock}\left(G,s\right)\subseteq S\}$$

Formalization. D5/S3/Combinatorics/Graph/DominatingSetAverageBoundStem.activeStemFamily (✓ std3).

Source. Repository-derived.

Commentary.

Retain the dominating sets that do not contain the whole stem block.

Theorem 1.7 (Stem-block counting bound).

$$\forall V\in \mathrm{Type}\left(\right),[\mathrm{Fintype}\left(V\right)][\mathrm{DecidableEq}\left(V\right)]\forall G\in \mathrm{SimpleGraph}\left(V\right),\forall s\in V,\mathrm{Nonempty}\left(\mathrm{leafNeighbors}\left(G,s\right)\right)\Rightarrow \sum _{\{}S\in \mathrm{activeStemFamily}\left(G,s\right)\}\mathrm{card}\left(\mathrm{inter}\left(\mathrm{criticalVertices}\left(G,S\right),\mathrm{stemBlock}\left(G,s\right)\right)\right)\le \sum _{\{}S\in \mathrm{activeStemFamily}\left(G,s\right)\}\mathrm{card}\left(\mathrm{sdiff}\left(\mathrm{stemBlock}\left(G,s\right),S\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/DominatingSetAverageBoundStem.activeStemFamily_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Pair each dominating set omitting the stem with its replacement selecting the stem and no leaves. The original has k critical and one omitted block vertex; its replacement has one critical and k omitted block vertices. The injection cancels these contributions. Each remaining active set contains the stem and has one critical block vertex and at least one omitted leaf.

Theorem 1.8 (Strictness for at least three leaves).

$$\forall V\in \mathrm{Type}\left(\right),[\mathrm{Fintype}\left(V\right)][\mathrm{DecidableEq}\left(V\right)]\forall G\in \mathrm{SimpleGraph}\left(V\right),\forall s\in V,3\le \mathrm{leafCount}\left(G,s\right)\Rightarrow \sum _{\{}S\in \mathrm{activeStemFamily}\left(G,s\right)\}\mathrm{card}\left(\mathrm{inter}\left(\mathrm{criticalVertices}\left(G,S\right),\mathrm{stemBlock}\left(G,s\right)\right)\right)<\sum _{\{}S\in \mathrm{activeStemFamily}\left(G,s\right)\}\mathrm{card}\left(\mathrm{sdiff}\left(\mathrm{stemBlock}\left(G,s\right),S\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/DominatingSetAverageBoundStem.activeStemFamily_strict (✓ std3). ∎

Source. Repository-derived.

Commentary.

Select every vertex except the stem, and substitute the stem together with one leaf. At least two leaves remain omitted and only the stem is critical in the block. This set cannot be an empty-leaf replacement, so its positive surplus remains after cancellation.

Theorem 1.9 (Exact balance in star-like blocks).

$$\forall V\in \mathrm{Type}\left(\right),[\mathrm{Fintype}\left(V\right)][\mathrm{DecidableEq}\left(V\right)]\forall G\in \mathrm{SimpleGraph}\left(V\right),\forall s\in V,\mathrm{StarLike}\left(G\right)\Rightarrow \left(\left(\mathrm{leafCount}\left(G,s\right)=1\vee \mathrm{leafCount}\left(G,s\right)=2\right)\Rightarrow \sum _{\{}S\in \mathrm{activeStemFamily}\left(G,s\right)\}\mathrm{card}\left(\mathrm{inter}\left(\mathrm{criticalVertices}\left(G,S\right),\mathrm{stemBlock}\left(G,s\right)\right)\right)=\sum _{\{}S\in \mathrm{activeStemFamily}\left(G,s\right)\}\mathrm{card}\left(\mathrm{sdiff}\left(\mathrm{stemBlock}\left(G,s\right),S\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/DominatingSetAverageBoundStem.activeStemFamily_eq_of_starLike (✓ std3). ∎

Source. Repository-derived.

Commentary.

With one leaf every selected-stem active set has zero gap. With two leaves any selected-stem set omitting both leaves comes from an omitted-stem predecessor: replace the stem by its leaves. Every other neighbour is itself a stem and retains a leaf neighbour, so domination is preserved. The remaining sets have one omitted and one critical block vertex, giving equality.

References

• Truth anchor: D5/S3/Combinatorics/Graph/DominatingSetAverageBoundStem.activeStemFamily
• Truth anchor: D5/S3/Combinatorics/Graph/DominatingSetAverageBoundStem.activeStemFamily_bound
• Truth anchor: D5/S3/Combinatorics/Graph/DominatingSetAverageBoundStem.activeStemFamily_eq_of_starLike
• Truth anchor: D5/S3/Combinatorics/Graph/DominatingSetAverageBoundStem.activeStemFamily_strict
• Truth anchor: D5/S3/Combinatorics/Graph/DominatingSetAverageBoundStem.stemBlock
• Truth anchor: D5/S3/Combinatorics/Graph/DominatingSetAverageBoundStem.stemBlocks
• Truth anchor: D5/S3/Combinatorics/Graph/DominatingSetAverageBoundStem.stemBlocks_pairwiseDisjoint
• Truth anchor: D5/S3/Combinatorics/Graph/DominatingSetAverageBoundStem.stemSwap
• Truth anchor: D5/S3/Combinatorics/Graph/DominatingSetAverageBoundStem.stemSwap_dominating
• Dependency: D5/S3/Combinatorics/Graph/DominatingSetAverageBoundCounting