Strong domination under clique gluing

Abstract

The strong domination number of a clique gluing satisfies Inequality (4) of Alikhani, Ghanbari and Henning for every clique size at least two.

Definition 1.1 (Strong dominating sets).

$$\forall (V:Type),[\mathrm{Fintype}\left(V\right)]\forall (G:\mathrm{SimpleGraph}\left(V\right)),[\mathrm{DecidableRel}\left(\mathrm{SimpleGraph}.\mathrm{Adj}\left(G\right)\right)]\forall (D:\mathrm{Finset}\left(V\right)),\mathrm{IsStrongDominatingSet}\left(G,D\right)\iff (\forall (x:V),(\neg x\in D)\Rightarrow (\exists (y:V),(y\in D)\wedge ((\mathrm{SimpleGraph}.\mathrm{Adj}\left(G,x,y\right))\wedge (\mathrm{SimpleGraph}.\mathrm{degree}\left(G,x\right)\le \mathrm{SimpleGraph}.\mathrm{degree}\left(G,y\right)))))$$

Formalization. D5/S3/Combinatorics/Graph/Domination/AlikhaniGhanbariHenningCliqueGluing.IsStrongDominatingSet (✓ std3).

Citation. Saeid Alikhani, Nima Ghanbari, Michael A. Henning (2026). Strong domination number of graphs from primary subgraphs. DOI: 10.2989/16073606.2025.2574046. URL: https://www.tandfonline.com/doi/full/10.2989/16073606.2025.2574046.

Commentary.

Abstract, p. 195: “A set D of vertices is a strong dominating set in a graph G, if for every vertex x ∈ V(G) \ D there is a vertex y ∈ D with xy ∈ E(G) and deg(x) ≤ deg(y). The strong domination number γst(G) of G is the minimum cardinality of a strong dominating set in G.” Finite sets encode vertex subsets. SimpleGraph.degree counts each distinct neighbour once.

Definition 1.2 (The minimum cardinality).

$$\forall (V:Type),[\mathrm{Fintype}\left(V\right)]\forall (G:\mathrm{SimpleGraph}\left(V\right)),[\mathrm{DecidableRel}\left(\mathrm{SimpleGraph}.\mathrm{Adj}\left(G\right)\right)]\mathrm{strongDominationNumber}\left(G\right)=\mathrm{sInf}\left(\{k:\mathbb{N}\mid \exists (D:\mathrm{Finset}\left(V\right)),(\mathrm{IsStrongDominatingSet}\left(G,D\right))\wedge (\mathrm{Finset}.\mathrm{card}\left(D\right)=k)\}\right)$$

Formalization. D5/S3/Combinatorics/Graph/Domination/AlikhaniGhanbariHenningCliqueGluing.strongDominationNumber (✓ std3).

Citation. Saeid Alikhani, Nima Ghanbari, Michael A. Henning (2026). Strong domination number of graphs from primary subgraphs. DOI: 10.2989/16073606.2025.2574046. URL: https://www.tandfonline.com/doi/full/10.2989/16073606.2025.2574046.

Commentary.

Abstract, p. 195: “A set D of vertices is a strong dominating set in a graph G, if for every vertex x ∈ V(G) \ D there is a vertex y ∈ D with xy ∈ E(G) and deg(x) ≤ deg(y). The strong domination number γst(G) of G is the minimum cardinality of a strong dominating set in G.” The full vertex set is strong dominating, so the natural-number infimum of attained sizes is attained.

Definition 1.3 (The second graph’s vertex map).

$$\forall (r:\mathbb{N}),\forall (V1:Type),\forall (V2:Type),[\mathrm{DecidableEq}\left(V2\right)]\forall (A:\mathrm{Function}.\mathrm{Embedding}\left(\mathrm{Fin}\left(r\right),V1\right)),\forall (B:\mathrm{Function}.\mathrm{Embedding}\left(\mathrm{Fin}\left(r\right),V2\right)),\forall (w:V2),\mathrm{embedRight}\left(A,B,w\right)=(\mathrm{if}h:w\in \mathrm{Set}.\mathrm{range}\left(B\right)\mathrm{then}\mathrm{Sum}.\mathrm{inl}\left(A\left(\mathrm{Function}.\mathrm{Embedding}.\mathrm{invOfMemRange}\left(B,⟨w,h⟩\right)\right)\right)\mathrm{else}\mathrm{Sum}.\mathrm{inr}\left(⟨w,h⟩\right))$$

Formalization. D5/S3/Combinatorics/Graph/Domination/AlikhaniGhanbariHenningCliqueGluing.embedRight (✓ std3).

Source. Repository-derived.

Acknowledgement. Saeid Alikhani, Nima Ghanbari, Michael A. Henning (2026). Strong domination number of graphs from primary subgraphs. DOI: 10.2989/16073606.2025.2574046. URL: https://www.tandfonline.com/doi/full/10.2989/16073606.2025.2574046.

Commentary.

A vertex B i maps to Sum.inl (A i). A vertex outside the range of B maps to the right summand, with its proof of exclusion. Function.Embedding.invOfMemRange recovers the unique index in the range of B.

Definition 1.4 (The glued graph).

$$\forall (r:\mathbb{N}),\forall (V1:Type),\forall (V2:Type),[\mathrm{DecidableEq}\left(V2\right)]\forall (G1:\mathrm{SimpleGraph}\left(V1\right)),\forall (G2:\mathrm{SimpleGraph}\left(V2\right)),\forall (A:\mathrm{Function}.\mathrm{Embedding}\left(\mathrm{Fin}\left(r\right),V1\right)),\forall (B:\mathrm{Function}.\mathrm{Embedding}\left(\mathrm{Fin}\left(r\right),V2\right)),\mathrm{glue}\left(G1,G2,A,B\right)=\mathrm{SimpleGraph}.\mathrm{fromRel}\left((\mathrm{fun}(p:\mathrm{Sum}\left(V1,\{w:V2\mid \neg w\in \mathrm{Set}.\mathrm{range}\left(B\right)\}\right))\mapsto (\mathrm{fun}(q:\mathrm{Sum}\left(V1,\{w:V2\mid \neg w\in \mathrm{Set}.\mathrm{range}\left(B\right)\}\right))\mapsto (\exists (x:V1),\exists (y:V1),(p=\mathrm{Sum}.\mathrm{inl}\left(x\right))\wedge ((q=\mathrm{Sum}.\mathrm{inl}\left(y\right))\wedge (\mathrm{SimpleGraph}.\mathrm{Adj}\left(G1,x,y\right))))\vee (\exists (x:V2),\exists (y:V2),(p=\mathrm{embedRight}\left(A,B,x\right))\wedge ((q=\mathrm{embedRight}\left(A,B,y\right))\wedge (\mathrm{SimpleGraph}.\mathrm{Adj}\left(G2,x,y\right))))))\right)$$

Formalization. D5/S3/Combinatorics/Graph/Domination/AlikhaniGhanbariHenningCliqueGluing.glue (✓ std3).

Citation. Saeid Alikhani, Nima Ghanbari, Michael A. Henning (2026). Strong domination number of graphs from primary subgraphs. DOI: 10.2989/16073606.2025.2574046. URL: https://www.tandfonline.com/doi/full/10.2989/16073606.2025.2574046.

Commentary.

Section 1, p. 196: “Choose a clique of cardinality r from each Gi, i = 1, 2, and form a new graph G from the union of G1 and G2 by identifying the two chosen r-cliques in an arbitrary manner.” The vertex type retains every vertex of G1 and exactly the vertices of G2 outside B. SimpleGraph.fromRel combines the two edge relations; repeated edges of the common clique occur once.

Definition 1.5 (External neighbours of a clique vertex).

$$\forall (r:\mathbb{N}),\forall (V1:Type),[\mathrm{Fintype}\left(V1\right)][\mathrm{DecidableEq}\left(V1\right)]\forall (G1:\mathrm{SimpleGraph}\left(V1\right)),[\mathrm{DecidableRel}\left(\mathrm{SimpleGraph}.\mathrm{Adj}\left(G1\right)\right)]\forall (A:\mathrm{Function}.\mathrm{Embedding}\left(\mathrm{Fin}\left(r\right),V1\right)),\forall (i:\mathrm{Fin}\left(r\right)),X\left(G1,A,i\right)=\mathrm{SimpleGraph}.\mathrm{neighborFinset}\left(G1,A\left(i\right)\right)\setminus \mathrm{Finset}.\mathrm{map}\left(A,\mathrm{Finset}.\mathrm{univ}\right)$$

Formalization. D5/S3/Combinatorics/Graph/Domination/AlikhaniGhanbariHenningCliqueGluing.X (✓ std3).

Citation. Saeid Alikhani, Nima Ghanbari, Michael A. Henning (2026). Strong domination number of graphs from primary subgraphs. DOI: 10.2989/16073606.2025.2574046. URL: https://www.tandfonline.com/doi/full/10.2989/16073606.2025.2574046.

Commentary.

Problem 1, p. 202: “For r ≥ 2, let G1 and G2 be connected graphs both of order at least r + 1 that contain r-cliques A = {u1, u2, …, ur} and B = {v1, v2, …, vr}, respectively. Let Xi = NG1(ui) \ A and Yi = NG2(vi) \ B for i ∈ [r], and let ΣX,Y = Σ_{i=1}^r |Xi| + Σ_{i=1}^r |Yi|. Let G ∈ G1 ∪Kr G2 be obtained by a Kr-gluing of the graphs G1 and G2 by identifying the cliques A and B, where we identify the vertices ui and vi for i ∈ [r]. Determine a best possible lower bound on γst(G) in terms of γst(G1), γst(G2) and ΣX,Y. In particular, is it true that γst(G) ≥ γst(G1) + γst(G2) − 1 − ΣX,Y? (4)” X G1 A i is Xi, and X G2 B i is Yi. Finset.univ.map A is the enumerated clique. Index i in Fin r corresponds to index i+1 in the paper.

Definition 1.6 (The total external-neighbour count).

$$\forall (r:\mathbb{N}),\forall (V1:Type),\forall (V2:Type),[\mathrm{Fintype}\left(V1\right)][\mathrm{DecidableEq}\left(V1\right)][\mathrm{Fintype}\left(V2\right)][\mathrm{DecidableEq}\left(V2\right)]\forall (G1:\mathrm{SimpleGraph}\left(V1\right)),[\mathrm{DecidableRel}\left(\mathrm{SimpleGraph}.\mathrm{Adj}\left(G1\right)\right)]\forall (G2:\mathrm{SimpleGraph}\left(V2\right)),[\mathrm{DecidableRel}\left(\mathrm{SimpleGraph}.\mathrm{Adj}\left(G2\right)\right)]\forall (A:\mathrm{Function}.\mathrm{Embedding}\left(\mathrm{Fin}\left(r\right),V1\right)),\forall (B:\mathrm{Function}.\mathrm{Embedding}\left(\mathrm{Fin}\left(r\right),V2\right)),\mathrm{sigmaXY}\left(G1,G2,A,B\right)=(\sum _{i:\mathrm{Fin}\left(r\right)}\mathrm{Finset}.\mathrm{card}\left(X\left(G1,A,i\right)\right))+(\sum _{i:\mathrm{Fin}\left(r\right)}\mathrm{Finset}.\mathrm{card}\left(X\left(G2,B,i\right)\right))$$

Formalization. D5/S3/Combinatorics/Graph/Domination/AlikhaniGhanbariHenningCliqueGluing.sigmaXY (✓ std3).

Citation. Saeid Alikhani, Nima Ghanbari, Michael A. Henning (2026). Strong domination number of graphs from primary subgraphs. DOI: 10.2989/16073606.2025.2574046. URL: https://www.tandfonline.com/doi/full/10.2989/16073606.2025.2574046.

Commentary.

Problem 1, p. 202: “For r ≥ 2, let G1 and G2 be connected graphs both of order at least r + 1 that contain r-cliques A = {u1, u2, …, ur} and B = {v1, v2, …, vr}, respectively. Let Xi = NG1(ui) \ A and Yi = NG2(vi) \ B for i ∈ [r], and let ΣX,Y = Σ_{i=1}^r |Xi| + Σ_{i=1}^r |Yi|. Let G ∈ G1 ∪Kr G2 be obtained by a Kr-gluing of the graphs G1 and G2 by identifying the cliques A and B, where we identify the vertices ui and vi for i ∈ [r]. Determine a best possible lower bound on γst(G) in terms of γst(G1), γst(G2) and ΣX,Y. In particular, is it true that γst(G) ≥ γst(G1) + γst(G2) − 1 − ΣX,Y? (4)” Each cardinality is counted separately for each clique vertex; a vertex adjacent to several clique vertices contributes several times.

Definition 1.7 (Inequality (4) on the whole stated domain).

$$claim\iff (\forall (r:\mathbb{N}),(2\le r)\Rightarrow (\forall (V1:Type),\forall (V2:Type),[\mathrm{Fintype}\left(V1\right)][\mathrm{DecidableEq}\left(V1\right)][\mathrm{Fintype}\left(V2\right)][\mathrm{DecidableEq}\left(V2\right)]\forall (G1:\mathrm{SimpleGraph}\left(V1\right)),\forall (G2:\mathrm{SimpleGraph}\left(V2\right)),\forall (A:\mathrm{Function}.\mathrm{Embedding}\left(\mathrm{Fin}\left(r\right),V1\right)),\forall (B:\mathrm{Function}.\mathrm{Embedding}\left(\mathrm{Fin}\left(r\right),V2\right)),(\mathrm{SimpleGraph}.\mathrm{Connected}\left(G1\right))\Rightarrow ((\mathrm{SimpleGraph}.\mathrm{Connected}\left(G2\right))\Rightarrow ((r+1\le \mathrm{Fintype}.\mathrm{card}\left(V1\right))\Rightarrow ((r+1\le \mathrm{Fintype}.\mathrm{card}\left(V2\right))\Rightarrow ((\mathrm{SimpleGraph}.\mathrm{IsClique}\left(G1,\mathrm{Set}.\mathrm{range}\left(A\right)\right))\Rightarrow ((\mathrm{SimpleGraph}.\mathrm{IsClique}\left(G2,\mathrm{Set}.\mathrm{range}\left(B\right)\right))\Rightarrow ((\mathrm{strongDominationNumber}\left(G1\right):\mathbb{Z})+(\mathrm{strongDominationNumber}\left(G2\right):\mathbb{Z})-1-(\mathrm{sigmaXY}\left(G1,G2,A,B\right):\mathbb{Z})\le (\mathrm{strongDominationNumber}\left(\mathrm{glue}\left(G1,G2,A,B\right)\right):\mathbb{Z})))))))))$$

Formalization. D5/S3/Combinatorics/Graph/Domination/AlikhaniGhanbariHenningCliqueGluing.claim (✓ std3).

Source. Repository-derived.

Acknowledgement. Saeid Alikhani, Nima Ghanbari, Michael A. Henning (2026). Strong domination number of graphs from primary subgraphs. DOI: 10.2989/16073606.2025.2574046. URL: https://www.tandfonline.com/doi/full/10.2989/16073606.2025.2574046.

Commentary.

Problem 1, p. 202: “For r ≥ 2, let G1 and G2 be connected graphs both of order at least r + 1 that contain r-cliques A = {u1, u2, …, ur} and B = {v1, v2, …, vr}, respectively. Let Xi = NG1(ui) \ A and Yi = NG2(vi) \ B for i ∈ [r], and let ΣX,Y = Σ_{i=1}^r |Xi| + Σ_{i=1}^r |Yi|. Let G ∈ G1 ∪Kr G2 be obtained by a Kr-gluing of the graphs G1 and G2 by identifying the cliques A and B, where we identify the vertices ui and vi for i ∈ [r]. Determine a best possible lower bound on γst(G) in terms of γst(G1), γst(G2) and ΣX,Y. In particular, is it true that γst(G) ≥ γst(G1) + γst(G2) − 1 − ΣX,Y? (4)” The displayed proposition answers the final question affirmatively. The two graph orders are Fintype.card, the cliques are the ranges of embeddings from Fin r, and all subtraction is in the integers. Adjacency of the glued graph is decided classically.

Theorem 1.8 (The lower bound for every r at least two).

$$\forall (r:\mathbb{N}),(2\le r)\Rightarrow (\forall (V1:Type),\forall (V2:Type),[\mathrm{Fintype}\left(V1\right)][\mathrm{DecidableEq}\left(V1\right)][\mathrm{Fintype}\left(V2\right)][\mathrm{DecidableEq}\left(V2\right)]\forall (G1:\mathrm{SimpleGraph}\left(V1\right)),\forall (G2:\mathrm{SimpleGraph}\left(V2\right)),\forall (A:\mathrm{Function}.\mathrm{Embedding}\left(\mathrm{Fin}\left(r\right),V1\right)),\forall (B:\mathrm{Function}.\mathrm{Embedding}\left(\mathrm{Fin}\left(r\right),V2\right)),(\mathrm{SimpleGraph}.\mathrm{Connected}\left(G1\right))\Rightarrow ((\mathrm{SimpleGraph}.\mathrm{Connected}\left(G2\right))\Rightarrow ((r+1\le \mathrm{Fintype}.\mathrm{card}\left(V1\right))\Rightarrow ((r+1\le \mathrm{Fintype}.\mathrm{card}\left(V2\right))\Rightarrow ((\mathrm{SimpleGraph}.\mathrm{IsClique}\left(G1,\mathrm{Set}.\mathrm{range}\left(A\right)\right))\Rightarrow ((\mathrm{SimpleGraph}.\mathrm{IsClique}\left(G2,\mathrm{Set}.\mathrm{range}\left(B\right)\right))\Rightarrow ((\mathrm{strongDominationNumber}\left(G1\right):\mathbb{Z})+(\mathrm{strongDominationNumber}\left(G2\right):\mathbb{Z})-1-(\mathrm{sigmaXY}\left(G1,G2,A,B\right):\mathbb{Z})\le (\mathrm{strongDominationNumber}\left(\mathrm{glue}\left(G1,G2,A,B\right)\right):\mathbb{Z}))))))))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Domination/AlikhaniGhanbariHenningCliqueGluing.result (✓ std3). ∎

Resolves. Problems/alikhani-ghanbari-henning-clique-gluing-problem-1 (proved) by D5/S3/Combinatorics/Graph/Domination/AlikhaniGhanbariHenningCliqueGluing.result.

Source. Repository-derived.

Acknowledgement. Saeid Alikhani, Nima Ghanbari, Michael A. Henning (2026). Strong domination number of graphs from primary subgraphs. DOI: 10.2989/16073606.2025.2574046. URL: https://www.tandfonline.com/doi/full/10.2989/16073606.2025.2574046.

Commentary.

Restrict a minimum strong dominating set to each graph outside the common clique. In each factor, add a clique vertex of maximum degree; it strongly dominates the rest of the clique. If the original set meets the clique, also add the external neighbours of that clique. Every remaining exterior vertex keeps its original dominator and degree comparison. The two restrictions then have total size at most the original size plus one plus sigmaXY: a selected clique vertex pays for one of the two added clique vertices. If the original set misses the clique, connectedness and the proper clique range give at least one external neighbour, which pays for the extra vertex. Taking minimum sizes and rearranging in the integers yields the displayed bound. General sharpness of the source family and bounds using finer parameters are not asserted.

References

• Truth anchor: D5/S3/Combinatorics/Graph/Domination/AlikhaniGhanbariHenningCliqueGluing.IsStrongDominatingSet
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/AlikhaniGhanbariHenningCliqueGluing.X
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/AlikhaniGhanbariHenningCliqueGluing.claim
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/AlikhaniGhanbariHenningCliqueGluing.embedRight
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/AlikhaniGhanbariHenningCliqueGluing.glue
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/AlikhaniGhanbariHenningCliqueGluing.result
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/AlikhaniGhanbariHenningCliqueGluing.sigmaXY
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/AlikhaniGhanbariHenningCliqueGluing.strongDominationNumber