GraphConjecture291.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

10 declarations, 1 contain sorry, 0 declared as axioms

Written on the Wall II - Conjecture 291

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

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.

Imports (1)

FormalConjecturesUtil

def WrittenOnTheWallII.GraphConjecture291.minTrianglesAtVertex The minimum number of triangles incident to any vertex, over all vertices of $G$ line 66 source
Source documentation
The minimum number of triangles incident to any vertex, over all vertices of $G$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, Nat
Proof uses: Finset.inf', Finset.univ, SimpleGraph.numTrianglesAtVertex
3 instances, coercions and auxiliary constants left out.
```
noncomputable def minTrianglesAtVertex (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=
…
```
def WrittenOnTheWallII.GraphConjecture291.freqMinTriangles The number of vertices achieving the minimum triangle count line 70 source
Source documentation
The number of vertices achieving the minimum triangle count.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, Nat
Proof uses: Finset.card, Finset.filter, Eq, SimpleGraph.numTrianglesAtVertex, WrittenOnTheWallII.GraphConjecture291.minTrianglesAtVertex, Finset.univ
1 instances, coercions and auxiliary constants left out.
```
noncomputable def freqMinTriangles (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=
…
```
def WrittenOnTheWallII.GraphConjecture291.descDegreeSequence The descending degree sequence of $G$, used as the starting point of the Havel-Hakimi reduction line 79 source
Source documentation
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]$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, List, Nat
Proof uses: Multiset.sort, Multiset.map, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Finset.val, Finset.univ, GE.ge
11 instances, coercions and auxiliary constants left out.
```
noncomputable def descDegreeSequence (G : SimpleGraph α) [DecidableRel G.Adj] : List ℕ :=
…
```
def WrittenOnTheWallII.GraphConjecture291.havelHakimiIterate The Havel-Hakimi sequence of iterates: s i is the result of applying havelHakimiStep $i$ times to the descending degree sequence of $G$ line 84 source
Source documentation
The Havel-Hakimi sequence of iterates: s i is the result of applying havelHakimiStep $i$ times to the descending degree sequence of $G$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, Nat, List
Proof uses: Nat.iterate, SimpleGraph.havelHakimiStep, WrittenOnTheWallII.GraphConjecture291.descDegreeSequence
```
noncomputable def havelHakimiIterate (G : SimpleGraph α) [DecidableRel G.Adj] (i : ℕ) :
    List ℕ :=
…
```
def WrittenOnTheWallII.GraphConjecture291.havelHakimiZeroStep 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 line 100 source
Source documentation
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).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, Nat
Proof uses: InfSet.sInf, Set.ofPred, Or, Membership.mem, List, WrittenOnTheWallII.GraphConjecture291.havelHakimiIterate, OfNat.ofNat, Eq, List.nil
3 instances, coercions and auxiliary constants left out.
```
noncomputable def havelHakimiZeroStep (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=
…
```
theorem WrittenOnTheWallII.GraphConjecture291.conjecture291 WOWII Conjecture 291 For a simple connected graph sorry line 123 source
Source documentation
WOWII 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 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.
L4DEL explanation
WOWII 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 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.
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Iff, False, Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, LT.lt, Nat, OfNat.ofNat, Fintype.card, LE.le, SimpleGraph.totalDominationNumber, HAdd.hAdd, WrittenOnTheWallII.GraphConjecture291.havelHakimiZeroStep, WrittenOnTheWallII.GraphConjecture291.freqMinTriangles
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
10 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem conjecture291 : answer(False) ↔
    ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
      (G : SimpleGraph α) [DecidableRel G.Adj] (_h : G.Connected) (_hn : 2 < Fintype.card α),
      G.totalDominationNumber ≤ havelHakimiZeroStep G + freqMinTriangles G := by
…
```
Mentions: WrittenOnTheWallII.GraphConjecture291.havelHakimiZeroStep, WrittenOnTheWallII.GraphConjecture291.freqMinTriangles
example WrittenOnTheWallII.GraphConjecture291.(example at line 133) line 133 source
Source documentation
In $K_3$, every vertex is in exactly $1$ triangle.
```
example : numTrianglesAtVertex (⊤ : SimpleGraph (Fin 3)) (0 : Fin 3) = 1 := by
…
```
example WrittenOnTheWallII.GraphConjecture291.(example at line 140) line 140 source
Source documentation
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
…
```
example WrittenOnTheWallII.GraphConjecture291.(example at line 147) line 147 source
Source documentation
In $K_3$, the minimum triangle count is $1$ (every vertex has $1$ triangle).
```
example : minTrianglesAtVertex (⊤ : SimpleGraph (Fin 3)) = 1 := by
…
```
Mentions: WrittenOnTheWallII.GraphConjecture291.minTrianglesAtVertex
example WrittenOnTheWallII.GraphConjecture291.(example at line 153) line 153 source
Source documentation
havelHakimiZeroStep is nonneg.
```
example (G : SimpleGraph (Fin 4)) [DecidableRel G.Adj] : 0 ≤ havelHakimiZeroStep G :=
…
```
Mentions: WrittenOnTheWallII.GraphConjecture291.havelHakimiZeroStep