Add 10 WOWII open conjectures (batch 2)

FormalConjectures/WrittenOnTheWallII/GraphConjecture189.lean

@@ -0,0 +1,81 @@
+/-
+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 189
+
+**Verbatim statement (WOWII #189, status O):**
+> If G is a simple connected graph with n > 1 such that maximum { dist_even(v) : dist_even(v) is the number of vertices at even distance from v } ≤ 1 + σ(G), then G has a Hamiltonian path.
+
+**Source:** http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj189
+
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture189
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/-- `distEven G v` counts the number of vertices at even distance from `v` in `G`. -/
+noncomputable def distEven (G : SimpleGraph α) (v : α) : ℕ :=
+  (Finset.univ.filter (fun w => Even (G.dist v w))).card
+
+/-- The **2-domination number** of `G` (Fink–Jacobson 1985): the minimum size
+of a set `S` such that every vertex outside `S` has at least 2 neighbours in `S`.
+
+This is DeLaVina's `σ(G)`, used consistently across WOWII conjectures
+188, 189, 190, and 201 (all Hamiltonian-path implications). -/
+noncomputable def twoDominationNumber (G : SimpleGraph α) : ℕ :=
+  sInf { n | ∃ S : Finset α, S.card = n ∧
+    ∀ v ∉ S, 2 ≤ (S.filter (fun w => G.Adj v w)).card }
+
+/--
+WOWII [Conjecture 189](http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj189)
+(status O):
+
+For a simple connected graph `G`, if `max_v distEven(v) ≤ 1 + σ(G)`,
+then `G` has a Hamiltonian path.
+
+Here `distEven(v)` is the number of vertices at even distance from `v`, and
+`σ(G) = twoDominationNumber G` is the 2-domination number of `G`
+(Fink–Jacobson 1985).
+-/
+@[category research open, AMS 5]
+theorem conjecture189 (G : SimpleGraph α) (h : G.Connected)
+    (hσ : (Finset.univ.image (distEven G)).max' (by simp) ≤ 1 + twoDominationNumber G) :
+    ∃ a b : α, ∃ p : G.Walk a b, p.IsHamiltonian := by
+  sorry
+
+-- Sanity checks
+
+/-- The 2-domination number is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ twoDominationNumber G := Nat.zero_le _
+
+/-- `distEven G v` is positive for any vertex `v`. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) (v : Fin 3) : 0 < distEven G v := by
+  unfold distEven
+  apply Finset.card_pos.mpr
+  exact ⟨v, Finset.mem_filter.mpr ⟨Finset.mem_univ _, ⟨0, by simp [SimpleGraph.dist_self]⟩⟩⟩
+
+end WrittenOnTheWallII.GraphConjecture189

FormalConjectures/WrittenOnTheWallII/GraphConjecture199.lean

@@ -0,0 +1,75 @@
+/-
+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 199
+
+**Verbatim statement (WOWII #199, status O):**
+> If G is a simple connected graph with n > 1 such that tree(G) - 2 ≤ κ(G), then G has a Hamiltonian path.
+
+**Source:** http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj199
+
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture199
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/-- `largestInducedTreeSize G` is the number of vertices in a largest induced subtree of `G`. -/
+noncomputable def largestInducedTreeSize (G : SimpleGraph α) : ℕ :=
+  sSup { n | ∃ s : Finset α, s.card = n ∧ (G.induce (s : Set α)).IsTree }
+
+/-- The vertex connectivity `κ(G)`: the minimum number of vertices whose removal
+disconnects the graph (or `n - 1` when the graph is complete).
+Vertex connectivity is not yet in Mathlib; we define it here as the minimum size of
+a vertex separator, where removing `S` leaves the induced subgraph on `Sᶜ` disconnected.
+-- TODO: replace with a Mathlib definition when one becomes available. -/
+noncomputable def vertexConnectivity (G : SimpleGraph α) : ℕ :=
+  if Fintype.card α ≤ 1 then 0
+  else sInf { k | ∃ S : Finset α, S.card = k ∧
+    (¬(G.induce (↑Sᶜ : Set α)).Connected ∨ S.card = Fintype.card α - 1) }
+
+/--
+WOWII [Conjecture 199](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+
+For a simple connected graph `G`, if `tree(G) - 2 ≤ κ(G)`, then `G` has a Hamiltonian path.
+Here `tree(G)` is the number of vertices in a largest induced tree and
+`κ(G) = vertexConnectivity G` is the vertex connectivity of `G`.
+-/
+@[category research open, AMS 5]
+theorem conjecture199 (G : SimpleGraph α) (h : G.Connected)
+    (hκ : largestInducedTreeSize G - 2 ≤ vertexConnectivity 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 vertex connectivity is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ vertexConnectivity G := Nat.zero_le _
+
+end WrittenOnTheWallII.GraphConjecture199

FormalConjectures/WrittenOnTheWallII/GraphConjecture24.lean

@@ -0,0 +1,78 @@
+/-
+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 24
+
+**Verbatim statement (WOWII #24, status F):**
+> If G is a simple connected graph, then b(G) ≥ λ(G) + CEIL[minimum of dist_even(v)/3]
+
+**Source:** http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj24
+
+This conjecture is **disproved** on the WOWII page (status F). Following the
+upstream pattern established in #3823 for the closely related Conjecture 23,
+we record the disproof using `answer(False) ↔ ...`.
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture24
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/-- `distEven G v` counts the number of vertices at even distance from `v` in `G`.
+Distance 0 (the vertex itself) is even, so `distEven G v ≥ 1`. -/
+noncomputable def distEven (G : SimpleGraph α) (v : α) : ℕ :=
+  (Finset.univ.filter (fun w => Even (G.dist v w))).card
+
+/--
+WOWII [Conjecture 24](http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj24)
+(status F, disproved):
+
+For a simple connected graph `G`,
+`b(G) ≥ λ(G) + ⌈(min_v dist_even(v)) / 3⌉`
+where `b(G)` is the size of a largest induced bipartite subgraph,
+`λ(G) := max_v l(v)` is the maximum over all vertices of the independence
+number of the open neighbourhood of `v`, and `dist_even(v)` is the number of
+vertices at even distance from `v`.
+-/
+@[category research solved, AMS 5]
+theorem conjecture24 : answer(False) ↔
+    ∀ (G : SimpleGraph α) (_ : G.Connected),
+      let maxL := (Finset.univ.image (fun v => indepNeighborsCard G v)).max' (by simp)
+      let minDistEven := (Finset.univ.image (distEven G)).min' (by simp)
+      (maxL : ℝ) + ⌈(minDistEven : ℝ) / 3⌉ ≤ b G := by
+  sorry
+
+-- Sanity checks
+
+/-- `distEven G v` is always positive, since `v` itself is at distance 0 (even) from itself. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) (v : Fin 3) : 0 < distEven G v := by
+  unfold distEven
+  apply Finset.card_pos.mpr
+  exact ⟨v, Finset.mem_filter.mpr ⟨Finset.mem_univ _, ⟨0, by simp [SimpleGraph.dist_self]⟩⟩⟩
+
+/-- The invariant `b G` is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ b G := Nat.cast_nonneg _
+
+end WrittenOnTheWallII.GraphConjecture24

FormalConjectures/WrittenOnTheWallII/GraphConjecture25.lean

@@ -0,0 +1,75 @@
+/-
+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 25
+
+**Verbatim statement (WOWII #25, status F):**
+> If G is a simple connected graph, then b(G) ≥ 2 CEIL[(1 + minimum of dist_even(v))/3]
+
+**Source:** http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj25
+
+This conjecture is **disproved** on the WOWII page (status F; "same
+counterexample as in #24"). Following the upstream pattern established in
+#3823 for Conjecture 23, we record the disproof using `answer(False) ↔ ...`.
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture25
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/-- `distEven G v` counts the number of vertices at even distance from `v` in `G`.
+Distance 0 (the vertex itself) is even, so `distEven G v ≥ 1`. -/
+noncomputable def distEven (G : SimpleGraph α) (v : α) : ℕ :=
+  (Finset.univ.filter (fun w => Even (G.dist v w))).card
+
+/--
+WOWII [Conjecture 25](http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj25)
+(status F, disproved):
+
+For a simple connected graph `G`,
+`b(G) ≥ 2 · ⌈(1 + min_v dist_even(v)) / 3⌉`
+where `b(G)` is the size of a largest induced bipartite subgraph and
+`dist_even(v)` is the number of vertices at even distance from `v`.
+-/
+@[category research solved, AMS 5]
+theorem conjecture25 : answer(False) ↔
+    ∀ (G : SimpleGraph α) (_ : G.Connected),
+      let minDistEven := (Finset.univ.image (distEven G)).min' (by simp)
+      2 * ⌈(1 + (minDistEven : ℝ)) / 3⌉ ≤ b G := by
+  sorry
+
+-- Sanity checks
+
+/-- `distEven G v` is always at least 1, since `v` itself is at distance 0 (even) from itself. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 4)) (v : Fin 4) : 1 ≤ distEven G v := by
+  unfold distEven
+  apply Finset.card_pos.mpr
+  exact ⟨v, Finset.mem_filter.mpr ⟨Finset.mem_univ _, ⟨0, by simp [SimpleGraph.dist_self]⟩⟩⟩
+
+/-- The invariant `b G` is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ b G := Nat.cast_nonneg _
+
+end WrittenOnTheWallII.GraphConjecture25

FormalConjectures/WrittenOnTheWallII/GraphConjecture63.lean

@@ -0,0 +1,70 @@
+/-
+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 63
+
+**Verbatim statement (WOWII #63, status O):**
+> If G is a simple connected graph, then f(G) ≥ CEIL[(minimum of dist_even(v) + b(G) + 1)/3]
+
+**Source:** http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj63
+
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+namespace WrittenOnTheWallII.GraphConjecture63
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/-- `distEven G v` counts the number of vertices at even distance from `v` in `G`. -/
+noncomputable def distEven (G : SimpleGraph α) (v : α) : ℕ :=
+  (Finset.univ.filter (fun w => Even (G.dist v w))).card
+
+/--
+WOWII [Conjecture 63](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+
+For a simple connected graph `G`,
+`f(G) ≥ ⌈(min_v distEven(v) + b(G) + 1) / 3⌉`
+where `f(G) = largestInducedForestSize G` is the size of a largest induced forest,
+`b(G)` is the largest induced bipartite subgraph size, and
+`distEven(v)` is the number of vertices at even distance from `v`.
+-/
+@[category research open, AMS 5]
+theorem conjecture63 (G : SimpleGraph α) (h : G.Connected) :
+    let minDistEven := (Finset.univ.image (distEven G)).min' (by simp)
+    ⌈((minDistEven : ℝ) + b G + 1) / 3⌉ ≤ (G.largestInducedForestSize : ℝ) := by
+  sorry
+
+-- Sanity checks
+
+/-- The largest induced forest size is a natural number (nonneg). -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ G.largestInducedForestSize := Nat.zero_le _
+
+/-- `distEven` of any vertex is positive. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) (v : Fin 3) : 0 < distEven G v := by
+  unfold distEven
+  apply Finset.card_pos.mpr
+  exact ⟨v, Finset.mem_filter.mpr ⟨Finset.mem_univ _, ⟨0, by simp [SimpleGraph.dist_self]⟩⟩⟩
+
+end WrittenOnTheWallII.GraphConjecture63