The Luiz–Vieira generalized Blanuša closing conjecture is false

Abstract

The first generalized Blanuša snark has a [21]-Roman function of weight 108 and every independent [21]-Roman function has weight at least 110.

Definition 1.1 ([k]-Roman dominating functions).

$$\forall V\in Type,[\mathrm{Fintype}\left(V\right)]\forall G\in \mathrm{SimpleGraph}\left(V\right),[\mathrm{DecidableRel}\left(\mathrm{SimpleGraph}.\mathrm{Adj}\left(G\right)\right)]\forall k\in \mathbb{N},\forall f\in V\to \mathbb{N},(\mathrm{IsRomanDom}\left(G,k,f\right))\iff ((\forall v\in V,f\left(v\right)\le k+1)\wedge (\forall v\in V,(f\left(v\right)<k)\Rightarrow (k+\mathrm{Finset}.\mathrm{card}\left(\mathrm{Finset}.\mathrm{filter}\left((\mathrm{fun}(u:V)\mapsto 0<f\left(u\right)),\mathrm{SimpleGraph}.\mathrm{neighborFinset}\left(G,v\right)\right)\right)\le f\left(v\right)+\mathrm{Finset}.\mathrm{sum}\left(\mathrm{SimpleGraph}.\mathrm{neighborFinset}\left(G,v\right),f\right))))$$

Formalization. D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.IsRomanDom (✓ std3).

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

Section 1: “For any integer k ≥ 1, a [k]-Roman dominating function on G, also called [k]-RDF, is a function f : V(G) → {0, 1, . . . , k + 1} such that f(N[v]) ≥ k + |AN(v)| for every vertex v ∈ V(G) with f(v) < k.” The displayed natural-valued encoding gives the same finite label interval.

Definition 1.2 (Independent [k]-Roman dominating functions).

$$\forall V\in Type,[\mathrm{Fintype}\left(V\right)]\forall G\in \mathrm{SimpleGraph}\left(V\right),[\mathrm{DecidableRel}\left(\mathrm{SimpleGraph}.\mathrm{Adj}\left(G\right)\right)]\forall k\in \mathbb{N},\forall f\in V\to \mathbb{N},(\mathrm{IsIndepRomanDom}\left(G,k,f\right))\iff ((\mathrm{IsRomanDom}\left(G,k,f\right))\wedge (\forall u\in V,\forall w\in V,(0<f\left(u\right))\Rightarrow ((0<f\left(w\right))\Rightarrow (\neg \mathrm{SimpleGraph}.\mathrm{Adj}\left(G\right)\left(u,w\right)))))$$

Formalization. D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.IsIndepRomanDom (✓ std3).

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

Section 1: “A [k]-Roman dominating function f = (V0, V1, . . . , Vk+1) on a graph G is called an independent [k]-Roman dominating function, or [k]-IRDF for short, if the set of active vertices V1 ∪ V2 ∪ · · · ∪ Vk+1 is an independent set.” Positive labels encode the active set.

Definition 1.3 (Roman weight).

$$\forall V\in Type,[\mathrm{Fintype}\left(V\right)]\forall f\in V\to \mathbb{N},\mathrm{weight}\left(f\right)=\mathrm{Finset}.\mathrm{sum}\left(\mathrm{Finset}.\mathrm{univ},f\right)$$

Formalization. D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.weight (✓ std3).

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

Section 1: “The weight of a [k]-RDF f on G is defined as ω(f) = f(V(G)) = Σ_{v∈V(G)} f(v).”

Definition 1.4 ([k]-Roman domination number).

$$\forall V\in Type,[\mathrm{Fintype}\left(V\right)]\forall G\in \mathrm{SimpleGraph}\left(V\right),[\mathrm{DecidableRel}\left(\mathrm{SimpleGraph}.\mathrm{Adj}\left(G\right)\right)]\forall k\in \mathbb{N},\mathrm{gammaRoman}\left(G,k\right)=\mathrm{sInf}\left(\{w:\mathbb{N}\mid \exists f\in V\to \mathbb{N},(\mathrm{IsRomanDom}\left(G,k,f\right))\wedge (\mathrm{weight}\left(f\right)=w)\}\right)$$

Formalization. D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.gammaRoman (✓ std3).

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

Section 1: “The [k]-Roman domination number of G is the minimum weight that a [k]-RDF of G can have, and is denoted by γ[kR](G).”

Definition 1.5 (Independent [k]-Roman domination number).

$$\forall V\in Type,[\mathrm{Fintype}\left(V\right)]\forall G\in \mathrm{SimpleGraph}\left(V\right),[\mathrm{DecidableRel}\left(\mathrm{SimpleGraph}.\mathrm{Adj}\left(G\right)\right)]\forall k\in \mathbb{N},\mathrm{indepRoman}\left(G,k\right)=\mathrm{sInf}\left(\{w:\mathbb{N}\mid \exists f\in V\to \mathbb{N},(\mathrm{IsIndepRomanDom}\left(G,k,f\right))\wedge (\mathrm{weight}\left(f\right)=w)\}\right)$$

Formalization. D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.indepRoman (✓ std3).

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

Section 1: “The independent [k]-Roman domination number i[kR](G) is the minimum weight of an independent [k]-IRDF on G”.

Definition 1.6 (Blanuša vertex labels).

$$\begin{array}{r}\mathrm{Vert}.\mathrm{blk}:\mathrm{Fin}\left(10\right)\to \mathrm{Vert}\left(\right)\\ \mathrm{Vert}.\mathrm{lnk}:\mathbb{N}\to \left(\mathrm{Fin}\left(8\right)\to \mathrm{Vert}\left(\right)\right)\end{array}$$

Formalization. D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.Vert (✓ std3).

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

The inductive type has exactly the two displayed constructors. Figure 5 labels the ten vertices of B₀ᵗ by blk 0 through blk 9 and the eight vertices of each link Lⱼ by lnk j 0 through lnk j 7.

Definition 1.7 (Block border vertex a).

$$a\left(\right)=\mathrm{Vert}.\mathrm{blk}\left(0\right)$$

Formalization. D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.a (✓ std3).

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

Figure 5(a) names a = blk 0.

Definition 1.8 (Block border vertex b).

$$b\left(\right)=\mathrm{Vert}.\mathrm{blk}\left(6\right)$$

Formalization. D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.b (✓ std3).

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

Figure 5(a) names b = blk 6.

Definition 1.9 (Block border vertex c).

$$c\left(\right)=\mathrm{Vert}.\mathrm{blk}\left(3\right)$$

Formalization. D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.c (✓ std3).

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

Figure 5(a) names c = blk 3.

Definition 1.10 (Block border vertex d).

$$d\left(\right)=\mathrm{Vert}.\mathrm{blk}\left(9\right)$$

Formalization. D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.d (✓ std3).

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

Figure 5(a) names d = blk 9.

Definition 1.11 (Link border vertex x).

$$\forall j\in \mathbb{N},x\left(j\right)=\mathrm{Vert}.\mathrm{lnk}\left(j,0\right)$$

Formalization. D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.x (✓ std3).

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

Figure 5(c) names xⱼ = lnk j 0.

Definition 1.12 (Link border vertex w).

$$\forall j\in \mathbb{N},w\left(j\right)=\mathrm{Vert}.\mathrm{lnk}\left(j,2\right)$$

Formalization. D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.w (✓ std3).

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

Figure 5(c) names wⱼ = lnk j 2.

Definition 1.13 (Link border vertex y).

$$\forall j\in \mathbb{N},y\left(j\right)=\mathrm{Vert}.\mathrm{lnk}\left(j,5\right)$$

Formalization. D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.y (✓ std3).

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

Figure 5(c) names yⱼ = lnk j 5.

Definition 1.14 (Link border vertex z).

$$\forall j\in \mathbb{N},z\left(j\right)=\mathrm{Vert}.\mathrm{lnk}\left(j,7\right)$$

Formalization. D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.z (✓ std3).

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

Figure 5(c) names zⱼ = lnk j 7.

Definition 1.15 (Edges of B₀¹).

$$\mathrm{blockOneEdges}\left(\right)=\left\{Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(0\right),\mathrm{Vert}.\mathrm{blk}\left(1\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(1\right),\mathrm{Vert}.\mathrm{blk}\left(2\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(2\right),\mathrm{Vert}.\mathrm{blk}\left(3\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(3\right),\mathrm{Vert}.\mathrm{blk}\left(9\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(9\right),\mathrm{Vert}.\mathrm{blk}\left(8\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(8\right),\mathrm{Vert}.\mathrm{blk}\left(7\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(7\right),\mathrm{Vert}.\mathrm{blk}\left(6\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(6\right),\mathrm{Vert}.\mathrm{blk}\left(4\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(4\right),\mathrm{Vert}.\mathrm{blk}\left(0\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(1\right),\mathrm{Vert}.\mathrm{blk}\left(7\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(2\right),\mathrm{Vert}.\mathrm{blk}\left(5\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(5\right),\mathrm{Vert}.\mathrm{blk}\left(8\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(4\right),\mathrm{Vert}.\mathrm{blk}\left(5\right)\right)\right\}$$

Formalization. D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.blockOneEdges (✓ std3).

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

Figure 5(a) gives the thirteen unordered edges of B₀¹.

Definition 1.16 (Edges of B₀²).

$$\mathrm{blockTwoEdges}\left(\right)=\left\{Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(0\right),\mathrm{Vert}.\mathrm{blk}\left(1\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(1\right),\mathrm{Vert}.\mathrm{blk}\left(3\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(1\right),\mathrm{Vert}.\mathrm{blk}\left(2\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(2\right),\mathrm{Vert}.\mathrm{blk}\left(8\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(2\right),\mathrm{Vert}.\mathrm{blk}\left(5\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(0\right),\mathrm{Vert}.\mathrm{blk}\left(4\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(4\right),\mathrm{Vert}.\mathrm{blk}\left(6\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(4\right),\mathrm{Vert}.\mathrm{blk}\left(5\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(5\right),\mathrm{Vert}.\mathrm{blk}\left(7\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(3\right),\mathrm{Vert}.\mathrm{blk}\left(7\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(7\right),\mathrm{Vert}.\mathrm{blk}\left(9\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(6\right),\mathrm{Vert}.\mathrm{blk}\left(8\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{blk}\left(8\right),\mathrm{Vert}.\mathrm{blk}\left(9\right)\right)\right\}$$

Formalization. D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.blockTwoEdges (✓ std3).

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

Figure 5(b) gives the thirteen unordered edges of B₀².

Definition 1.17 (Edges of Lⱼ).

$$\forall j\in \mathbb{N},\mathrm{linkEdges}\left(j\right)=\left\{Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{lnk}\left(j,0\right),\mathrm{Vert}.\mathrm{lnk}\left(j,1\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{lnk}\left(j,1\right),\mathrm{Vert}.\mathrm{lnk}\left(j,2\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{lnk}\left(j,2\right),\mathrm{Vert}.\mathrm{lnk}\left(j,4\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{lnk}\left(j,4\right),\mathrm{Vert}.\mathrm{lnk}\left(j,7\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{lnk}\left(j,7\right),\mathrm{Vert}.\mathrm{lnk}\left(j,6\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{lnk}\left(j,6\right),\mathrm{Vert}.\mathrm{lnk}\left(j,5\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{lnk}\left(j,5\right),\mathrm{Vert}.\mathrm{lnk}\left(j,3\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{lnk}\left(j,3\right),\mathrm{Vert}.\mathrm{lnk}\left(j,0\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{lnk}\left(j,1\right),\mathrm{Vert}.\mathrm{lnk}\left(j,6\right)\right),Sym2.\mathrm{mk}\left(\mathrm{Vert}.\mathrm{lnk}\left(j,3\right),\mathrm{Vert}.\mathrm{lnk}\left(j,4\right)\right)\right\}$$

Formalization. D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.linkEdges (✓ std3).

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

Figure 5(c) gives the ten edges of each link block Lⱼ.

Definition 1.18 (Base block edge selector).

$$\forall t\in \mathbb{N},\mathrm{blockEdges}\left(t\right)=\mathrm{ite}\left(t=1,\mathrm{blockOneEdges}\left(\right),\mathrm{blockTwoEdges}\left(\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.blockEdges (✓ std3).

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

The base block is B₀¹ when t = 1 and B₀² otherwise.

Definition 1.19 (Vertices of Lⱼ).

$$\forall j\in \mathbb{N},\mathrm{linkVerts}\left(j\right)=\mathrm{Finset}.\mathrm{image}\left((\mathrm{fun}(r:\mathrm{Fin}\left(8\right))\mapsto \mathrm{Vert}.\mathrm{lnk}\left(j,r\right)),\mathrm{Finset}.\mathrm{univ}\right)$$

Formalization. D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.linkVerts (✓ std3).

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

Each Lⱼ has the eight vertices lnk j r for r ∈ Fin 8.

Definition 1.20 (Edges of the link graph).

$$\forall i\in \mathbb{N},\mathrm{linkGraphEdges}\left(i\right)=((\mathrm{linkEdges}\left(i-1\right))\cup (\mathrm{linkEdges}\left(i\right)))\cup (\left\{Sym2.\mathrm{mk}\left(w\left(i-1\right),y\left(i\right)\right),Sym2.\mathrm{mk}\left(z\left(i-1\right),x\left(i\right)\right)\right\})$$

Formalization. D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.linkGraphEdges (✓ std3).

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

Section 4, Figure 8: E(LGᵢ) = E(Lᵢ₋₁) ∪ E(Lᵢ) ∪ {wᵢ₋₁yᵢ, zᵢ₋₁xᵢ}.

Definition 1.21 (Vertices of Bᵢᵗ).

$$\begin{array}{r}\mathrm{verts}\left(0\right)=\mathrm{Finset}.\mathrm{image}\left(\mathrm{Vert}.\mathrm{blk},\mathrm{Finset}.\mathrm{univ}\right)\\ \mathrm{verts}\left(1\right)=(\mathrm{Finset}.\mathrm{image}\left(\mathrm{Vert}.\mathrm{blk},\mathrm{Finset}.\mathrm{univ}\right))\cup (\mathrm{linkVerts}\left(1\right))\\ \mathrm{verts}\left(2\right)=((\mathrm{Finset}.\mathrm{image}\left(\mathrm{Vert}.\mathrm{blk},\mathrm{Finset}.\mathrm{univ}\right))\cup (\mathrm{linkVerts}\left(1\right)))\cup (\mathrm{linkVerts}\left(2\right))\\ \forall i\in \mathbb{N},\mathrm{verts}\left(i+3\right)=(\mathrm{verts}\left(i+1\right))\cup ((\mathrm{linkVerts}\left(i+2\right))\cup (\mathrm{linkVerts}\left(i+3\right)))\end{array}$$

Formalization. D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.verts (✓ std3).

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

Section 4: V(Bᵢᵗ) is the base block together with the required link blocks, recursively adding two links at each step.

Definition 1.22 (Edges of Bᵢᵗ).

$$\forall t\in \mathbb{N},\begin{array}{r}\mathrm{edges}\left(t,0\right)=\mathrm{blockEdges}\left(t\right)\\ \mathrm{edges}\left(t,1\right)=\mathrm{ite}\left(t=1,((\mathrm{blockEdges}\left(t\right))\cup (\mathrm{linkEdges}\left(1\right)))\cup (\left\{Sym2.\mathrm{mk}\left(c\left(\right),y\left(1\right)\right),Sym2.\mathrm{mk}\left(d\left(\right),x\left(1\right)\right),Sym2.\mathrm{mk}\left(a\left(\right),z\left(1\right)\right),Sym2.\mathrm{mk}\left(b\left(\right),w\left(1\right)\right)\right\}),((\mathrm{blockEdges}\left(t\right))\cup (\mathrm{linkEdges}\left(1\right)))\cup (\left\{Sym2.\mathrm{mk}\left(b\left(\right),w\left(1\right)\right),Sym2.\mathrm{mk}\left(a\left(\right),z\left(1\right)\right),Sym2.\mathrm{mk}\left(c\left(\right),y\left(1\right)\right),Sym2.\mathrm{mk}\left(d\left(\right),x\left(1\right)\right)\right\})\right)\\ \mathrm{edges}\left(t,2\right)=\mathrm{ite}\left(t=1,(((\mathrm{blockEdges}\left(t\right))\cup (\mathrm{linkEdges}\left(1\right)))\cup (\mathrm{linkEdges}\left(2\right)))\cup (\left\{Sym2.\mathrm{mk}\left(c\left(\right),y\left(1\right)\right),Sym2.\mathrm{mk}\left(d\left(\right),x\left(1\right)\right),Sym2.\mathrm{mk}\left(w\left(1\right),y\left(2\right)\right),Sym2.\mathrm{mk}\left(z\left(1\right),x\left(2\right)\right),Sym2.\mathrm{mk}\left(a\left(\right),z\left(2\right)\right),Sym2.\mathrm{mk}\left(b\left(\right),w\left(2\right)\right)\right\}),(((\mathrm{blockEdges}\left(t\right))\cup (\mathrm{linkEdges}\left(1\right)))\cup (\mathrm{linkEdges}\left(2\right)))\cup (\left\{Sym2.\mathrm{mk}\left(b\left(\right),w\left(2\right)\right),Sym2.\mathrm{mk}\left(a\left(\right),z\left(2\right)\right),Sym2.\mathrm{mk}\left(c\left(\right),y\left(1\right)\right),Sym2.\mathrm{mk}\left(d\left(\right),x\left(1\right)\right),Sym2.\mathrm{mk}\left(z\left(1\right),x\left(2\right)\right),Sym2.\mathrm{mk}\left(w\left(1\right),y\left(2\right)\right)\right\})\right)\\ \forall i\in \mathbb{N},\mathrm{edges}\left(t,i+3\right)=(((\mathrm{edges}\left(t,i+1\right))\setminus (\left\{Sym2.\mathrm{mk}\left(a\left(\right),z\left(i+1\right)\right),Sym2.\mathrm{mk}\left(b\left(\right),w\left(i+1\right)\right)\right\}))\cup (\mathrm{linkGraphEdges}\left(i+3\right)))\cup (\left\{Sym2.\mathrm{mk}\left(w\left(i+1\right),y\left(i+2\right)\right),Sym2.\mathrm{mk}\left(z\left(i+1\right),x\left(i+2\right)\right),Sym2.\mathrm{mk}\left(a\left(\right),z\left(i+3\right)\right),Sym2.\mathrm{mk}\left(b\left(\right),w\left(i+3\right)\right)\right\})\end{array}$$

Formalization. D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.edges (✓ std3).

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

Section 4: “For each integer i, with i ≥ 3, the snark Bᵢᵗ is obtained recursively from the snark Bᵗᵢ₋₂ and the link graph LGᵢ” with the displayed edge deletion and insertion sets.

Definition 1.23 (Generalized Blanuša snark).

$$\forall t\in \mathbb{N},\forall i\in \mathbb{N},\mathrm{snark}\left(t,i\right)=\mathrm{SimpleGraph}.\mathrm{fromRel}\left((\mathrm{fun}(u:\mathrm{Subtype}\left((\mathrm{fun}(q:\mathrm{Vert}\left(\right))\mapsto q\in \mathrm{verts}\left(i\right))\right))\mapsto (\mathrm{fun}(v:\mathrm{Subtype}\left((\mathrm{fun}(q:\mathrm{Vert}\left(\right))\mapsto q\in \mathrm{verts}\left(i\right))\right))\mapsto Sym2.\mathrm{mk}\left(\mathrm{Subtype}.\mathrm{val}\left(u\right),\mathrm{Subtype}.\mathrm{val}\left(v\right)\right)\in \mathrm{edges}\left(t,i\right)))\right)$$

Formalization. D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.snark (✓ std3).

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

The graph Bᵢᵗ is the SimpleGraph.fromRel graph on the vertex subtype v ∈ verts i, with adjacency represented by Sym2.mk membership in edges t i.

Definition 1.24 (The closing conjecture).

$$(claim)\iff (\forall t\in \mathbb{N},\forall i\in \mathbb{N},\forall k\in \mathbb{N},((t=1)\vee (t=2))\Rightarrow ((1\le i)\Rightarrow ((2\le k)\Rightarrow (\mathrm{gammaRoman}\left(\mathrm{snark}\left(t,i\right),k\right)=\mathrm{indepRoman}\left(\mathrm{snark}\left(t,i\right),k\right)))))$$

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

Citation. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

Section 6: “another interesting line of research is finding other classes of graphs with ∆(G) ≤ 3 for which γ[kR](G) = i[kR](G) for k ≥ 2. In fact, we conjecture that this property holds for all generalized Blanuša snarks.” The parameters are encoded by t ∈ {1, 2}, i ≥ 1 and k ≥ 2.

Theorem 1.25 (A counterexample at B₁¹ and k = 21).

$$\neg \left(\forall t\in \mathbb{N},\forall i\in \mathbb{N},\forall k\in \mathbb{N},((t=1)\vee (t=2))\Rightarrow ((1\le i)\Rightarrow ((2\le k)\Rightarrow (\mathrm{gammaRoman}\left(\mathrm{snark}\left(t,i\right),k\right)=\mathrm{indepRoman}\left(\mathrm{snark}\left(t,i\right),k\right))))\right)$$

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

Resolves. Problems/luiz-vieira-2024-blanusa-independent-roman-closing-conjecture (refuted) by D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.result.

Source. Repository-derived.

Acknowledgement. A. G. Luiz and F. A. S. Vieira (2025). Independent [k]-Roman Domination on Graphs. DOI: 10.7151/dmgt.2580. URL: https://arxiv.org/abs/2406.11688v1.

Commentary.

For B₁¹, the constant label 6 is a [21]-RDF of weight 108. The independent witness assigns 22 exactly to Vert.blk 1, Vert.blk 4, Vert.blk 9, Vert.lnk 1 4 and Vert.lnk 1 6, and assigns 0 to every other vertex, giving weight 110. The support and private-neighbour bounds show that every independent [21]-RDF has weight at least 110. Thus γ[21R](B₁¹) ≤ 108 < 110 = i[21R](B₁¹), refuting the closing conjecture.

References

• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.IsIndepRomanDom
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.IsRomanDom
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.Vert
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.a
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.b
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.blockEdges
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.blockOneEdges
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.blockTwoEdges
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.c
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.claim
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.d
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.edges
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.gammaRoman
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.indepRoman
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.linkEdges
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.linkGraphEdges
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.linkVerts
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.result
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.snark
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.verts
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.w
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.weight
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.x
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.y
• Truth anchor: D5/S3/Combinatorics/Graph/Domination/LuizVieiraBlanusaIndependentRoman.z
• Dependency: D5/S3/Combinatorics/Graph/DirectSquareWeakFour/LowDegreeCount
• Dependency: D5/S3/Combinatorics/Graph/DominatingSetAverageBoundCounting
• Dependency: D5/S3/Combinatorics/Graph/DominatingSetAverageBoundNonstem
• Dependency: D5/S3/ConceptDynamics/GraphColoring/GraphCoverDomination