Add 16 WOWII open conjectures (batch 1)

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

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

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

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

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

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