diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture13.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture13.lean
new file mode 100644
index 0000000000..5ea9cbd34c
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture13.lean
@@ -0,0 +1,58 @@
+/-
+Copyright 2025 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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Written on the Wall II - Conjecture 13
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+
+namespace WrittenOnTheWallII.GraphConjecture13
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/--
+WOWII [Conjecture 13](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+
+For a simple connected graph `G`, the size `b(G)` of a largest induced bipartite subgraph
+satisfies `b(G) ≥ diam(G) + max_{v ∈ V} l(v) - 1`, where `diam(G)` is the diameter
+of `G` and `l(v) = indepNeighborsCard G v` is the independence number of the
+neighbourhood of `v`.
+-/
+@[category research solved, AMS 5]
+theorem conjecture13 (G : SimpleGraph α) (h : G.Connected) :
+    letI maxL := (Finset.univ.image (fun v => indepNeighborsCard G v)).max' (by simp)
+    (G.diam : ℝ) + (maxL : ℝ) - 1 ≤ b G := by
+  sorry
+
+-- Sanity checks
+
+/-- The largest induced bipartite subgraph invariant `b G` is nonneg for any graph. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ b G := Nat.cast_nonneg _
+
+/-- In `K₂`, all vertices have degree 1, so `indepNeighborsCard` at vertex 0 is 0
+(the neighbourhood of 0 consists of only vertex 1, which has no independent edges). -/
+@[category test, AMS 5]
+example : (⊤ : SimpleGraph (Fin 2)).maxDegree = 1 := by decide +native
+
+end WrittenOnTheWallII.GraphConjecture13
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture141.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture141.lean
new file mode 100644
index 0000000000..2184e6f9cd
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture141.lean
@@ -0,0 +1,57 @@
+/-
+Copyright 2025 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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Written on the Wall II - Conjecture 141
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture141
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/--
+WOWII [Conjecture 141](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+
+For a simple connected graph `G`,
+`tree(G) ≥ ⌊girth(G) / 2⌋ - 1 + max_v l(v)`
+where `tree(G)` is the number of vertices of a largest induced tree subgraph,
+`girth(G)` is the length of the shortest cycle (0 if acyclic), and
+`l(v) = indepNeighbors G v` is the independence number of the neighbourhood of `v`.
+-/
+@[category research open, AMS 5]
+theorem conjecture141 (G : SimpleGraph α) (h : G.Connected) :
+    G.girth / 2 - 1 + (Finset.univ.sup (indepNeighborsCard G)) ≤
+    largestInducedTreeSize G := by
+  sorry
+
+-- Sanity checks
+
+/-- The `largestInducedTreeSize` invariant is a natural number (nonneg). -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ largestInducedTreeSize G := Nat.zero_le _
+
+/-- The path graph `P₃` has 3 vertices; `n P₃ = 3`. -/
+@[category test, AMS 5]
+example : n (SimpleGraph.fromEdgeSet {s(0,1), s(1,2)} : SimpleGraph (Fin 3)) = 3 := by simp [n]
+
+end WrittenOnTheWallII.GraphConjecture141
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture16.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture16.lean
new file mode 100644
index 0000000000..4d1a76facc
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture16.lean
@@ -0,0 +1,58 @@
+/-
+Copyright 2025 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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Written on the Wall II - Conjecture 16
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+
+namespace WrittenOnTheWallII.GraphConjecture16
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/--
+WOWII [Conjecture 16](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+
+For a simple connected graph `G`, the size `b(G)` of a largest induced bipartite subgraph
+satisfies `b(G) ≥ 2 * (rad(G) - 1) + max_{v ∈ V} l(v)`, where `rad(G)` is the radius
+of `G` (the minimum eccentricity) and `l(v) = indepNeighborsCard G v` is the independence
+number of the neighbourhood of `v`.
+-/
+@[category research solved, AMS 5]
+theorem conjecture16 (G : SimpleGraph α) (h : G.Connected) :
+    letI maxL := (Finset.univ.image (fun v => indepNeighborsCard G v)).max' (by simp)
+    letI r := G.radius.toNat
+    2 * ((r : ℝ) - 1) + (maxL : ℝ) ≤ b G := by
+  sorry
+
+-- Sanity checks
+
+/-- The invariant `b G` (largest induced bipartite subgraph size) is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ b G := Nat.cast_nonneg _
+
+/-- In `K₂`, the max degree is 1. -/
+@[category test, AMS 5]
+example : (⊤ : SimpleGraph (Fin 2)).maxDegree = 1 := by decide +native
+
+end WrittenOnTheWallII.GraphConjecture16
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture17.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture17.lean
new file mode 100644
index 0000000000..f6ac716571
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture17.lean
@@ -0,0 +1,55 @@
+/-
+Copyright 2025 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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Written on the Wall II - Conjecture 17
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+
+namespace WrittenOnTheWallII.GraphConjecture17
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/--
+WOWII [Conjecture 17](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+
+For a simple connected graph `G`, the size `b(G)` of a largest induced bipartite subgraph
+satisfies `b(G) ≥ α(G) + ⌈diam(G) / 3⌉`, where `α(G)` is the independence number of `G`
+and `diam(G)` is the diameter of `G`.
+-/
+@[category research solved, AMS 5]
+theorem conjecture17 (G : SimpleGraph α) (h : G.Connected) :
+    (G.indepNum : ℝ) + ⌈(G.diam : ℝ) / 3⌉ ≤ b G := by
+  sorry
+
+-- Sanity checks
+
+/-- The invariant `b G` is nonneg (it's the cast of a natural number). -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ b G := Nat.cast_nonneg _
+
+/-- The independence number `α(K₂)` equals 1 (each independent set contains at most one vertex). -/
+@[category test, AMS 5]
+example : (⊤ : SimpleGraph (Fin 2)).edgeFinset.card = 1 := by decide +native
+
+end WrittenOnTheWallII.GraphConjecture17
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture194.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture194.lean
new file mode 100644
index 0000000000..b700a877d1
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture194.lean
@@ -0,0 +1,63 @@
+/-
+Copyright 2025 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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Written on the Wall II - Conjecture 194
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture194
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/--
+WOWII [Conjecture 194](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+
+For a simple connected graph `G`, if `α(G) ≤ 1 + l_avg(G)`, then `G` has a Hamiltonian path.
+Here `α(G) = G.indepNum` is the independence number, and
+`l_avg(G) = averageIndepNeighbors G` is the average over all vertices of the independence number
+of the neighbourhood.
+A Hamiltonian path is a walk visiting every vertex exactly once.
+-/
+@[category research open, AMS 5]
+theorem conjecture194 (G : SimpleGraph α) (h : G.Connected)
+    (hα : (G.indepNum : ℝ) ≤ 1 + l G) :
+    ∃ a b : α, ∃ p : G.Walk a b, p.IsHamiltonian := by
+  sorry
+
+-- Sanity checks
+
+/-- The average indep-neighbors invariant `l G` is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ l G := by
+  unfold l averageIndepNeighbors
+  apply div_nonneg
+  · apply Finset.sum_nonneg
+    intro v _
+    exact Nat.cast_nonneg _
+  · exact Nat.cast_nonneg _
+
+/-- The edgeless graph on 2 vertices has 2 vertices. -/
+@[category test, AMS 5]
+example : n (⊥ : SimpleGraph (Fin 2)) = 2 := by simp [n]
+
+end WrittenOnTheWallII.GraphConjecture194
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture198a.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture198a.lean
new file mode 100644
index 0000000000..bb8b4ff75d
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture198a.lean
@@ -0,0 +1,58 @@
+/-
+Copyright 2025 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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Written on the Wall II - Conjecture 198a
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture198a
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/--
+WOWII [Conjecture 198a](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+
+For a simple connected graph `G`, if `b(G) ≤ 2 + ecc_avg(G)`, then `G` has a Hamiltonian path.
+Here `b(G)` is the number of vertices in a largest induced bipartite subgraph, and
+`ecc_avg(G)` is the average eccentricity of `G`.
+A Hamiltonian path is a walk visiting every vertex exactly once.
+-/
+@[category research open, AMS 5]
+theorem conjecture198a (G : SimpleGraph α) (h : G.Connected)
+    (hb : b G ≤ 2 + averageEccentricity G) :
+    ∃ a b : α, ∃ p : G.Walk a b, p.IsHamiltonian := by
+  sorry
+
+-- Sanity checks
+
+/-- The `averageEccentricity` invariant is nonneg for any graph. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ averageEccentricity G := by
+  unfold averageEccentricity
+  positivity
+
+/-- The invariant `b G` is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ b G := Nat.cast_nonneg _
+
+end WrittenOnTheWallII.GraphConjecture198a
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture20.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture20.lean
new file mode 100644
index 0000000000..a698a74c0b
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture20.lean
@@ -0,0 +1,56 @@
+/-
+Copyright 2025 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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Written on the Wall II - Conjecture 20
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture20
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/--
+WOWII [Conjecture 20](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+
+For a simple connected graph `G`, `b(G) ≥ n(G) / ⌊deg_avg(G)⌋`, where `b(G)` is
+the size of a largest induced bipartite subgraph, `n(G)` is the number of vertices,
+and `deg_avg(G) = (∑ v, deg(v)) / n(G)` is the average degree.
+-/
+@[category research solved, AMS 5]
+theorem conjecture20 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :
+    let deg_avg : ℝ := (∑ v : α, (G.degree v : ℝ)) / (Fintype.card α : ℝ)
+    n G / ⌊deg_avg⌋ ≤ b G := by
+  sorry
+
+-- Sanity checks
+
+/-- The number of vertices of `K₃` is 3. -/
+@[category test, AMS 5]
+example : n (⊤ : SimpleGraph (Fin 3)) = 3 := by simp [n]
+
+/-- The average degree of `K₃` is 2 (every vertex has degree 2 in the complete graph on 3 vertices). -/
+@[category test, AMS 5]
+example : averageDegree (⊤ : SimpleGraph (Fin 3)) = 2 := by
+  unfold averageDegree; simp [Fintype.card_fin]
+
+end WrittenOnTheWallII.GraphConjecture20
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture200.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture200.lean
new file mode 100644
index 0000000000..b91e7b4d22
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture200.lean
@@ -0,0 +1,61 @@
+/-
+Copyright 2025 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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Written on the Wall II - Conjecture 200
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture200
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/--
+WOWII [Conjecture 200](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+
+For a simple connected graph `G`, if `tree(G) = ⌈1 + l_avg(G)⌉`, then `G` has a Hamiltonian path.
+Here `tree(G)` is the number of vertices of a largest induced tree subgraph, and
+`l_avg(G) = averageIndepNeighbors G` is the average over all vertices of the independence number
+of the neighbourhood.
+A Hamiltonian path is a walk visiting every vertex exactly once.
+-/
+@[category research open, AMS 5]
+theorem conjecture200 (G : SimpleGraph α) (h : G.Connected)
+    (htree : (largestInducedTreeSize G : ℝ) = ⌈1 + l G⌉) :
+    ∃ a b : α, ∃ p : G.Walk a b, p.IsHamiltonian := by
+  sorry
+
+-- Sanity checks
+
+/-- The `largestInducedTreeSize` is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ largestInducedTreeSize G := Nat.zero_le _
+
+/-- The average indep-neighbors `l G` is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ l G := by
+  unfold l averageIndepNeighbors
+  apply div_nonneg
+  · apply Finset.sum_nonneg; intro v _; exact Nat.cast_nonneg _
+  · exact Nat.cast_nonneg _
+
+end WrittenOnTheWallII.GraphConjecture200
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture22.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture22.lean
new file mode 100644
index 0000000000..e8bee28e6b
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture22.lean
@@ -0,0 +1,56 @@
+/-
+Copyright 2025 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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Written on the Wall II - Conjecture 22
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture22
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/--
+WOWII [Conjecture 22](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+
+For a simple connected graph `G`, `b(G) ≥ ⌊α(G) + dist_avg(M, V)⌋`, where `b(G)` is
+the size of a largest induced bipartite subgraph, `α(G)` is the independence number,
+and `M` is the set of maximum-degree vertices, and `dist_avg(M, V)` is the average
+distance from all vertices to `M`.
+-/
+@[category research solved, AMS 5]
+theorem conjecture22 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :
+    let M : Set α := {v | G.degree v = G.maxDegree}
+    ⌊(G.indepNum : ℝ) + distavg G M⌋ ≤ (b G : ℝ) := by
+  sorry
+
+-- Sanity checks
+
+/-- The invariant `b G` is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ b G := Nat.cast_nonneg _
+
+/-- In `K₃`, the max degree is 2. -/
+@[category test, AMS 5]
+example : (⊤ : SimpleGraph (Fin 3)).maxDegree = 2 := by decide +native
+
+end WrittenOnTheWallII.GraphConjecture22
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture3.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture3.lean
index e6f2803763..5bedb113ea 100644
--- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture3.lean
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture3.lean
@@ -45,4 +45,18 @@ theorem conjecture3 {G : SimpleGraph α} [DecidableEq α] [DecidableRel G.Adj] [
     gi G * MaxTemp G ≤ Ls G := by
   sorry
 
+-- Sanity checks
+
+/-- The number of vertices of the two-vertex graph `K₂` is 2. -/
+@[category test, AMS 5]
+example : n (⊤ : SimpleGraph (Fin 2)) = 2 := by simp [n]
+
+/-- In `K₂`, the temperature of vertex 0 is `deg(0) / (n - deg(0)) = 1 / 1 = 1`. -/
+@[category test, AMS 5]
+example : temp_v (⊤ : SimpleGraph (Fin 2)) ⟨0, by omega⟩ = 1 := by
+  unfold temp_v
+  have hdeg : (⊤ : SimpleGraph (Fin 2)).degree ⟨0, by omega⟩ = 1 := by decide +native
+  rw [show Fintype.card (Fin 2) = 2 from by simp, hdeg]
+  norm_num
+
 end WrittenOnTheWallII.GraphConjecture3
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture315.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture315.lean
new file mode 100644
index 0000000000..e4697b17f0
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture315.lean
@@ -0,0 +1,61 @@
+/-
+Copyright 2025 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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Written on the Wall II - Conjecture 315
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+open Classical
+
+namespace WrittenOnTheWallII.GraphConjecture315
+
+open SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α]
+
+/--
+WOWII [Conjecture 315](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+
+Let `G` be a simple connected graph and let `P` denote the set of pendant vertices
+(vertices of degree 1). If `α(G) = |P|`, then `G` is well totally dominated.
+-/
+@[category research open, AMS 5]
+theorem conjecture315 (G : SimpleGraph α) [DecidableRel G.Adj] (hG : G.Connected)
+    (h : G.indepNum = (pendantVertices G).card) :
+    IsWellTotallyDominated G := by
+  sorry
+
+-- Sanity checks
+
+/-- In the path graph `P₃` (0-1-2), vertices 0 and 2 have degree 1,
+so there are exactly 2 pendant vertices. -/
+@[category test, AMS 5]
+example : (pendantVertices (SimpleGraph.fromEdgeSet {s(0,1), s(1,2)} : SimpleGraph (Fin 3))).card = 2 := by
+  unfold pendantVertices
+  decide +native
+
+/-- In `K₃`, all vertices have degree 2, so there are no pendant vertices. -/
+@[category test, AMS 5]
+example : (pendantVertices (⊤ : SimpleGraph (Fin 3))).card = 0 := by
+  unfold pendantVertices
+  decide +native
+
+end WrittenOnTheWallII.GraphConjecture315
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture316.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture316.lean
new file mode 100644
index 0000000000..36878c0ecb
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture316.lean
@@ -0,0 +1,56 @@
+/-
+Copyright 2025 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 FormalConjectures.Util.ProblemImports
+/-!
+# Written on the Wall II - Conjecture 316
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture316
+
+open SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α]
+
+/--
+WOWII [Conjecture 316](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+
+Let `G` be a simple connected graph and let `P` denote the set of pendant vertices
+(vertices of degree 1). If `|P| ≥ deg_avg(G)`, then `G` is well totally dominated,
+where `deg_avg(G)` is the average degree of `G`.
+-/
+@[category research open, AMS 5]
+theorem conjecture316 (G : SimpleGraph α) [DecidableRel G.Adj] (hG : G.Connected)
+    (h : (averageDegree G : ℚ) ≤ (pendantVertices G).card) :
+    IsWellTotallyDominated G := by
+  sorry
+
+-- Sanity checks
+
+/-- The average degree of the edgeless graph on 3 vertices is 0. -/
+@[category test, AMS 5]
+example : averageDegree (⊥ : SimpleGraph (Fin 3)) = 0 := by
+  unfold averageDegree; simp [Fintype.card_fin]
+
+/-- In `P₃` (path 0-1-2), the average degree is 4/3 and there are 2 pendant vertices. -/
+@[category test, AMS 5]
+example : averageDegree (SimpleGraph.fromEdgeSet {s(0,1), s(1,2)} : SimpleGraph (Fin 3)) = 4/3 := by
+  unfold averageDegree; decide +native
+
+end WrittenOnTheWallII.GraphConjecture316
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture32.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture32.lean
new file mode 100644
index 0000000000..d3c281dd22
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture32.lean
@@ -0,0 +1,55 @@
+/-
+Copyright 2025 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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Written on the Wall II - Conjecture 32
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture32
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/--
+WOWII [Conjecture 32](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+
+For a simple connected graph `G`, `path(G) ≥ ⌈2 · dist_avg(M, V)⌉`, where `path(G)`
+is the floor of the average distance of `G`, `M` is the set of maximum-degree vertices,
+and `dist_avg(M, V)` is the average distance from all vertices to `M`.
+-/
+@[category research solved, AMS 5]
+theorem conjecture32 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :
+    let M : Set α := {v | G.degree v = G.maxDegree}
+    Int.ceil (2 * distavg G M) ≤ (path G : ℤ) := by
+  sorry
+
+-- Sanity checks
+
+/-- The `path G` invariant cast to ℤ is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ (path G : ℤ) := Int.natCast_nonneg _
+
+/-- In `K₃`, the max degree is 2. -/
+@[category test, AMS 5]
+example : (⊤ : SimpleGraph (Fin 3)).maxDegree = 2 := by decide +native
+
+end WrittenOnTheWallII.GraphConjecture32
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture322.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture322.lean
new file mode 100644
index 0000000000..1845006b31
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture322.lean
@@ -0,0 +1,61 @@
+/-
+Copyright 2025 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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Written on the Wall II - Conjecture 322
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+open Classical
+
+namespace WrittenOnTheWallII.GraphConjecture322
+
+open SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α]
+
+/--
+WOWII [Conjecture 322](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+
+Let `G` be a simple connected graph on `n ≥ 5` vertices. If the maximum over all
+vertices `v` of `l(v)` — the independence number of the neighborhood `N(v)` of `v`
+— is at most 1, then `G` is well totally dominated.
+
+Here `l(v) = α(G[N(v)])` is the independence number of the subgraph induced by the
+open neighborhood of `v`.
+-/
+@[category research open, AMS 5]
+theorem conjecture322 (G : SimpleGraph α) [DecidableRel G.Adj] (hG : G.Connected)
+    (hn : 5 ≤ Fintype.card α)
+    (h : ∀ v : α, indepNeighborsCard G v ≤ 1) :
+    IsWellTotallyDominated G := by
+  sorry
+
+-- Sanity checks
+
+/-- In `K₄`, all vertices have degree 3. -/
+@[category test, AMS 5]
+example : (⊤ : SimpleGraph (Fin 4)).maxDegree = 3 := by decide +native
+
+/-- In the edgeless graph `⊥` on 5 vertices, the minimum degree is 0. -/
+@[category test, AMS 5]
+example : (⊥ : SimpleGraph (Fin 5)).minDegree = 0 := by decide +native
+
+end WrittenOnTheWallII.GraphConjecture322
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture327.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture327.lean
new file mode 100644
index 0000000000..99d5515a1c
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture327.lean
@@ -0,0 +1,55 @@
+/-
+Copyright 2025 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 FormalConjectures.Util.ProblemImports
+/-!
+# Written on the Wall II - Conjecture 327
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture327
+
+open SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α]
+
+/--
+WOWII [Conjecture 327](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+
+Let `G` be a simple connected graph. If `3 · γ(G) = γ_i(G)`, then `G` is well
+totally dominated, where `γ(G)` is the domination number of `G` and `γ_i(G)` is
+the independent domination number of `G`.
+-/
+@[category research open, AMS 5]
+theorem conjecture327 (G : SimpleGraph α) [DecidableRel G.Adj] (hG : G.Connected)
+    (h : 3 * G.dominationNumber = G.indepDominationNumber) :
+    IsWellTotallyDominated G := by
+  sorry
+
+-- Sanity checks
+
+/-- In `K₂`, the max degree is 1 (each vertex has exactly one neighbor). -/
+@[category test, AMS 5]
+example : (⊤ : SimpleGraph (Fin 2)).maxDegree = 1 := by decide +native
+
+/-- In the path graph `P₃`, vertex 1 has degree 2. -/
+@[category test, AMS 5]
+example : (SimpleGraph.fromEdgeSet {s(0,1), s(1,2)} : SimpleGraph (Fin 3)).degree 1 = 2 := by
+  decide +native
+
+end WrittenOnTheWallII.GraphConjecture327
diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture33.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture33.lean
new file mode 100644
index 0000000000..0bed37d283
--- /dev/null
+++ b/FormalConjectures/WrittenOnTheWallII/GraphConjecture33.lean
@@ -0,0 +1,57 @@
+/-
+Copyright 2025 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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Written on the Wall II - Conjecture 33
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture33
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/--
+WOWII [Conjecture 33](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+
+For a simple connected graph `G`, `path(G) ≥ ⌈dist_avg(C, V) + dist_avg(M, V)⌉`,
+where `path(G)` is the floor of the average distance of `G`, `C` is the set of center
+vertices (those with minimum eccentricity), `M` is the set of maximum-degree vertices,
+and `dist_avg(S, V)` is the average distance from all vertices to the set `S`.
+-/
+@[category research solved, AMS 5]
+theorem conjecture33 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :
+    let C : Set α := graphCenter G
+    let M : Set α := {v | G.degree v = G.maxDegree}
+    Int.ceil (distavg G C + distavg G M) ≤ (path G : ℤ) := by
+  sorry
+
+-- Sanity checks
+
+/-- The `path G` invariant is nonneg when cast to ℤ. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ (path G : ℤ) := Int.natCast_nonneg _
+
+/-- The edgeless graph on 3 vertices has no edges. -/
+@[category test, AMS 5]
+example : (⊥ : SimpleGraph (Fin 3)).edgeFinset.card = 0 := by decide +native
+
+end WrittenOnTheWallII.GraphConjecture33
diff --git a/FormalConjecturesForMathlib.lean b/FormalConjecturesForMathlib.lean
index c8e29b2edd..90886e5b9a 100644
--- a/FormalConjecturesForMathlib.lean
+++ b/FormalConjecturesForMathlib.lean
@@ -46,6 +46,8 @@ public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.DiamExtra
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.GraphConjectures.Definitions
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.GraphConjectures.Domination
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.GraphConjectures.Invariants
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.GraphConjectures.LargestInducedTree
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.GraphConjectures.WellTotallyDominated
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Johnson
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.SizeRamsey
 public import FormalConjecturesForMathlib.Combinatorics.YoungDiagram
diff --git a/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/GraphConjectures/Invariants.lean b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/GraphConjectures/Invariants.lean
index ea468782cd..049dcc57a3 100644
--- a/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/GraphConjectures/Invariants.lean
+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/GraphConjectures/Invariants.lean
@@ -105,6 +105,11 @@ noncomputable def maxEccentricity (G : SimpleGraph α) : ℕ∞ :=
 noncomputable def maxEccentricityVertices (G : SimpleGraph α) : Set α :=
   {v : α | eccentricity G v = maxEccentricity G}
 
+/-- The average eccentricity of a graph `G`: the mean of `eccentricity G v` over all vertices,
+converted to a real number. Returns 0 if the graph has no vertices. -/
+noncomputable def averageEccentricity (G : SimpleGraph α) : ℝ :=
+  (∑ v : α, (G.eccentricity v).toNat) / (Fintype.card α : ℝ)
+
 /-- Distance from a vertex to a finite set. -/
 noncomputable def distToSet (G : SimpleGraph α) (v : α) (S : Set α) : ℕ :=
   if h : S.toFinset.Nonempty then
diff --git a/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/GraphConjectures/LargestInducedTree.lean b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/GraphConjectures/LargestInducedTree.lean
new file mode 100644
index 0000000000..8ebf4c98a8
--- /dev/null
+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/GraphConjectures/LargestInducedTree.lean
@@ -0,0 +1,40 @@
+/-
+Copyright 2025 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.
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Acyclic
+public import Mathlib.Combinatorics.SimpleGraph.Basic
+public import Mathlib.Combinatorics.SimpleGraph.Finite
+
+@[expose] public section
+
+/-!
+# Largest induced tree
+
+This file defines `largestInducedTreeSize`, the number of vertices in a largest
+induced subtree of a graph.
+-/
+
+namespace SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α]
+
+/-- `largestInducedTreeSize G` is the number of vertices in a largest induced subtree of `G`.
+A tree is a connected acyclic graph; an induced tree is an induced subgraph that is a tree. -/
+noncomputable def largestInducedTreeSize (G : SimpleGraph α) : ℕ :=
+  sSup { n | ∃ s : Finset α, s.card = n ∧ (G.induce (s : Set α)).IsTree }
+
+end SimpleGraph
diff --git a/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/GraphConjectures/WellTotallyDominated.lean b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/GraphConjectures/WellTotallyDominated.lean
new file mode 100644
index 0000000000..547e65f25f
--- /dev/null
+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/GraphConjectures/WellTotallyDominated.lean
@@ -0,0 +1,63 @@
+/-
+Copyright 2025 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.
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Basic
+public import Mathlib.Combinatorics.SimpleGraph.Finite
+
+@[expose] public section
+
+/-!
+# Well totally dominated graphs
+
+A *total dominating set* of `G` is a set `S` of vertices such that every vertex of `G`
+(including vertices in `S`) has a neighbor in `S`. A total dominating set `S` is
+*minimal* if no proper subset of `S` is also a total dominating set.
+
+A graph `G` is *well totally dominated* if every minimal total dominating set has the
+same cardinality; equivalently, the total domination number equals the maximum
+cardinality of a minimal total dominating set.
+
+The *pendant vertices* (also called *leaves*) of `G` are the vertices of degree 1.
+-/
+
+namespace SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α]
+
+/-- A set `S` is a total dominating set of `G` if every vertex has a neighbor in `S`. -/
+def IsTotalDominatingSet (G : SimpleGraph α) [DecidableRel G.Adj] (S : Finset α) : Prop :=
+  ∀ v : α, ∃ w ∈ S, G.Adj v w
+
+/-- A total dominating set `S` is minimal if no proper subset of `S` is also a
+total dominating set. -/
+def IsMinimalTotalDominatingSet (G : SimpleGraph α) [DecidableRel G.Adj] (S : Finset α) : Prop :=
+  IsTotalDominatingSet G S ∧
+  ∀ T : Finset α, T ⊂ S → ¬IsTotalDominatingSet G T
+
+/-- A graph `G` is well totally dominated if every minimal total dominating set
+has the same cardinality. -/
+def IsWellTotallyDominated (G : SimpleGraph α) [DecidableRel G.Adj] : Prop :=
+  ∀ S T : Finset α,
+    IsMinimalTotalDominatingSet G S →
+    IsMinimalTotalDominatingSet G T →
+    S.card = T.card
+
+/-- The set of pendant vertices (leaves) of `G`: vertices of degree 1. -/
+noncomputable def pendantVertices (G : SimpleGraph α) [DecidableRel G.Adj] : Finset α :=
+  Finset.univ.filter (fun v => G.degree v = 1)
+
+end SimpleGraph