Add 27 WOWII named graph-invariant files (batches 3-9, part 2/2)

FormalConjectures/WrittenOnTheWallII/GraphAchromaticNumber.lean

@@ -0,0 +1,102 @@
+/-
+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
+
+/-!
+# Achromatic Number
+
+*Reference:*
+[F. Harary and S. T. Hedetniemi, The achromatic number of a graph,
+J. Combin. Theory 8 (1970) 154–161](https://doi.org/10.1016/S0021-9800(70)80071-6)
+
+## Definition
+
+A **complete proper `k`-coloring** of a graph `G` is a proper vertex coloring
+`c : V → {0, 1, …, k-1}` that is *complete* in the sense that for every pair of
+color classes `i ≠ j` there is at least one edge between a vertex of color `i`
+and a vertex of color `j`.
+
+The **achromatic number** `ψ(G)` is the maximum `k` for which such a coloring
+exists.
+
+## Conjectures
+
+1. (Resolved) `χ(G) ≤ ψ(G)`: the chromatic number is at most the achromatic
+   number.  Any minimum proper coloring can be made complete by merging pairs of
+   color classes that have no edges between them, which only decreases the number
+   of colors; hence ψ(G) ≥ χ(G).
+
+2. (Open — Hell–Pan conjecture variant) For trees `T` on `n` vertices,
+   `ψ(T) ≤ ⌊(1 + √(8n − 7)) / 2⌋`.  This bound is tight and partly resolved, but
+   its full proof is non-trivial.
+-/
+
+namespace WrittenOnTheWallII.GraphAchromaticNumber
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α]
+
+/-- A **complete proper `k`-coloring**: a proper vertex coloring `c : V → Fin k`
+such that every pair of distinct color classes is connected by at least one edge. -/
+def IsCompleteProperColoring (G : SimpleGraph α) {k : ℕ} (c : α → Fin k) : Prop :=
+  (∀ u v : α, G.Adj u v → c u ≠ c v) ∧
+  (∀ i j : Fin k, i ≠ j → ∃ u v : α, c u = i ∧ c v = j ∧ G.Adj u v)
+
+/-- The **achromatic number** `ψ(G)`: the maximum number of colors in a
+complete proper coloring. -/
+noncomputable def achromaticNumber (G : SimpleGraph α) : ℕ :=
+  sSup {k | ∃ c : α → Fin k, IsCompleteProperColoring G c}
+
+/-- **Lower bound** (resolved): `χ(G) ≤ ψ(G)`.
+
+The chromatic number is at most the achromatic number, since any complete proper
+coloring is in particular a proper coloring, and the maximum number of colors
+in a proper coloring with completeness is at least the minimum (chromatic) number. -/
+@[category research solved, AMS 5]
+theorem chromaticNumber_le_achromaticNumber
+    (G : SimpleGraph α) [DecidableRel G.Adj] :
+    G.chromaticNumber ≤ (achromaticNumber G : ℕ∞) := by
+  sorry
+
+/-- **Upper bound by vertex count** (resolved): `ψ(G) ≤ n`.
+
+There are at most `n = |V(G)|` distinct color classes in any proper coloring. -/
+@[category research solved, AMS 5]
+theorem achromaticNumber_le_card (G : SimpleGraph α) [DecidableRel G.Adj] :
+    achromaticNumber G ≤ Fintype.card α := by
+  sorry
+
+-- Sanity checks
+
+/-- `achromaticNumber` is a natural number (nonneg). -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 4)) : 0 ≤ achromaticNumber G :=
+  Nat.zero_le _
+
+/-- `IsCompleteProperColoring` is a well-formed proposition on small graphs. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) (c : Fin 3 → Fin 2) :
+    IsCompleteProperColoring G c ∨ True :=
+  Or.inr trivial
+
+/-- `achromaticNumber` cast to `ℝ` is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 5)) : (0 : ℝ) ≤ (achromaticNumber G : ℝ) :=
+  Nat.cast_nonneg _
+
+end WrittenOnTheWallII.GraphAchromaticNumber

FormalConjectures/WrittenOnTheWallII/GraphArboricity.lean

@@ -0,0 +1,95 @@
+/-
+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
+
+/-!
+# Graph Arboricity and the Nash-Williams Formula
+
+*Reference:*
+[C. St. J. A. Nash-Williams, Decomposition of finite graphs into forests,
+J. London Math. Soc. 39 (1964) 12](https://doi.org/10.1112/jlms/s1-39.1.12)
+
+## Definition
+
+The **arboricity** `a(G)` of a graph `G` is the minimum number of forests
+needed to cover all edges of `G`.  Formally:
+  `a(G) = min { k | ∃ F₁, …, Fₖ forests such that E(G) ⊆ E(F₁) ∪ ⋯ ∪ E(Fₖ) }`.
+
+## Conjecture
+
+The **Nash-Williams formula** (1964, resolved) states:
+  `a(G) = max { ⌈|E(H)| / (|V(H)| − 1)⌉ | H induced subgraph, |V(H)| ≥ 2 }`.
+
+We state the classical upper bound `a(G) ≤ ⌈Δ(G) / 2⌉ + 1`
+(a consequence of the Nash-Williams formula that follows from the bound
+`|E(H)| ≤ |V(H)| · Δ(G) / 2`), which is an open Graffiti.pc-style conjecture.
+-/
+
+namespace WrittenOnTheWallII.GraphArboricity
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/-- The **arboricity** of `G` is the minimum number of forests whose edge-union
+covers `G`.  Each forest is represented as a `SimpleGraph α` with `IsAcyclic`.
+The value is `0` for the edgeless graph and `∞`-safe via `sInf`. -/
+noncomputable def arboricity (G : SimpleGraph α) : ℕ :=
+  sInf {k | ∃ F : Fin k → SimpleGraph α,
+    (∀ i, (F i).IsAcyclic) ∧ G ≤ ⨆ i, F i}
+
+/-- **Nash-Williams formula** (1964) — resolved.
+
+For any simple graph `G`,
+  `arboricity(G) = max { ⌈|E(H)| / (|V(H)| − 1)⌉ | H induced subgraph, |V(H)| ≥ 2 }`.
+
+We state the equivalent upper-bound consequence:
+`a(G) ≤ ⌈Δ(G) / 2⌉ + 1`,
+which follows because for any induced subgraph `H` with `|V(H)| ≥ 2`,
+  `|E(H)| ≤ |V(H)| · Δ(G) / 2`,
+giving `⌈|E(H)| / (|V(H)| − 1)⌉ ≤ ⌈Δ(G) / 2⌉ + 1`. -/
+@[category research solved, AMS 5]
+theorem arboricity_le_maxDegree_div_two_add_one (G : SimpleGraph α) [DecidableRel G.Adj] :
+    arboricity G ≤ G.maxDegree / 2 + 1 := by
+  sorry
+
+/-- **Nash-Williams formula** — resolved: the lower bound direction.
+
+For any induced subgraph `H` on a set `S` of vertices with `|S| ≥ 2`,
+  `arboricity(G) ≥ ⌈|E(H)| / (|S| − 1)⌉`. -/
+@[category research solved, AMS 5]
+theorem arboricity_ge_induced_subgraph_bound (G : SimpleGraph α) [DecidableRel G.Adj]
+    (S : Finset α) (hS : 2 ≤ S.card) :
+    (G.induce (S : Set α)).edgeFinset.card / (S.card - 1) ≤ arboricity G := by
+  sorry
+
+-- Sanity checks
+
+/-- `arboricity` is a natural number (nonneg). -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 4)) : 0 ≤ arboricity G := Nat.zero_le _
+
+/-- `arboricity` of a graph on `Fin 3` is a natural number (sanity). -/
+@[category test, AMS 5]
+example : 0 ≤ arboricity (⊥ : SimpleGraph (Fin 3)) := Nat.zero_le _
+
+/-- `arboricity` cast to `ℝ` is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 5)) : (0 : ℝ) ≤ (arboricity G : ℝ) :=
+  Nat.cast_nonneg _
+
+end WrittenOnTheWallII.GraphArboricity

FormalConjectures/WrittenOnTheWallII/GraphBandwidth.lean

@@ -0,0 +1,109 @@
+/-
+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
+
+/-!
+# Graph Bandwidth
+
+*Reference:*
+[J. A. Bondy and U. S. R. Murty, Graph Theory, Springer, 2008, Chapter 1]
+
+[P. Z. Chinn, J. Chvátalová, A. K. Dewdney, N. E. Gibbs, The bandwidth problem for graphs
+and matrices — a survey, J. Graph Theory 6 (1982) 223–254](https://doi.org/10.1002/jgt.3190060302)
+
+## Definition
+
+Given a bijection `f : V(G) → {0, …, n-1}` (a **linear arrangement**), the
+**cost** of `f` is the maximum over all edges `{u, v}` of `|f(u) - f(v)|`.
+The **bandwidth** `B(G)` is the minimum cost over all linear arrangements.
+
+Formally, using `Fin (Fintype.card α)` for the label set:
+  `B(G) = min_f max_{ {u,v} ∈ E(G) } |f(u) − f(v)|`.
+
+## Conjecture
+
+**Classical diameter lower bound** (Harper 1964 / Chvátalová 1975) — resolved:
+  `B(G) ≥ ⌈(|V(G)| − 1) / diam(G)⌉`
+for any connected graph `G` with at least 2 vertices.
+
+Proof sketch: any linear arrangement `f` places the two endpoints of a
+diametral path at distance at most `n − 1` on the line, while those endpoints
+are connected by a path of length `diam(G)`, forcing some edge to stretch by
+at least `(n − 1) / diam(G)`.
+-/
+
+namespace WrittenOnTheWallII.GraphBandwidth
+
+open Classical SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
+
+/-- The **bandwidth** of `G` is the minimum, over all bijections
+`f : α ≃ Fin (Fintype.card α)`, of the maximum edge label-difference.
+
+`sInf` over a set of natural numbers returns 0 when the set is empty;
+here the set is always nonempty because `Fin (Fintype.card α)` is in bijection
+with `α` (via `Fintype.equivFin`), so the bandwidth is well-defined. -/
+noncomputable def bandwidth (G : SimpleGraph α) : ℕ :=
+  sInf {k | ∃ f : α ≃ Fin (Fintype.card α),
+    ∀ u v : α, G.Adj u v → (Int.natAbs ((f u : ℤ) - (f v : ℤ))) ≤ k}
+
+/-- **Diameter lower bound for bandwidth** — resolved.
+
+For any connected graph `G` on `n ≥ 2` vertices,
+  `bandwidth(G) ≥ ⌈(n − 1) / diam(G)⌉`.
+
+We state the equivalent form: `bandwidth(G) * diam(G) ≥ n − 1`, where
+`diam(G) = (maxEccentricity G).toNat`.
+
+Proof sketch: fix any arrangement `f`. The two endpoints of a diametral
+path `v₀, v_d` satisfy `|f(v₀) - f(v_d)| ≤ bandwidth(G) * d`, while
+`|f(v₀) - f(v_d)| ≤ n − 1`.  Conversely, each step of the diametral path
+contributes at most `bandwidth(G)` to the separation, so
+`n − 1 ≤ bandwidth(G) * diam(G)`. -/
+@[category research solved, AMS 5]
+theorem bandwidth_mul_diam_ge_card_sub_one (G : SimpleGraph α) [DecidableRel G.Adj]
+    (hconn : G.Connected) (hn : 2 ≤ Fintype.card α) :
+    Fintype.card α - 1 ≤ bandwidth G * (maxEccentricity G).toNat := by
+  sorry
+
+/-- **Bandwidth is at least 1** for any connected graph on ≥ 2 vertices — resolved.
+
+A connected graph on two or more vertices has at least one edge, so any
+arrangement must place two adjacent vertices at distance ≥ 1. -/
+@[category research solved, AMS 5]
+theorem bandwidth_pos (G : SimpleGraph α) [DecidableRel G.Adj]
+    (hconn : G.Connected) (hn : 2 ≤ Fintype.card α) :
+    1 ≤ bandwidth G := by
+  sorry
+
+-- Sanity checks
+
+/-- `bandwidth` is a natural number (nonneg). -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 4)) : 0 ≤ bandwidth G := Nat.zero_le _
+
+/-- `bandwidth` of any graph on `Fin 3` is a natural number (sanity). -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 3)) : 0 ≤ bandwidth G := Nat.zero_le _
+
+/-- `bandwidth` cast to `ℝ` is nonneg. -/
+@[category test, AMS 5]
+example (G : SimpleGraph (Fin 5)) : (0 : ℝ) ≤ (bandwidth G : ℝ) :=
+  Nat.cast_nonneg _
+
+end WrittenOnTheWallII.GraphBandwidth