Božović Conjecture 12: limited domination in Sierpiński graphs

Abstract

The k-limited domination number of the Sierpiński graph S(n,m) is proved exactly for n ≥ 1, 2 ≤ m, and 1 ≤ k ≤ m − 1.

Definition 1.1 (Sierpiński adjacency).

$$\forall r\in \mathrm{Nat},\forall m\in \mathrm{Nat},\forall u\in \mathrm{Fin}\left(r+1\right)\to \mathrm{Fin}\left(m\right),\forall v\in \mathrm{Fin}\left(r+1\right)\to \mathrm{Fin}\left(m\right),(\mathrm{sierAdj}\left(r,m,u,v\right))\iff (\exists h\in \mathrm{Fin}\left(r+1\right),(\forall t\in \mathrm{Fin}\left(r+1\right),(t<h)\Rightarrow (u\left(t\right)=v\left(t\right)))\wedge ((u\left(h\right)\ne v\left(h\right))\wedge (\forall t\in \mathrm{Fin}\left(r+1\right),(h<t)\Rightarrow ((u\left(t\right)=v\left(h\right))\wedge (v\left(t\right)=u\left(h\right))))))$$

Formalization. D5/S3/Combinatorics/Graph/SierpinskiLimitedDomination.sierAdj (✓ std3).

Citation. D. Božović (2026). On k-limited domination: complexity and Sierpiński graphs. DOI: 10.48550/arXiv.2610.01584. URL: https://arxiv.org/abs/2610.01584v1.

Commentary.

For words u and v, adjacency is witnessed by an index h: the coordinates before h agree, the h-coordinates differ, and every later coordinate of each word is the other’s h-coordinate. This is the adjacency rule of Section 2.

Definition 1.2 (Sierpiński graph).

$$\forall r\in \mathrm{Nat},\forall m\in \mathrm{Nat},\forall u\in \mathrm{Fin}\left(r+1\right)\to \mathrm{Fin}\left(m\right),\forall v\in \mathrm{Fin}\left(r+1\right)\to \mathrm{Fin}\left(m\right),(\mathrm{Adj}\left(\mathrm{sierGraph}\left(r,m\right),u,v\right))\iff (\mathrm{sierAdj}\left(r,m,u,v\right))$$

Formalization. D5/S3/Combinatorics/Graph/SierpinskiLimitedDomination.sierGraph (✓ std3).

Citation. D. Božović (2026). On k-limited domination: complexity and Sierpiński graphs. DOI: 10.48550/arXiv.2610.01584. URL: https://arxiv.org/abs/2610.01584v1.

Commentary.

sierGraph r m is the loopless undirected SimpleGraph on functions from Fin (r + 1) to Fin m whose adjacency relation is sierAdj r m.

Definition 1.3 (k-limited dominating set).

$$\forall r\in \mathrm{Nat},\forall m\in \mathrm{Nat},\forall k\in \mathrm{Nat},\forall D\in \mathrm{Finset}\left(\mathrm{Fin}\left(r+1\right)\to \mathrm{Fin}\left(m\right)\right),(\mathrm{isKLimited}\left(r,m,k,D\right))\iff ((\mathrm{IsDominating}\left(\mathrm{sierGraph}\left(r,m\right),(D:\mathrm{Set}\left(\mathrm{Fin}\left(r+1\right)\to \mathrm{Fin}\left(m\right)\right))\right))\wedge (\forall u\in \mathrm{Fin}\left(r+1\right)\to \mathrm{Fin}\left(m\right),(u\in D)\Rightarrow (\mathrm{card}\left(\mathrm{sdiff}\left(\mathrm{neighborFinset}\left(\mathrm{sierGraph}\left(r,m\right),u\right),D\right)\right)\le k)))$$

Formalization. D5/S3/Combinatorics/Graph/SierpinskiLimitedDomination.isKLimited (✓ std3).

Citation. D. Božović (2026). On k-limited domination: complexity and Sierpiński graphs. DOI: 10.48550/arXiv.2610.01584. URL: https://arxiv.org/abs/2610.01584v1.

Commentary.

A set is k-limited dominating when it is dominating and every selected vertex has at most k neighbors outside the set.

Definition 1.4 (Limited domination number).

$$\forall r\in \mathrm{Nat},\forall m\in \mathrm{Nat},\forall k\in \mathrm{Nat},\mathrm{gamma}\left(r,m,k\right)=\mathrm{sInf}\left(\{n:\mathrm{Nat}\mid \exists D\in \mathrm{Finset}\left(\mathrm{Fin}\left(r+1\right)\to \mathrm{Fin}\left(m\right)\right),(\mathrm{isKLimited}\left(r,m,k,D\right))\wedge (\mathrm{card}\left(D\right)=n)\}\right)$$

Formalization. D5/S3/Combinatorics/Graph/SierpinskiLimitedDomination.gamma (✓ std3).

Citation. D. Božović (2026). On k-limited domination: complexity and Sierpiński graphs. DOI: 10.48550/arXiv.2610.01584. URL: https://arxiv.org/abs/2610.01584v1.

Commentary.

gamma r m k is the infimum of the cardinalities of k-limited dominating subsets of the functions from Fin (r + 1) to Fin m.

Definition 1.5 (Conjecture 12).

$$(claim)\iff (\forall n\in \mathrm{Nat},\forall m\in \mathrm{Nat},\forall k\in \mathrm{Nat},((1\le n)\wedge ((2\le m)\wedge ((1\le k)\wedge (k\le m-1))))\Rightarrow (\mathrm{gamma}\left(n-1,m,k\right)=\left(m-k\right)\cdot m^{n-1}))$$

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

Citation. D. Božović (2026). On k-limited domination: complexity and Sierpiński graphs. DOI: 10.48550/arXiv.2610.01584. URL: https://arxiv.org/abs/2610.01584v1.

Commentary.

Section 6, Conjecture 12 (p. 9) states verbatim: “Let n, m, and k be integers such that n ≥ 1 and 1 ≤ k ≤ m − 1. Then γ_k^L(S(n, m)) = (m−k)·m^(n−1).” The formal encoding uses n,m,k : ℕ, the graph rank n−1, and gamma for γ_k^L.

Theorem 1.6 (Conjecture 12 proved).

$$claim$$

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

Resolves. Problems/bozovic-2026-sierpinski-limited-domination (proved) by D5/S3/Combinatorics/Graph/SierpinskiLimitedDomination.result.

Citation. D. Božović (2026). On k-limited domination: complexity and Sierpiński graphs. DOI: 10.48550/arXiv.2610.01584. URL: https://arxiv.org/abs/2610.01584v1.

Commentary.

The theorem result has type claim. Its proof gives a recursive coloring constant on linking edges and bijective on every base clique for the upper bound; the lower bound charges every empty base clique an additional k−1 vertices. The result also specializes the source’s Theorems 10 and 11 at k = 1 and m = 3.

References

• Truth anchor: D5/S3/Combinatorics/Graph/SierpinskiLimitedDomination.claim
• Truth anchor: D5/S3/Combinatorics/Graph/SierpinskiLimitedDomination.gamma
• Truth anchor: D5/S3/Combinatorics/Graph/SierpinskiLimitedDomination.isKLimited
• Truth anchor: D5/S3/Combinatorics/Graph/SierpinskiLimitedDomination.result
• Truth anchor: D5/S3/Combinatorics/Graph/SierpinskiLimitedDomination.sierAdj
• Truth anchor: D5/S3/Combinatorics/Graph/SierpinskiLimitedDomination.sierGraph
• Dependency: D5/S3/ConceptDynamics/GraphColoring/GraphCoverDomination