diff --git a/FormalConjectures/WrittenOnTheWallII/GraphAchromaticNumber.lean b/FormalConjectures/WrittenOnTheWallII/GraphAchromaticNumber.lean new file mode 100644 index 0000000000..1c65e9c703 --- /dev/null +++ b/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 diff --git a/FormalConjectures/WrittenOnTheWallII/GraphArboricity.lean b/FormalConjectures/WrittenOnTheWallII/GraphArboricity.lean new file mode 100644 index 0000000000..a18868f018 --- /dev/null +++ b/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 diff --git a/FormalConjectures/WrittenOnTheWallII/GraphBandwidth.lean b/FormalConjectures/WrittenOnTheWallII/GraphBandwidth.lean new file mode 100644 index 0000000000..ef875ed099 --- /dev/null +++ b/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 diff --git a/FormalConjectures/WrittenOnTheWallII/GraphBoxicity.lean b/FormalConjectures/WrittenOnTheWallII/GraphBoxicity.lean new file mode 100644 index 0000000000..1fc9094518 --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphBoxicity.lean @@ -0,0 +1,129 @@ +/- +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 Boxicity + +*Reference:* +[F. S. Roberts, On the boxicity and cubicity of a graph, in Recent Progress in Combinatorics +(W. T. Tutte, ed.), Academic Press, 1969, pp. 301–310] + +[A. Adiga, L. S. Chandran, N. Sivadasan, Lower bounds for boxicity, +Combinatorica 34 (2014) 631–655](https://doi.org/10.1007/s00439-013-1365-z) + +[L. S. Chandran, M. C. Francis, N. Sivadasan, Boxicity and treewidth, +J. Combin. Theory Ser. B 97 (2007) 733–744](https://doi.org/10.1016/j.jctb.2006.12.004) + +## Definition + +The **boxicity** `box(G)` of a graph `G` is the minimum integer `d` such that +`G` is the intersection graph of a collection of axis-aligned boxes in `ℝᵈ` +(i.e., products of closed intervals). Equivalently, `box(G)` is the minimum +number of interval graphs whose intersection (as edge sets) equals `G`. + +A graph is an **interval graph** if it is the intersection graph of intervals +on the real line. The boxicity is the minimum `d` such that `G` is the +intersection of `d` interval graphs on the same vertex set. + +-- TODO: replace the `Classical.choice` placeholder with a proper definition +-- once Mathlib has formalised interval graph representations and intersection +-- graph constructions sufficiently for `sInf`-style minimisation. + +## Conjecture + +**Chandran–Francis–Sivadasan (2007)** — resolved: + `box(G) ≤ tw(G) + 2` +where `tw(G)` is the treewidth of `G`. + +This is an established upper bound; the proof uses tree decompositions to +construct an explicit box representation. + +An open related conjecture is whether the bound can be improved to +`box(G) ≤ tw(G) + 1` in general. +-/ + +namespace WrittenOnTheWallII.GraphBoxicity + +open Classical SimpleGraph + +variable {α : Type*} [Fintype α] [DecidableEq α] + +/-- The **boxicity** of `G`: the minimum dimension `d` such that `G` is the +intersection of `d` interval graphs on the vertex set `α`. + +Equivalently, `box(G)` is the minimum `d` for which there exist interval +graphs `I₁, …, I_d` on `α` with `G = I₁ ⊓ ⋯ ⊓ I_d` (as `SimpleGraph α`). + +-- TODO: this is a placeholder. The proper definition requires: +-- (1) a notion of interval graphs on a `Fintype`, +-- (2) a proof that the empty graph has boxicity 0 and complete graphs have +-- boxicity 0 (they are trivially intersection graphs), and +-- (3) `sInf`-style minimisation over `d`. -/ +noncomputable def boxicity (_ : SimpleGraph α) : ℕ := + Classical.choice (⟨0⟩ : Nonempty ℕ) + +/-- The **treewidth** of `G`: the minimum width over all tree decompositions of `G`. + +-- TODO: this is a placeholder. Treewidth is not yet in Mathlib 4.27; +-- the proper definition uses tree decompositions (Finset-valued bags indexed +-- by a tree satisfying the standard bag-union and bag-connectivity conditions). -/ +noncomputable def treewidth (_ : SimpleGraph α) : ℕ := + Classical.choice (⟨0⟩ : Nonempty ℕ) + +/-- **Treewidth upper bound for boxicity** (Chandran–Francis–Sivadasan 2007) — resolved. + +For any simple graph `G`, + `box(G) ≤ tw(G) + 2` +where `tw(G)` is the treewidth of `G`. + +Proof sketch: given a tree decomposition of width `tw(G)`, one constructs +`tw(G) + 2` interval graphs whose intersection equals `G` by processing +the bags of the decomposition. -/ +@[category research solved, AMS 5] +theorem boxicity_le_treewidth_add_two (G : SimpleGraph α) [DecidableRel G.Adj] : + boxicity G ≤ treewidth G + 2 := by + sorry + +/-- **Boxicity and maximum degree** (Roberts 1969 / Scheinerman 1984) — resolved. + +For any simple graph `G` on `n` vertices, + `box(G) ≤ ⌊n / 2⌋`. + +This bound follows because every graph on `n` vertices can be represented +as the intersection of at most `n / 2` interval graphs. -/ +@[category research solved, AMS 5] +theorem boxicity_le_card_div_two (G : SimpleGraph α) [DecidableRel G.Adj] : + boxicity G ≤ Fintype.card α / 2 := by + sorry + +-- Sanity checks + +/-- `boxicity` is a natural number (nonneg). -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 4)) : 0 ≤ boxicity G := Nat.zero_le _ + +/-- `boxicity` of any graph on `Fin 3` is a natural number (sanity). -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 3)) : 0 ≤ boxicity G := Nat.zero_le _ + +/-- `boxicity` cast to `ℝ` is nonneg. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 5)) : (0 : ℝ) ≤ (boxicity G : ℝ) := + Nat.cast_nonneg _ + +end WrittenOnTheWallII.GraphBoxicity diff --git a/FormalConjectures/WrittenOnTheWallII/GraphCircumference.lean b/FormalConjectures/WrittenOnTheWallII/GraphCircumference.lean new file mode 100644 index 0000000000..992b8bcde7 --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphCircumference.lean @@ -0,0 +1,91 @@ +/- +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 Circumference Conjecture + +*Reference:* +[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/) + +## Definitions + +The **circumference** of a graph `G` is the length (number of edges) of a +longest cycle in `G`. If `G` is acyclic (a forest), the circumference is +defined to be 0. + +## Conjecture + +A classical result due to Dirac (1952) states that every 2-connected graph +satisfies `circumference(G) ≥ 2 · δ(G)` where `δ(G)` is the minimum degree. +We state it as a conjecture in the Graffiti.pc style. +-/ + +namespace WrittenOnTheWallII.GraphCircumference + +open Classical SimpleGraph + +variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α] + +/-- The **circumference** of `G` is the length of a longest cycle. +It equals 0 for acyclic graphs (forests). -/ +noncomputable def circumference (G : SimpleGraph α) : ℕ := + sSup ({0} ∪ {k | ∃ v : α, ∃ w : G.Walk v v, w.IsCycle ∧ w.length = k}) + +/-- 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) } + +/-- Dirac's theorem (1952): Every 2-connected graph `G` on `n ≥ 3` vertices +satisfies `circumference(G) ≥ 2 · δ(G)`. +Here `δ(G) = G.minDegree` is the minimum degree and 2-connectivity means +`vertexConnectivity G ≥ 2`. -/ +@[category research solved, AMS 5] +theorem dirac_circumference (G : SimpleGraph α) [DecidableRel G.Adj] + (hconn : 2 ≤ vertexConnectivity G) : + 2 * G.minDegree ≤ circumference G := by + sorry + +-- Sanity checks + +/-- The circumference of `K₃` is 3 (the triangle itself is a 3-cycle). -/ +@[category test, AMS 5] +example : circumference (⊤ : SimpleGraph (Fin 3)) = 3 := by + unfold circumference + sorry + +/-- The circumference of the 4-cycle `C₄` is 4. -/ +@[category test, AMS 5] +example : circumference (SimpleGraph.fromEdgeSet + {s(0,1), s(1,2), s(2,3), s(3,0)} : SimpleGraph (Fin 4)) = 4 := by + unfold circumference + sorry + +/-- For a path `P₃` (which is acyclic), the circumference is 0. -/ +@[category test, AMS 5] +example : circumference + (SimpleGraph.fromEdgeSet {s(0,1), s(1,2)} : SimpleGraph (Fin 3)) = 0 := by + unfold circumference + sorry + +end WrittenOnTheWallII.GraphCircumference diff --git a/FormalConjectures/WrittenOnTheWallII/GraphCrossingNumber.lean b/FormalConjectures/WrittenOnTheWallII/GraphCrossingNumber.lean new file mode 100644 index 0000000000..018af1a49e --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphCrossingNumber.lean @@ -0,0 +1,111 @@ +/- +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 Crossing Number + +*Reference:* +[M. R. Garey and D. S. Johnson, Crossing number is NP-complete, SIAM J. Algebraic Discrete +Methods 4 (1983) 312–316](https://doi.org/10.1137/0604033) + +[R. B. Richter and C. Thomassen, Minimal graphs with crossing number at least k, +J. Combin. Theory Ser. B 58 (1993) 217–224] + +[F. T. Leighton, Complexity issues in VLSI, MIT Press, 1983] + +## Definition + +The **crossing number** `cr(G)` of a graph `G` is the minimum number of edge +crossings over all drawings of `G` in the plane (where vertices map to distinct +points and edges to Jordan arcs between their endpoints, with only finitely many +pairwise crossings, each transverse and not at a vertex). + +A full geometric formalization of this definition requires substantial topological +infrastructure. We use a placeholder definition here. + +-- TODO: replace `Classical.choice` with a proper topological definition once +-- Mathlib has sufficient support for planar graph drawings (Jordan curves, etc.). + +## Conjecture + +**Zarankiewicz's conjecture** (1954) — **open**: + `cr(K_{m,n}) = ⌊m/2⌋ · ⌊(m−1)/2⌋ · ⌊n/2⌋ · ⌊(n−1)/2⌋`. + +The formula gives the number of crossings in the standard "cylindrical" drawing +of the complete bipartite graph `K_{m,n}`. The conjecture is known to hold for +`min(m, n) ≤ 6` but remains open in general. +-/ + +namespace WrittenOnTheWallII.GraphCrossingNumber + +open Classical SimpleGraph + +variable {α : Type*} [Fintype α] [DecidableEq α] + +/-- The **crossing number** of a graph `G`: the minimum number of edge crossings +in any planar drawing of `G`. + +-- TODO: this is a placeholder. A geometric formalization requires defining +-- graph drawings as continuous maps from topological realizations of `G` into +-- `ℝ²`, together with a count of transverse crossing points. The placeholder +-- returns an arbitrary natural number via `Classical.choice`. -/ +noncomputable def crossingNumber (_ : SimpleGraph α) : ℕ := + Classical.choice (⟨0⟩ : Nonempty ℕ) + +/-- **Zarankiewicz's conjecture** (1954) — **open**. + +For the complete bipartite graph `K_{m,n}` (here modeled as the complete +bipartite graph on `Fin m ⊕ Fin n`): + `cr(K_{m,n}) = ⌊m/2⌋ · ⌊(m−1)/2⌋ · ⌊n/2⌋ · ⌊(n−1)/2⌋`. + +The right-hand side counts the crossings in the standard cylindrical drawing. -/ +@[category research open, AMS 5] +theorem zarankiewicz_conjecture (m n : ℕ) : + crossingNumber (completeBipartiteGraph (Fin m) (Fin n)) = + (m / 2) * ((m - 1) / 2) * (n / 2) * ((n - 1) / 2) := by + sorry + +/-- **Crossing Lemma** (Ajtai–Chvátal–Newborn–Szemerédi / Leighton, 1982) — resolved. + +For any simple graph `G` with `|E| ≥ 4 |V|`: + `cr(G) ≥ |E|³ / (64 · |V|²)`. + +We state the inequality in terms of `Fintype.card` and `G.edgeFinset.card`. -/ +@[category research solved, AMS 5] +theorem crossing_lemma [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] + (h : 4 * Fintype.card α ≤ G.edgeFinset.card) : + (G.edgeFinset.card : ℝ) ^ 3 / (64 * (Fintype.card α : ℝ) ^ 2) ≤ + crossingNumber G := by + sorry + +-- Sanity checks + +/-- `crossingNumber` is a natural number (nonneg). -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 4)) : 0 ≤ crossingNumber G := Nat.zero_le _ + +/-- `crossingNumber` of any graph on `Fin 3` is a natural number (sanity). -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 3)) : 0 ≤ crossingNumber G := Nat.zero_le _ + +/-- `crossingNumber` cast to `ℝ` is nonneg. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 5)) : (0 : ℝ) ≤ (crossingNumber G : ℝ) := + Nat.cast_nonneg _ + +end WrittenOnTheWallII.GraphCrossingNumber diff --git a/FormalConjectures/WrittenOnTheWallII/GraphDegeneracy.lean b/FormalConjectures/WrittenOnTheWallII/GraphDegeneracy.lean new file mode 100644 index 0000000000..e6c2c188bc --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphDegeneracy.lean @@ -0,0 +1,93 @@ +/- +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 Degeneracy and the Coloring Bound + +*Reference:* +[L. Lick and A. White, k-degenerate graphs, Canad. J. Math. 22 (1970) 1082–1096](https://doi.org/10.4153/CJM-1970-125-1) + +## Definition + +A graph `G` is **k-degenerate** if every induced subgraph has a vertex of +degree at most `k`. The **degeneracy** `d(G)` is the smallest such `k`. + +Equivalently, `d(G) = max { minDegree(H) | H induced subgraph of G }`. + +## Conjecture + +A classical greedy argument (resolved) shows: + `χ(G) ≤ d(G) + 1`. + +The bound is tight: for the complete graph `Kₙ`, `d(Kₙ) = n − 1` and `χ(Kₙ) = n`. +-/ + +namespace WrittenOnTheWallII.GraphDegeneracy + +open Classical SimpleGraph + +variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α] + +/-- The **degeneracy** of `G`: the maximum, over all nonempty induced subgraphs `H`, +of the minimum degree of `H`. + +We take the supremum over all nonempty vertex subsets `S : Finset α` of +`minDegree(G[S])`. For the empty set we contribute 0 so the `sup` is over a +nonempty domain (`Finset.univ` includes `∅`). -/ +noncomputable def degeneracy (G : SimpleGraph α) : ℕ := + Finset.univ.sup (fun S : Finset α => + if S.Nonempty then (G.induce (S : Set α)).minDegree else 0) + +/-- **Degeneracy coloring bound** — resolved (greedy coloring). + +For any simple graph `G`, + `χ(G) ≤ degeneracy(G) + 1`. + +Proof sketch: order vertices by the degeneracy ordering (repeatedly remove a +minimum-degree vertex); a greedy coloring then uses at most `d(G) + 1` colors +since each vertex has at most `d(G)` earlier neighbors. -/ +@[category research solved, AMS 5] +theorem chromaticNumber_le_degeneracy_add_one (G : SimpleGraph α) [DecidableRel G.Adj] : + G.chromaticNumber ≤ (degeneracy G + 1 : ℕ∞) := by + sorry + +/-- **Degeneracy lower bound from clique number** — resolved. + +For any simple graph `G`, `degeneracy(G) ≥ G.cliqueNum − 1`, because the +complete subgraph `Kₖ` is an induced subgraph with `minDegree = k − 1`. -/ +@[category research solved, AMS 5] +theorem degeneracy_ge_cliqueNum_sub_one (G : SimpleGraph α) [DecidableRel G.Adj] : + G.cliqueNum - 1 ≤ degeneracy G := by + sorry + +-- Sanity checks + +/-- `degeneracy` is a natural number (nonneg). -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 4)) : 0 ≤ degeneracy G := Nat.zero_le _ + +/-- `degeneracy` of any graph on `Fin 3` is a natural number (sanity). -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 3)) : 0 ≤ degeneracy G := Nat.zero_le _ + +/-- `degeneracy` cast to `ℝ` is nonneg. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 5)) : (0 : ℝ) ≤ (degeneracy G : ℝ) := + Nat.cast_nonneg _ + +end WrittenOnTheWallII.GraphDegeneracy diff --git a/FormalConjectures/WrittenOnTheWallII/GraphDistOdd.lean b/FormalConjectures/WrittenOnTheWallII/GraphDistOdd.lean new file mode 100644 index 0000000000..3078a64a1b --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphDistOdd.lean @@ -0,0 +1,121 @@ +/- +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 + +/-! +# distOdd Invariant and WOWII Conjecture + +*Reference:* +[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/) + +## Definitions + +For a vertex `v` in a graph `G`, define: +- `distEven G v`: number of vertices at **even** distance from `v` (including `v` itself + at distance 0). +- `distOdd G v`: number of vertices at **odd** distance from `v`. + +These two quantities partition the vertex set: `distEven G v + distOdd G v = n`. + +## Conjecture + +This file states a Graffiti.pc-style upper bound using the minimum of +`distOdd`: + +`α(G) ≤ 1 + min_v distOdd(v) · (max_v l(v) - 1)` + +where `α(G) = G.indepNum` is the independence number and `l(v) = indepNeighborsCard G v`. + +**Not a verbatim WOWII transcription.** This is the `distOdd`-analogue of +WOWII Conjecture 96 (which uses `distEven`); we file it as a new +Graffiti.pc-style observation rather than a formalisation of any specific +numbered WOWII conjecture. + +For bipartite graphs, one of the two parts has all vertices at even (resp. odd) distance +from any fixed vertex in one part; so `distOdd` tracks the "opposite part" size. +-/ + +namespace WrittenOnTheWallII.GraphDistOdd + +open Classical SimpleGraph + +variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α] + +/-- `distOdd G v` counts the number of vertices at odd distance from `v` in `G`. +Note: since `G.dist v v = 0` is even, `v` itself is never counted here. -/ +noncomputable def distOdd (G : SimpleGraph α) (v : α) : ℕ := + (Finset.univ.filter (fun w => Odd (G.dist v w))).card + +/-- `distEven G v` counts the number of vertices at even distance from `v` in `G`, +including `v` itself (at distance 0). -/ +noncomputable def distEven (G : SimpleGraph α) (v : α) : ℕ := + (Finset.univ.filter (fun w => Even (G.dist v w))).card + +/-- For any vertex `v`, `distEven G v + distOdd G v = Fintype.card α`: +every vertex is at either even or odd distance from `v`. -/ +@[category research solved, AMS 5] +theorem distEven_add_distOdd (G : SimpleGraph α) (v : α) : + distEven G v + distOdd G v = Fintype.card α := by + unfold distEven distOdd + rw [← Finset.card_union_of_disjoint] + · rw [← Finset.filter_or] + congr 1 + ext w; simp + exact (Nat.even_or_odd (G.dist v w)).imp id id + · apply Finset.disjoint_filter.mpr + intro w _ he ho + exact (Nat.not_odd_iff_even.mpr he) ho + +/-- +**distOdd upper bound for the independence number** (WOWII-style conjecture). + +For a simple connected graph `G`, +`α(G) ≤ 1 + min_v distOdd(v) · (max_v l(v) - 1)` +where `α(G) = G.indepNum` is the independence number, +`distOdd(v)` is the number of vertices at odd distance from `v`, and +`max_v l(v)` is the maximum independence number of a vertex neighbourhood. + +This is the odd-distance analogue of WOWII Conjecture 96. +-/ +@[category research open, AMS 5] +theorem distOdd_indepNum_upper_bound (G : SimpleGraph α) [DecidableRel G.Adj] + (hconn : G.Connected) : + let minDistOdd := (Finset.univ.image (distOdd G)).min' (by simp) + let maxL := (Finset.univ.image (indepNeighborsCard G)).max' (by simp) + (G.indepNum : ℝ) ≤ 1 + (minDistOdd : ℝ) * ((maxL : ℝ) - 1) := by + sorry + +-- Sanity checks + +/-- `distOdd G v` is a natural number (nonneg). -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 3)) (v : Fin 3) : 0 ≤ distOdd G v := Nat.zero_le _ + +/-- `distOdd K₃ 0 = 2`: from vertex 0 in `K₃`, both vertices 1 and 2 are at distance 1 +(odd). -/ +@[category test, AMS 5] +example : distOdd (⊤ : SimpleGraph (Fin 3)) 0 = 2 := by + unfold distOdd + sorry + +/-- `distEven K₃ 0 + distOdd K₃ 0 = 3 = Fintype.card (Fin 3)`. -/ +@[category test, AMS 5] +example : distEven (⊤ : SimpleGraph (Fin 3)) 0 + distOdd (⊤ : SimpleGraph (Fin 3)) 0 = 3 := by + have := distEven_add_distOdd (⊤ : SimpleGraph (Fin 3)) 0 + simpa using this + +end WrittenOnTheWallII.GraphDistOdd diff --git a/FormalConjectures/WrittenOnTheWallII/GraphEdgeConnectivity.lean b/FormalConjectures/WrittenOnTheWallII/GraphEdgeConnectivity.lean new file mode 100644 index 0000000000..0317050643 --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphEdgeConnectivity.lean @@ -0,0 +1,120 @@ +/- +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 + +/-! +# Edge Connectivity + +*Reference:* +[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/) + +## Definitions + +The **edge connectivity** `λ(G)` is the minimum number of edges whose removal +disconnects `G` (or reduces it to a single vertex). Formally, + `λ(G) = min { |F| | F ⊆ E(G), G - F is disconnected }`. + +For the edgeless graph or a single-vertex graph, we define `λ(G) = 0`. + +## Classical bound + +`λ(G) ≤ δ(G)` — the edge connectivity is at most the minimum degree. + +This is a classical theorem: for any vertex `v` of minimum degree, the `δ(G)` +edges incident to `v` form a disconnecting set (removing them isolates `v`). + +## WOWII-style conjecture + +A Graffiti.pc lower bound relating edge connectivity to the independence number: + +`α(G) ≤ n(G) - λ(G)` + +where `α(G)` is the independence number and `n = |V(G)|`. This holds because +the complement of any independent set spans at most `n - α(G)` vertices, which +must still be connected; removing all edges incident to an independent set +disconnects at most `α(G)` vertices. +-/ + +namespace WrittenOnTheWallII.GraphEdgeConnectivity + +open Classical SimpleGraph + +variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α] + +/-- The **edge connectivity** `λ(G)` of a simple graph `G`. + +We define it as the minimum size of a set of edges `F ⊆ E(G)` whose removal +renders `G` disconnected. If no such set exists (i.e., `G` has ≤ 1 vertex or +is already disconnected), we define `λ(G) = 0`. -/ +noncomputable def edgeConnectivity (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ := + sInf { k | ∃ F : Finset (Sym2 α), + F.card = k ∧ + (↑F : Set (Sym2 α)) ⊆ G.edgeSet ∧ + ¬ (G.deleteEdges ↑F).Connected } + +/-- +**Classical bound:** `λ(G) ≤ δ(G)`. + +The edge connectivity is at most the minimum degree. Removing all edges +incident to a minimum-degree vertex disconnects (or isolates) it, giving a +disconnecting set of size `δ(G)`. +-/ +@[category research solved, AMS 5] +theorem edgeConnectivity_le_minDegree (G : SimpleGraph α) [DecidableRel G.Adj] + (hconn : G.Connected) : + edgeConnectivity G ≤ G.minDegree := by + sorry + +/-- +**Independence-number upper bound** (WOWII-style). + +For a connected graph `G`, +`α(G) + λ(G) ≤ n(G)` +i.e., `G.indepNum + edgeConnectivity G ≤ Fintype.card α`. + +Intuitively, the complement of a maximum independent set induces a connected +subgraph (since `G` is connected and removing an independent set cannot alone +disconnect the rest without removing edges); a sharper version says we need at +least `λ(G)` edge removals to disconnect, so `n - α ≥ λ`. +-/ +@[category research open, AMS 5] +theorem indepNum_add_edgeConnectivity_le_card (G : SimpleGraph α) [DecidableRel G.Adj] + (hconn : G.Connected) : + G.indepNum + edgeConnectivity G ≤ Fintype.card α := by + sorry + +-- Sanity checks + +/-- `edgeConnectivity` is a natural number (nonneg). -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 3)) [DecidableRel G.Adj] : 0 ≤ edgeConnectivity G := + Nat.zero_le _ + +/-- For `K₃`, `minDegree = 2` and `edgeConnectivity ≤ 2` +(removing the two edges incident to vertex 0 disconnects it). -/ +@[category test, AMS 5] +example : edgeConnectivity (⊤ : SimpleGraph (Fin 3)) ≤ 2 := by + unfold edgeConnectivity + apply Nat.sInf_le + exact ⟨{s(0, 1), s(0, 2)}, by decide, by sorry, by sorry⟩ + +/-- `edgeConnectivity` is nonneg as a real number. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 4)) [DecidableRel G.Adj] : (0 : ℝ) ≤ (edgeConnectivity G : ℝ) := + Nat.cast_nonneg _ + +end WrittenOnTheWallII.GraphEdgeConnectivity diff --git a/FormalConjectures/WrittenOnTheWallII/GraphEvenModeMin.lean b/FormalConjectures/WrittenOnTheWallII/GraphEvenModeMin.lean new file mode 100644 index 0000000000..fe36af0af6 --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphEvenModeMin.lean @@ -0,0 +1,98 @@ +/- +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 +import FormalConjectures.WrittenOnTheWallII.GraphMode + +/-! +# Graph Even Mode-Min Count Invariant + +*Reference:* +[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/) + +## Definition + +Recall that `modeDegreeMin G` (from `GraphMode.lean`) is the smallest degree +value that achieves the mode frequency in the degree sequence of `G`. + +The **even mode-min count** `evenModeMinCount G` is the number of vertices `v` +whose degree is equal to `modeDegreeMin G` **and** whose degree is even. In +other words, it counts vertices at the minimum modal degree if and only if that +degree value is even (otherwise the count is 0). + +## Conjecture + +WOWII-style conjecture: For a simple connected graph `G`, +`G.indepNum ≤ evenModeMinCount G * (Finset.univ.sup (indepNeighborsCard G)) + 1`. + +The right-hand side bounds the independence number by the product of the +"even-parity mode-frequency" and the maximum neighbourhood independence value, +plus 1. This mirrors the Graffiti.pc philosophy of combining frequency +statistics with neighbourhood invariants. +-/ + +namespace WrittenOnTheWallII.GraphEvenModeMin + +open Classical SimpleGraph WrittenOnTheWallII.GraphMode + +variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α] + +/-- The number of vertices whose degree equals `modeDegreeMin G` **and** is even. +When `modeDegreeMin G` is odd, every vertex counted by `modeDegreeMin G` has an +odd degree, so `evenModeMinCount G = 0`. -/ +noncomputable def evenModeMinCount (G : SimpleGraph α) : ℕ := + (Finset.univ.filter (fun v => G.degree v = modeDegreeMin G ∧ Even (G.degree v))).card + +/-- +**WOWII-style open conjecture**: For a simple connected graph `G`, +`G.indepNum ≤ evenModeMinCount G * (Finset.univ.sup (indepNeighborsCard G)) + 1`. + +The independence number is bounded above by the product of the number of vertices +at the minimum modal degree (even-degree variant) and the maximum neighbourhood +independence number, plus 1. The `+1` accounts for the case where +`evenModeMinCount G = 0` (all vertices at the minimum modal degree have odd +degree), in which case the bound trivially becomes `G.indepNum ≤ 1`. +-/ +@[category research open, AMS 5] +theorem evenModeMinCount_indepNum_bound (G : SimpleGraph α) [DecidableRel G.Adj] + (hconn : G.Connected) : + G.indepNum ≤ evenModeMinCount G * Finset.univ.sup (indepNeighborsCard G) + 1 := by + sorry + +-- Sanity checks + +/-- In `K₃`, every vertex has degree 2 (even), `modeDegreeMin K₃ = 2`, so all +3 vertices qualify; `evenModeMinCount K₃ = 3`. -/ +@[category test, AMS 5] +example : evenModeMinCount (⊤ : SimpleGraph (Fin 3)) = 3 := by + unfold evenModeMinCount modeDegreeMin maxDegreeCount degreeCount + sorry + +/-- In the path `P₃` (0–1–2), degrees are `[1, 2, 1]`. `modeDegreeMin P₃ = 1` +(degree 1 appears twice, degree 2 appears once). Degree 1 is odd, so no vertex +qualifies; `evenModeMinCount P₃ = 0`. -/ +@[category test, AMS 5] +example : evenModeMinCount + (SimpleGraph.fromEdgeSet {s(0,1), s(1,2)} : SimpleGraph (Fin 3)) = 0 := by + unfold evenModeMinCount modeDegreeMin maxDegreeCount degreeCount + sorry + +/-- `evenModeMinCount` is nonneg. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 4)) : 0 ≤ evenModeMinCount G := + Nat.zero_le _ + +end WrittenOnTheWallII.GraphEvenModeMin diff --git a/FormalConjectures/WrittenOnTheWallII/GraphFrequencyMaxL.lean b/FormalConjectures/WrittenOnTheWallII/GraphFrequencyMaxL.lean new file mode 100644 index 0000000000..6841e394e6 --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphFrequencyMaxL.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 209 + +**Verbatim statement (WOWII #209, status O):** +> If G is a simple connected graph with n > 1 such that +> (1/6) * [1 + 2 * |E(Ḡ)|] ≤ frequency of λ_max(G), +> then G has a Hamiltonian path. + +**Source:** http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj209 + +Here `λ_max(G)` is interpreted as `max_v l(v)` (the maximum over vertices of +the independence number of the open neighbourhood, the standard reading of +the Greek `λ` across the WOWII conjectures), and `frequency of λ_max(G)` is +the number of vertices `v` that achieve this maximum. `|E(Ḡ)|` is the +edge count of the complement of `G`. + +*Reference:* +[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/) +-/ + +namespace WrittenOnTheWallII.GraphFrequencyMaxL + +open Classical SimpleGraph + +variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α] + +/-- The maximum value of `indepNeighborsCard G v` over all vertices `v`. -/ +noncomputable def maxLValue (G : SimpleGraph α) : ℕ := + Finset.univ.sup (indepNeighborsCard G) + +/-- The number of vertices `v` that achieve the maximum value of +`indepNeighborsCard G v`. This is the "frequency of `λ_max(G)`". -/ +noncomputable def frequencyMaxL (G : SimpleGraph α) : ℕ := + (Finset.univ.filter (fun v => indepNeighborsCard G v = maxLValue G)).card + +/-- +WOWII [Conjecture 209](http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj209) +(status O): + +If `G` is a simple connected graph on `n > 1` vertices and +`(1/6) · (1 + 2 · |E(Gᶜ)|) ≤ frequencyMaxL G`, +then `G` has a Hamiltonian path. +-/ +@[category research open, AMS 5] +theorem conjecture209 (G : SimpleGraph α) + [DecidableRel G.Adj] [DecidableRel Gᶜ.Adj] + (hn : 1 < Fintype.card α) + (h : G.Connected) + (hbound : (1 : ℝ) / 6 * (1 + 2 * (Gᶜ.edgeFinset.card : ℝ)) ≤ frequencyMaxL G) : + ∃ a b : α, ∃ p : G.Walk a b, p.IsHamiltonian := by + sorry + +-- Sanity checks + +/-- `frequencyMaxL` is nonneg. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 4)) : 0 ≤ frequencyMaxL G := Nat.zero_le _ + +/-- `maxLValue` is nonneg. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 3)) : 0 ≤ maxLValue G := Nat.zero_le _ + +end WrittenOnTheWallII.GraphFrequencyMaxL diff --git a/FormalConjectures/WrittenOnTheWallII/GraphGeodeticNumber.lean b/FormalConjectures/WrittenOnTheWallII/GraphGeodeticNumber.lean new file mode 100644 index 0000000000..a6ae41ad17 --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphGeodeticNumber.lean @@ -0,0 +1,111 @@ +/- +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 + +/-! +# Geodetic Number of Graphs + +*Reference:* +[F. Buckley and F. Harary, Distance in Graphs, Addison-Wesley, 1990] + +[G. Chartrand, F. Harary, P. Zhang, On the geodetic number of a graph, +Networks 39 (2002) 1–6](https://doi.org/10.1002/net.10007) + +## Definition + +A set `S ⊆ V(G)` is a **geodetic set** if every vertex of `G` lies on some +shortest path (geodesic) between two vertices of `S`. + +The **geodetic number** `g(G)` is the minimum cardinality of a geodetic set. + +## Conjecture + +A classical fact (resolved) is that for the complete graph `Kₙ`, +`g(Kₙ) = n`, since every vertex must be an endpoint of some geodesic in `S` +(all shortest paths have length 1, so each vertex must appear in `S` itself). + +A nontrivial open conjecture is that for any connected graph `G`, +`g(G) ≤ diam(G) + 1` is **false** in general (e.g., it fails for hypercubes), +so we instead state the resolved classical lower bound `g(G) ≥ 2` for connected +graphs with at least 2 vertices, and the Graffiti.pc-style upper bound +`g(G) ≤ n − diam(G) + 1` for connected graphs (a known resolved bound). +-/ + +namespace WrittenOnTheWallII.GraphGeodeticNumber + +open Classical SimpleGraph + +variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α] + +/-- A set `S` is a **geodetic set** of `G` if every vertex `v` lies on a +shortest `u`-`w` path for some `u, w ∈ S`. + +A walk `p` is a shortest path from `u` to `w` if it is a path and its length +equals `G.dist u w`. -/ +def IsGeodeticSet (G : SimpleGraph α) (S : Finset α) : Prop := + ∀ v : α, ∃ u ∈ S, ∃ w ∈ S, + ∃ p : G.Walk u w, p.IsPath ∧ p.length = G.dist u w ∧ v ∈ p.support + +/-- The **geodetic number** of `G`: the minimum size of a geodetic set. +Returns 0 when no geodetic set exists; for any connected graph with ≥ 2 vertices +the value is at least 2. -/ +noncomputable def geodeticNumber (G : SimpleGraph α) : ℕ := + sInf {k | ∃ S : Finset α, S.card = k ∧ IsGeodeticSet G S} + +/-- **Geodetic number lower bound** — resolved. + +For any connected graph `G` with at least 2 vertices, `geodeticNumber(G) ≥ 2`. + +Proof: the geodetic set `S` must include at least two vertices (one geodesic +must start and end at distinct points), and both endpoints must be in `S`. -/ +@[category research solved, AMS 5] +theorem geodeticNumber_ge_two (G : SimpleGraph α) [DecidableRel G.Adj] + (hconn : G.Connected) (hn : 2 ≤ Fintype.card α) : + 2 ≤ geodeticNumber G := by + sorry + +/-- **Geodetic number upper bound** — resolved. + +For any connected graph `G` on `n` vertices, + `geodeticNumber(G) ≤ n − diam(G) + 1` +where `diam(G) = (maxEccentricity G).toNat`. + +Proof sketch: take a diametral path `v₀–v₁–⋯–v_d`; the set `{v₀} ∪ (V \ {v₁,…,v_{d-1}})` +is a geodetic set of size `n − d + 1`. -/ +@[category research solved, AMS 5] +theorem geodeticNumber_le_card_sub_diam_add_one (G : SimpleGraph α) [DecidableRel G.Adj] + (hconn : G.Connected) (hn : 2 ≤ Fintype.card α) : + geodeticNumber G ≤ Fintype.card α - (maxEccentricity G).toNat + 1 := by + sorry + +-- Sanity checks + +/-- `geodeticNumber` is a natural number (nonneg). -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 4)) : 0 ≤ geodeticNumber G := Nat.zero_le _ + +/-- `IsGeodeticSet` is a well-formed proposition on small graphs. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 3)) (S : Finset (Fin 3)) : IsGeodeticSet G S ∨ True := + Or.inr trivial + +/-- `geodeticNumber` cast to `ℝ` is nonneg. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 5)) : (0 : ℝ) ≤ (geodeticNumber G : ℝ) := + Nat.cast_nonneg _ + +end WrittenOnTheWallII.GraphGeodeticNumber diff --git a/FormalConjectures/WrittenOnTheWallII/GraphGirthComplement.lean b/FormalConjectures/WrittenOnTheWallII/GraphGirthComplement.lean new file mode 100644 index 0000000000..d9b5568319 --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphGirthComplement.lean @@ -0,0 +1,104 @@ +/- +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 + +/-! +# Girth of the Complement Graph + +*Reference:* +[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/) + +## Definition + +The **complement girth** `girthComplement G` of a graph `G` is the girth of the +complement graph `Gᶜ`, i.e., the length of a shortest cycle in `Gᶜ`. By the +Mathlib convention, `SimpleGraph.girth Gᶜ = 0` when `Gᶜ` is acyclic (a forest +or edgeless graph). + +## Conjectures + +1. (Test case) The complement of `K₃` (complete graph on 3 vertices) is the + empty graph (no edges), which is acyclic, so `girthComplement K₃ = 0`. + +2. (Open) For any simple graph `G`, either `G` contains a triangle or + `G.indepNum ≤ girthComplement G`. Informally, if `G` is triangle-free then + its complement `Gᶜ` is "sparse enough" that the girth of `Gᶜ` is a valid + upper bound for the independence number of `G`. +-/ + +namespace WrittenOnTheWallII.GraphGirthComplement + +open Classical SimpleGraph + +variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α] + +/-- The **complement girth** of `G` is the girth of its complement graph `Gᶜ`. +Returns 0 when `Gᶜ` is acyclic (including when `Gᶜ` has no edges). -/ +noncomputable def girthComplement (G : SimpleGraph α) : ℕ := + Gᶜ.girth + +/-- +**Test-case fact**: The complement of `K_n` (the complete graph on `n` vertices) +is the empty graph (no edges). An edgeless graph has no cycles, so its girth is 0 +by the Mathlib convention. In particular, `girthComplement (⊤ : SimpleGraph (Fin n)) = 0`. +-/ +@[category research solved, AMS 5] +theorem girthComplement_completeGraph (n : ℕ) : + girthComplement (⊤ : SimpleGraph (Fin n)) = 0 := by + unfold girthComplement + simp [compl_top] + +/-- +**WOWII-style open conjecture**: For any simple connected graph `G`, +either `G` contains a triangle (a 3-clique) or `G.indepNum ≤ girthComplement G`. + +Informally: if `G` has no triangle then the complement `Gᶜ` must be relatively +dense (many edges), which tends to create short cycles and thus a small +`girthComplement G`. Meanwhile, the independence number of a triangle-free graph +can be large. The conjecture asserts that these two quantities are in balance +unless a triangle is present. +-/ +@[category research open, AMS 5] +theorem indepNum_le_girthComplement_or_triangle (G : SimpleGraph α) [DecidableRel G.Adj] + (hconn : G.Connected) : + (∃ v w x : α, G.Adj v w ∧ G.Adj w x ∧ G.Adj v x) ∨ + G.indepNum ≤ girthComplement G := by + sorry + +-- Sanity checks + +/-- The complement of the 6-cycle `C₆` is the graph `2K₃` (two disjoint triangles). +Its girth is 3, so `girthComplement C₆ = 3`. -/ +@[category test, AMS 5] +example : girthComplement (cycleGraph 6) = 3 := by + unfold girthComplement + sorry + +/-- `girthComplement` is nonneg. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 4)) : 0 ≤ girthComplement G := + Nat.zero_le _ + +/-- For the path `P₃` (0–1–2), the complement has the single edge `{0, 2}`, which +is acyclic, so `girthComplement P₃ = 0`. -/ +@[category test, AMS 5] +example : girthComplement + (SimpleGraph.fromEdgeSet {s(0,1), s(1,2)} : SimpleGraph (Fin 3)) = 0 := by + unfold girthComplement + sorry + +end WrittenOnTheWallII.GraphGirthComplement diff --git a/FormalConjectures/WrittenOnTheWallII/GraphIsoperimetric.lean b/FormalConjectures/WrittenOnTheWallII/GraphIsoperimetric.lean new file mode 100644 index 0000000000..b2c216f189 --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphIsoperimetric.lean @@ -0,0 +1,124 @@ +/- +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 + +/-! +# Isoperimetric Number (Cheeger Constant) of a Graph + +*Reference:* +[B. Mohar, Isoperimetric numbers of graphs, +J. Combin. Theory Ser. B 47 (1989) 274–291](https://doi.org/10.1016/0095-8956(89)90029-4) + +## Definition + +For a finite simple graph `G = (V, E)` and a set `S ⊆ V`, the **edge boundary** +`∂(S)` is the set of edges with one endpoint in `S` and the other in `V \ S`. +The **isoperimetric number** (Cheeger constant) of `G` is + + `h(G) = min { |∂(S)| / |S| | S ⊆ V, S ≠ ∅, 2·|S| ≤ |V| }`. + +This measures how "well-connected" a graph is: a large `h(G)` means no small set +has a small boundary. + +## Conjectures + +1. (Resolved) `h(G) ≤ Δ(G)` (maximum degree bound): every vertex in `S` + contributes at most `Δ(G)` edges to the boundary, so `|∂(S)| ≤ Δ(G) · |S|`. + +2. (Open — Cheeger inequality for graphs) `h(G)² / (2 · Δ(G)) ≤ λ₁(G) ≤ 2·h(G)`, + where `λ₁(G)` is the smallest positive eigenvalue of the Laplacian of `G` + (algebraic connectivity / Fiedler value). +-/ + +namespace WrittenOnTheWallII.GraphIsoperimetric + +open Classical SimpleGraph + +variable {α : Type*} [Fintype α] [DecidableEq α] + +/-- The **edge boundary cardinality** `|∂(S)|`: the number of edges of `G` with +exactly one endpoint in `S`. -/ +noncomputable def edgeBoundaryCard (G : SimpleGraph α) [DecidableRel G.Adj] + (S : Finset α) : ℕ := + (G.edgeFinset.filter (fun e => + Sym2.lift ⟨fun u v => (u ∈ S) ≠ (v ∈ S), fun u v => by simp [Iff.comm]⟩ e)).card + +/-- The **isoperimetric number** (Cheeger constant) `h(G)`: + `h(G) = inf { |∂(S)| / |S| | S ⊆ V, S ≠ ∅, 2·|S| ≤ n }`. + +We take the infimum over nonempty vertex subsets `S` satisfying `2 · |S| ≤ n` +of the ratio `|∂(S)| / |S|` as a real number. -/ +noncomputable def isoperimetricNumber (G : SimpleGraph α) [DecidableRel G.Adj] : ℝ := + sInf {r | ∃ S : Finset α, S.Nonempty ∧ 2 * S.card ≤ Fintype.card α ∧ + r = (edgeBoundaryCard G S : ℝ) / (S.card : ℝ)} + +/-- **Maximum-degree upper bound** (resolved): `h(G) ≤ Δ(G)`. + +For any nonempty `S` with `2·|S| ≤ n`, each vertex in `S` contributes at most +`Δ(G)` edges to `∂(S)`, giving `|∂(S)| ≤ Δ(G) · |S|` and hence +`|∂(S)| / |S| ≤ Δ(G)`. -/ +@[category research solved, AMS 5] +theorem isoperimetricNumber_le_maxDegree + (G : SimpleGraph α) [DecidableRel G.Adj] : + isoperimetricNumber G ≤ G.maxDegree := by + sorry + +/-- **Cheeger inequality** (open in this Lean formulation): the isoperimetric +number and the algebraic connectivity `mu` (smallest positive Laplacian +eigenvalue) satisfy + `isoperimetricNumber G ^ 2 / (2 * G.maxDegree) ≤ mu`. + +This is the discrete analogue of the classical Cheeger inequality in Riemannian +geometry. The matching upper bound `mu ≤ 2 · isoperimetricNumber G` is also +classical. -/ +@[category research open, AMS 5] +theorem cheeger_inequality + (G : SimpleGraph α) [DecidableRel G.Adj] + (hG : G.Connected) (hΔ : 0 < G.maxDegree) + (mu : ℝ) (hmu : mu > 0) + -- `hmu_spec` encodes that `mu` is the smallest positive Laplacian eigenvalue; + -- stated as a hypothesis to avoid full spectral-theory dependencies. + (hmu_spec : ∀ S : Finset α, S.Nonempty → 2 * S.card ≤ Fintype.card α → + (edgeBoundaryCard G S : ℝ) / (S.card : ℝ) ≥ Real.sqrt (2 * G.maxDegree * mu)) : + isoperimetricNumber G ^ 2 / (2 * G.maxDegree) ≤ mu := by + sorry + +-- Sanity checks + +/-- `isoperimetricNumber` is a real number — type-checks correctly. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 4)) [DecidableRel G.Adj] : + (isoperimetricNumber G : ℝ) = isoperimetricNumber G := + rfl + +/-- `edgeBoundaryCard` is a natural number (nonneg). -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 4)) [DecidableRel G.Adj] (S : Finset (Fin 4)) : + 0 ≤ edgeBoundaryCard G S := + Nat.zero_le _ + +/-- `isoperimetricNumber` cast to `ℝ` is nonneg. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 5)) [DecidableRel G.Adj] : + (0 : ℝ) ≤ isoperimetricNumber G := by + apply Real.sInf_nonneg (s := {r | ∃ S : Finset (Fin 5), S.Nonempty ∧ + 2 * S.card ≤ Fintype.card (Fin 5) ∧ + r = (edgeBoundaryCard G S : ℝ) / (S.card : ℝ)}) + rintro _ ⟨S, hS, _, rfl⟩ + positivity + +end WrittenOnTheWallII.GraphIsoperimetric diff --git a/FormalConjectures/WrittenOnTheWallII/GraphLength.lean b/FormalConjectures/WrittenOnTheWallII/GraphLength.lean new file mode 100644 index 0000000000..a284e23823 --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphLength.lean @@ -0,0 +1,87 @@ +/- +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 19 + +**Verbatim statement (WOWII #19, status O):** +> If G is a simple connected graph, then b(G) ≥ FLOOR(average of ecc(v) + maximum of λ(v)) + +**Source:** http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj19 + +Here `b(G)` is the **size of a largest induced bipartite subgraph** of `G` +(see `FormalConjecturesForMathlib.Combinatorics.SimpleGraph.GraphConjectures.Definitions`, +where `b` is defined). It is **not** the independence number. + +The DeLaVina note on the WOWII page (June 22, 2005) observes that if +`average of ecc(v) ≤ diam − 1`, this conjecture follows from Conjecture 13. + +The auxiliary `graphLength G = ∑_v ecc(v)` (`length(G)` in DeLaVina's +notation) is retained below because `length(G)/n = averageEccentricity G`, +and some neighbouring Graffiti.pc-style observations use the unscaled +`length(G)` directly. + +*Reference:* +[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/) +-/ + +namespace WrittenOnTheWallII.GraphLength + +open Classical SimpleGraph + +variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α] + +/-- The **length** of `G` in DeLaVina's WOWII notation: the sum of +eccentricities over all vertices. We have +`graphLength G / Fintype.card α = averageEccentricity G`. -/ +noncomputable def graphLength (G : SimpleGraph α) : ℕ := + ∑ v : α, (eccentricity G v).toNat + +/-- +WOWII [Conjecture 19](http://cms.uhd.edu/faculty/delavinae/research/wowII/all.html#conj19) +(status O): + +For a simple connected graph `G`, +`b(G) ≥ ⌊avg_v ecc(v) + max_v l(v)⌋`, +where `b(G)` is the size of a largest induced bipartite subgraph, +`ecc(v)` is the eccentricity of `v` (so `avg_v ecc(v) = averageEccentricity G`), +and `l(v) = indepNeighborsCard G v` is the independence number of the +neighbourhood of `v`. +-/ +@[category research open, AMS 5] +theorem conjecture19 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) : + let maxL := (Finset.univ.image (indepNeighborsCard G)).max' (by simp) + (⌊averageEccentricity G + (maxL : ℝ)⌋ : ℝ) ≤ b G := by + sorry + +-- Sanity checks + +/-- `graphLength` is a natural number (nonneg). -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 3)) : 0 ≤ graphLength G := Nat.zero_le _ + +/-- `graphLength` of any graph is nonneg as a real. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 4)) : (0 : ℝ) ≤ (graphLength G : ℝ) := + Nat.cast_nonneg _ + +/-- `b G` is nonneg. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 3)) : 0 ≤ b G := Nat.cast_nonneg _ + +end WrittenOnTheWallII.GraphLength diff --git a/FormalConjectures/WrittenOnTheWallII/GraphMedianDegree.lean b/FormalConjectures/WrittenOnTheWallII/GraphMedianDegree.lean new file mode 100644 index 0000000000..7c76ac7e64 --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphMedianDegree.lean @@ -0,0 +1,97 @@ +/- +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 Median Degree Invariant + +*Reference:* +[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/) + +## Definition + +The **median degree** of a graph `G` on `n` vertices is the middle value of the +sorted degree sequence. Concretely, we sort the list of degrees of all vertices +in non-decreasing order and return the element at index `n / 2` (integer +division), which is the lower median when `n` is even. + +For the empty graph (`n = 0`) the median degree is defined to be 0. + +## Conjecture + +For any simple connected graph `G` with at least 2 vertices, +`1 ≤ medianDegree G`. + +In a connected graph every vertex has degree at least 1, so every entry of the +sorted degree sequence is at least 1; in particular the middle entry is ≥ 1. +-/ + +namespace WrittenOnTheWallII.GraphMedianDegree + +open Classical SimpleGraph + +variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α] + +/-- The **median degree** of `G`. + +We form the list of degrees of all vertices, sort it in non-decreasing order, and +return the element at position `Fintype.card α / 2`. When the graph has no +vertices the degree list is empty; we return 0 in that case. -/ +noncomputable def medianDegree (G : SimpleGraph α) : ℕ := + if Fintype.card α = 0 then 0 + else + let degList : List ℕ := Finset.univ.toList.map (fun v => G.degree v) + let sorted : List ℕ := degList.mergeSort (· ≤ ·) + sorted.getD (Fintype.card α / 2) 0 + +/-- +**WOWII-style conjecture**: For a simple connected graph `G` with at least +2 vertices, `1 ≤ medianDegree G`. + +In a connected graph, every vertex has degree at least 1. Hence the sorted degree +sequence consists entirely of values ≥ 1, and in particular the element at the +median position is ≥ 1. +-/ +@[category research open, AMS 5] +theorem medianDegree_pos (G : SimpleGraph α) [DecidableRel G.Adj] + (hconn : G.Connected) : + 1 ≤ medianDegree G := by + sorry + +-- Sanity checks + +/-- In `K₃`, all degrees are 2, so the sorted sequence is `[2, 2, 2]` and the +median (at index 1) is 2. -/ +@[category test, AMS 5] +example : medianDegree (⊤ : SimpleGraph (Fin 3)) = 2 := by + unfold medianDegree + sorry + +/-- In the path `P₄` (0–1–2–3), degrees are `[1, 2, 2, 1]`. Sorted: `[1, 1, 2, 2]`. +The median at index `4 / 2 = 2` is 2. -/ +@[category test, AMS 5] +example : medianDegree + (SimpleGraph.fromEdgeSet {s(0,1), s(1,2), s(2,3)} : SimpleGraph (Fin 4)) = 2 := by + unfold medianDegree + sorry + +/-- `medianDegree` is nonneg. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 5)) : 0 ≤ medianDegree G := + Nat.zero_le _ + +end WrittenOnTheWallII.GraphMedianDegree diff --git a/FormalConjectures/WrittenOnTheWallII/GraphMetricDimension.lean b/FormalConjectures/WrittenOnTheWallII/GraphMetricDimension.lean new file mode 100644 index 0000000000..348a0ad6f1 --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphMetricDimension.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 + +/-! +# Metric Dimension of Graphs + +*Reference:* +[G. Chartrand, L. Eroh, M. A. Johnson, O. R. Oellermann, Resolvability in graphs and the metric +dimension of a graph, Discrete Appl. Math. 105 (2000) 99–113](https://doi.org/10.1016/S0166-218X(00)00198-0) + +## Definition + +A set `R ⊆ V(G)` is a **resolving set** if for every two distinct vertices +`u, v`, there exists `r ∈ R` such that `dist(u, r) ≠ dist(v, r)`. + +The **metric dimension** `dim(G)` is the minimum cardinality of a resolving set. + +## Conjecture + +A classical result (Chartrand et al., 2000, resolved) states: + `dim(G) ≤ |V(G)| − diam(G)` +for any connected graph `G` with `|V(G)| ≥ 2`, where `diam(G)` is the diameter. + +We also state the trivial resolved lower bound `dim(G) ≥ 1` for `|V(G)| ≥ 2`. +-/ + +namespace WrittenOnTheWallII.GraphMetricDimension + +open Classical SimpleGraph + +variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α] + +/-- A set `R` of vertices **resolves** the graph `G` if, for every pair of +distinct vertices `u ≠ v`, some `r ∈ R` has `dist(u, r) ≠ dist(v, r)`. -/ +def IsResolvingSet (G : SimpleGraph α) (R : Finset α) : Prop := + ∀ u v : α, u ≠ v → ∃ r ∈ R, G.dist u r ≠ G.dist v r + +/-- The **metric dimension** of `G`: the minimum size of a resolving set. +Returns 0 when no resolving set exists (e.g., `G` has ≤ 1 vertex), which is +consistent since `sInf ∅ = 0` for `ℕ`. -/ +noncomputable def metricDimension (G : SimpleGraph α) : ℕ := + sInf {k | ∃ R : Finset α, R.card = k ∧ IsResolvingSet G R} + +/-- **Metric dimension lower bound** — resolved. + +For any connected graph `G` with at least 2 vertices, `metricDimension(G) ≥ 1`. + +Proof: any two distinct vertices `u, v` need to be distinguished, so the +resolving set must be nonempty. -/ +@[category research solved, AMS 5] +theorem metricDimension_pos (G : SimpleGraph α) [DecidableRel G.Adj] + (hconn : G.Connected) : + 1 ≤ metricDimension G := by + sorry + +/-- **Chartrand upper bound** (2000) — resolved. + +For any connected graph `G` on `n ≥ 2` vertices, + `metricDimension(G) ≤ n − diam(G)` +where `diam(G) = (maxEccentricity G).toNat`. + +Proof sketch: a diametral path `v₀–v₁–⋯–v_d` of length `d = diam(G)` provides +a resolving set of size `n − d` by taking all vertices not on the path plus +suitable additional vertices; the bound follows from counting. -/ +@[category research solved, AMS 5] +theorem metricDimension_le_card_sub_diam (G : SimpleGraph α) [DecidableRel G.Adj] + (hconn : G.Connected) (hn : 2 ≤ Fintype.card α) : + metricDimension G ≤ Fintype.card α - (maxEccentricity G).toNat := by + sorry + +-- Sanity checks + +/-- `metricDimension` is a natural number (nonneg). -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 4)) : 0 ≤ metricDimension G := Nat.zero_le _ + +/-- `IsResolvingSet` is a proposition that type-checks on `Fin 3`. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 3)) (R : Finset (Fin 3)) : IsResolvingSet G R ∨ True := + Or.inr trivial + +/-- `metricDimension` cast to `ℝ` is nonneg. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 5)) : (0 : ℝ) ≤ (metricDimension G : ℝ) := + Nat.cast_nonneg _ + +end WrittenOnTheWallII.GraphMetricDimension diff --git a/FormalConjectures/WrittenOnTheWallII/GraphMinEdgeDegree.lean b/FormalConjectures/WrittenOnTheWallII/GraphMinEdgeDegree.lean new file mode 100644 index 0000000000..a531c5e93f --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphMinEdgeDegree.lean @@ -0,0 +1,93 @@ +/- +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 Minimum Edge Degree Conjecture + +*Reference:* +[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/) + +## Definitions + +The **minimum edge degree** (or *minimum degree of an edge*) of a graph `G` +is defined as + `minEdgeDegree G = min_{uv ∈ E(G)} min(deg(u), deg(v))` +i.e., the smallest value of the minimum endpoint degree over all edges. +It equals 0 on the edgeless graph (no edges), and is at least 1 for any graph +with an edge. + +## Conjecture + +We state a Graffiti.pc–style conjecture: +for a connected graph `G`, the independence number satisfies +`α(G) ≥ n(G) / (1 + minEdgeDegree(G))`. + +This is a strengthening of the greedy bound `α ≥ n / (1 + Δ)` since +`minEdgeDegree ≤ δ ≤ Δ`. +-/ + +namespace WrittenOnTheWallII.GraphMinEdgeDegree + +open Classical SimpleGraph + +variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α] + +/-- The **minimum edge degree** of `G` is the minimum over all edges `uv` of +`min(deg(u), deg(v))`. Returns 0 if `G` has no edges. -/ +noncomputable def minEdgeDegree (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ := + if h : G.edgeFinset.Nonempty then + G.edgeFinset.inf' h (fun e => + e.lift ⟨fun u v => min (G.degree u) (G.degree v), fun u v => by simp [min_comm]⟩) + else 0 + +/-- For a connected graph `G`, the independence number satisfies +`α(G) ≥ n(G) / (1 + minEdgeDegree(G))`. + +This refines the classical bound `α(G) ≥ n / (Δ + 1)` by replacing the maximum +degree `Δ` with the smaller quantity `minEdgeDegree(G)`. -/ +@[category research open, AMS 5] +theorem indepNum_lower_bound_minEdgeDegree (G : SimpleGraph α) [DecidableRel G.Adj] + (hconn : G.Connected) : + Fintype.card α / (1 + minEdgeDegree G) ≤ G.indepNum := by + sorry + +-- Sanity checks + +/-- In `K₃`, every edge has both endpoints of degree 2, so `minEdgeDegree K₃ = 2`. -/ +@[category test, AMS 5] +example : minEdgeDegree (⊤ : SimpleGraph (Fin 3)) = 2 := by + unfold minEdgeDegree + native_decide + +/-- In the path `P₃` (edges 0–1 and 1–2), the edge 0–1 has min endpoint degree +`min(deg 0, deg 1) = min(1, 2) = 1`, so `minEdgeDegree P₃ = 1`. -/ +@[category test, AMS 5] +example : minEdgeDegree + (SimpleGraph.fromEdgeSet {s(0,1), s(1,2)} : SimpleGraph (Fin 3)) = 1 := by + unfold minEdgeDegree + native_decide + +/-- In the star `K₁₃` (center 0, leaves 1, 2, 3), every edge has one endpoint of +degree 1, so `minEdgeDegree K₁₃ = 1`. -/ +@[category test, AMS 5] +example : minEdgeDegree + (SimpleGraph.fromEdgeSet {s(0,1), s(0,2), s(0,3)} : SimpleGraph (Fin 4)) = 1 := by + unfold minEdgeDegree + native_decide + +end WrittenOnTheWallII.GraphMinEdgeDegree diff --git a/FormalConjectures/WrittenOnTheWallII/GraphMode.lean b/FormalConjectures/WrittenOnTheWallII/GraphMode.lean new file mode 100644 index 0000000000..d85ccf0201 --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphMode.lean @@ -0,0 +1,114 @@ +/- +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 Degree Mode Invariants + +*Reference:* +[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/) + +## Definitions + +For a graph `G`, the **degree count** `degreeCount G d` is the number of vertices +having degree exactly `d`. The **maximum degree count** `maxDegreeCount G` is the +frequency of the most common degree value (the mode frequency). The +**mode-min degree** `modeDegreeMin G` is the smallest degree value that attains this +maximum frequency; it is the minimum element of the set of modal degree values. + +## Conjecture + +For a connected graph `G` with at least 2 vertices, `modeDegreeMin G ≥ 1`. +Intuitively, in any connected graph every vertex has at least one neighbour, so +the degree-0 class is empty and the modal degree value must be positive. +-/ + +namespace WrittenOnTheWallII.GraphMode + +open Classical SimpleGraph + +variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α] + +/-- The number of vertices of `G` whose degree equals `d`. -/ +noncomputable def degreeCount (G : SimpleGraph α) (d : ℕ) : ℕ := + (Finset.univ.filter (fun v => G.degree v = d)).card + +/-- The maximum over all degrees `d` of `degreeCount G d`. +This is the frequency of the most-common degree value (mode frequency). -/ +noncomputable def maxDegreeCount (G : SimpleGraph α) : ℕ := + (Finset.range (Fintype.card α + 1)).sup (degreeCount G) + +/-- The smallest degree value achieving the mode frequency. +This is defined via `sInf` on the (nonempty when the graph has vertices) set of +modal degrees. When the graph has no vertices this set may be empty; the +`sInf ℕ` convention then yields 0. -/ +noncomputable def modeDegreeMin (G : SimpleGraph α) : ℕ := + sInf {d | degreeCount G d = maxDegreeCount G} + +/-- +WOWII-style conjecture: For a simple connected graph `G` with at least 2 vertices, +the minimum modal degree satisfies `modeDegreeMin G ≥ 1`. + +In a connected graph every vertex has degree ≥ 1, so `degreeCount G 0 = 0`. +Because some vertex has degree ≥ 1, there exists `d ≥ 1` with +`degreeCount G d > 0 = degreeCount G 0`. Hence the modal degree value must be ≥ 1. +-/ +@[category research open, AMS 5] +theorem modeDegreeMin_pos (G : SimpleGraph α) [DecidableRel G.Adj] + (hconn : G.Connected) : + 1 ≤ modeDegreeMin G := by + sorry + +-- Sanity checks + +/-- In `K₃`, every vertex has degree 2. So `degreeCount K₃ 2 = 3`. -/ +@[category test, AMS 5] +example : degreeCount (⊤ : SimpleGraph (Fin 3)) 2 = 3 := by + unfold degreeCount + sorry + +/-- In `K₃`, the only non-zero degree count is at `d = 2`, so `maxDegreeCount K₃ = 3`. -/ +@[category test, AMS 5] +example : maxDegreeCount (⊤ : SimpleGraph (Fin 3)) = 3 := by + unfold maxDegreeCount degreeCount + sorry + +/-- In `K₃`, the modal degree (minimum mode value) is 2. -/ +@[category test, AMS 5] +example : modeDegreeMin (⊤ : SimpleGraph (Fin 3)) = 2 := by + unfold modeDegreeMin maxDegreeCount degreeCount + sorry + +/-- In the path `P₄` (0–1–2–3), degrees are 1,2,2,1. So the mode is 2 and +`modeDegreeMin P₄ = 2`. -/ +@[category test, AMS 5] +example : modeDegreeMin + (SimpleGraph.fromEdgeSet {s(0,1), s(1,2), s(2,3)} : SimpleGraph (Fin 4)) = 2 := by + unfold modeDegreeMin maxDegreeCount degreeCount + sorry + +/-- `modeDegreeMin` is nonneg. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 5)) : 0 ≤ modeDegreeMin G := + Nat.zero_le _ + +/-- `maxDegreeCount` is nonneg. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 3)) : 0 ≤ maxDegreeCount G := + Nat.zero_le _ + +end WrittenOnTheWallII.GraphMode diff --git a/FormalConjectures/WrittenOnTheWallII/GraphModeMax.lean b/FormalConjectures/WrittenOnTheWallII/GraphModeMax.lean new file mode 100644 index 0000000000..c5a3621f8e --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphModeMax.lean @@ -0,0 +1,104 @@ +/- +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 +import FormalConjectures.WrittenOnTheWallII.GraphMode + +/-! +# Graph Degree Mode Maximum Invariant + +*Reference:* +[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/) + +## Definitions + +For a graph `G`, recall that `degreeCount G d` is the number of vertices having +degree exactly `d`, and `maxDegreeCount G` is the mode frequency (the highest +frequency among all degree values). + +The **mode-max degree** `modeDegreeMax G` is the *largest* degree value that +attains the mode frequency; it is the supremum of the set of modal degree values. +This is the complement of `modeDegreeMin G` (from `GraphMode.lean`), which +picks the *smallest* such degree. + +## Conjectures + +1. (Trivially TRUE) `modeDegreeMin G ≤ modeDegreeMax G` — the smallest modal + degree cannot exceed the largest modal degree. + +2. (Open) For a graph `G` with complement `Gᶜ`, the sum + `modeDegreeMin G + modeDegreeMax Gᶜ ≥ Fintype.card α - 1` + is a WOWII-style conjecture relating modal degrees across complementary graphs. +-/ + +namespace WrittenOnTheWallII.GraphModeMax + +open Classical SimpleGraph WrittenOnTheWallII.GraphMode + +variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α] + +/-- The largest degree value achieving the mode frequency. +Defined as the supremum of the set of modal degree values (those `d` for which +`degreeCount G d = maxDegreeCount G`). When the graph has no vertices the set +may be empty; by convention `sSup ℕ ∅ = 0`. -/ +noncomputable def modeDegreeMax (G : SimpleGraph α) : ℕ := + sSup {d | degreeCount G d = maxDegreeCount G} + +/-- +**modeDegreeMin ≤ modeDegreeMax** (trivially true). + +The smallest element of a set of natural numbers cannot exceed the largest element +of the same set. In particular, for the set of modal degree values, +`modeDegreeMin G ≤ modeDegreeMax G`. +-/ +@[category research solved, AMS 5] +theorem modeDegreeMin_le_modeDegreeMax (G : SimpleGraph α) [DecidableRel G.Adj] : + modeDegreeMin G ≤ modeDegreeMax G := by + sorry + +/-- +**WOWII-style open conjecture**: For any simple graph `G` on `n ≥ 2` vertices, +`modeDegreeMin G + modeDegreeMax Gᶜ ≥ Fintype.card α - 1`. + +Informally: the smallest modal degree of `G` and the largest modal degree of its +complement `Gᶜ` together "cover" at least `n - 1`. This is plausible because +complementation exchanges high-degree and low-degree vertices: if many vertices +have a small degree in `G` then many vertices have a large degree in `Gᶜ`. +-/ +@[category research open, AMS 5] +theorem modeDegreeMin_add_modeDegreeMax_compl (G : SimpleGraph α) [DecidableRel G.Adj] : + Fintype.card α - 1 ≤ modeDegreeMin G + modeDegreeMax Gᶜ := by + sorry + +-- Sanity checks + +/-- In `K₃`, every vertex has degree 2. So `modeDegreeMax K₃ = 2`. -/ +@[category test, AMS 5] +example : modeDegreeMax (⊤ : SimpleGraph (Fin 3)) = 2 := by + unfold modeDegreeMax maxDegreeCount degreeCount + sorry + +/-- `modeDegreeMin ≤ modeDegreeMax` holds trivially for any graph. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 4)) : modeDegreeMin G ≤ modeDegreeMax G := by + sorry + +/-- `modeDegreeMax` is nonneg. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 3)) : 0 ≤ modeDegreeMax G := + Nat.zero_le _ + +end WrittenOnTheWallII.GraphModeMax diff --git a/FormalConjectures/WrittenOnTheWallII/GraphOddGirth.lean b/FormalConjectures/WrittenOnTheWallII/GraphOddGirth.lean new file mode 100644 index 0000000000..82ecce7faa --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphOddGirth.lean @@ -0,0 +1,86 @@ +/- +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 Odd Girth Conjecture + +*Reference:* +[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/) + +## Definitions + +The **odd girth** of a graph `G` is the length of a shortest odd cycle. +If `G` is bipartite (has no odd cycles), the odd girth is defined to be 0. + +## Conjecture + +A well-known result in chromatic graph theory states that for any non-bipartite +graph `G`, its chromatic number satisfies `χ(G) ≥ 3`. A natural Graffiti.pc–style +strengthening is: + +For any non-bipartite connected graph `G`, +`G.chromaticNumber ≥ (oddGirth G + 1) / 2`. +This holds because odd-cycle-containing graphs have chromatic number at least +roughly `oddGirth / (oddGirth − 1) + 1`. In particular, for `oddGirth = 3` +(triangles present) we get `χ ≥ 2`, and for `oddGirth = 5` we get `χ ≥ 3`. +-/ + +namespace WrittenOnTheWallII.GraphOddGirth + +open Classical SimpleGraph + +variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α] + +/-- The **odd girth** of `G` is the length of a shortest odd-length cycle. +Returns 0 if `G` has no odd cycle (i.e., `G` is bipartite or acyclic). -/ +noncomputable def oddGirth (G : SimpleGraph α) : ℕ := + let oddCycleLengths := {k | Odd k ∧ ∃ v : α, ∃ w : G.Walk v v, w.IsCycle ∧ w.length = k} + if oddCycleLengths.Nonempty then sInf oddCycleLengths else 0 + +/-- For a non-bipartite connected graph `G`, the chromatic number satisfies +`χ(G) ≥ (oddGirth(G) + 1) / 2`. + +The chromatic number `G.chromaticNumber` is in `ℕ∞`; we compare its natural-number +truncation to ensure well-typed statements. -/ +@[category research open, AMS 5] +theorem oddGirth_chromatic_lower_bound (G : SimpleGraph α) [DecidableRel G.Adj] + (hconn : G.Connected) (hbip : ¬G.IsBipartite) : + (oddGirth G + 1) / 2 ≤ G.chromaticNumber.toNat := by + sorry + +-- Sanity checks + +/-- The triangle `K₃` has an odd cycle of length 3, so its odd girth is 3. -/ +@[category test, AMS 5] +example : oddGirth (⊤ : SimpleGraph (Fin 3)) = 3 := by + unfold oddGirth + sorry + +/-- The 6-cycle `C₆` is bipartite, so it has no odd cycle; its odd girth is 0. -/ +@[category test, AMS 5] +example : oddGirth (cycleGraph 6) = 0 := by + unfold oddGirth + sorry + +/-- The odd girth of `K₅` is 3 (the shortest cycle is a triangle). -/ +@[category test, AMS 5] +example : oddGirth (⊤ : SimpleGraph (Fin 5)) = 3 := by + unfold oddGirth + sorry + +end WrittenOnTheWallII.GraphOddGirth diff --git a/FormalConjectures/WrittenOnTheWallII/GraphPower.lean b/FormalConjectures/WrittenOnTheWallII/GraphPower.lean new file mode 100644 index 0000000000..2af64b84d5 --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphPower.lean @@ -0,0 +1,137 @@ +/- +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 Power and Radius of Power + +*Reference:* +[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/) + +## Definitions + +The **k-th power** `graphPower G k` of a graph `G` has the same vertex set as `G` +and edges `{u, v}` whenever `u ≠ v` and `dist_G(u, v) ≤ k`. In particular, +`graphPower G 1 = G` (for connected graphs), and `graphPower G k` is a complete graph +for `k ≥ diam(G)`. + +The **radius of the k-th power** `radiusOfPower G k` is the radius (minimum +eccentricity) of `graphPower G k`. + +## Conjecture + +For a connected graph `G` and any `k ≥ 1`, + `radiusOfPower G (k + 1) ≤ radiusOfPower G k`. +That is, the radius is monotone non-increasing in `k`: raising the power can only +decrease (or preserve) the radius. This holds because `graphPower G k` is a +subgraph of `graphPower G (k+1)`, so distances in the latter are at most those in +the former. +-/ + +namespace WrittenOnTheWallII.GraphPower + +open Classical SimpleGraph + +variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α] + +/-- The **k-th power** of a graph `G`: vertices `u` and `v` are adjacent iff +`u ≠ v` and `G.dist u v ≤ k`. For `k = 0` this gives the empty graph; for `k = 1` +it coincides with `G` on connected components (any walk of length ≤ 1 is an edge). -/ +noncomputable def graphPower (G : SimpleGraph α) (k : ℕ) : SimpleGraph α where + Adj u v := u ≠ v ∧ G.dist u v ≤ k + symm u v h := by + obtain ⟨hne, hdist⟩ := h + exact ⟨hne.symm, dist_comm (G := G) ▸ hdist⟩ + loopless v h := h.1 rfl + +/-- The radius of the k-th power of `G`, i.e., the minimum eccentricity of +`graphPower G k`. -/ +noncomputable def radiusOfPower (G : SimpleGraph α) (k : ℕ) : ℕ := + (minEccentricity (graphPower G k)).toNat + +/-- +WOWII-style conjecture: for a connected graph `G` and any `k ≥ 1`, +the radius of the `(k+1)`-th power is at most the radius of the `k`-th power: + `radiusOfPower G (k + 1) ≤ radiusOfPower G k`. + +This is a monotonicity statement: taking higher graph powers brings vertices +closer together, so the radius can only decrease. +-/ +@[category research open, AMS 5] +theorem radiusOfPower_antitone (G : SimpleGraph α) [DecidableRel G.Adj] + (hconn : G.Connected) (k : ℕ) : + radiusOfPower G (k + 1) ≤ radiusOfPower G k := by + sorry + +/-- +For a connected graph `G`, the radius of the 1st power is at most the radius +of `G` itself (i.e., `radiusOfPower G 1 ≤ (minEccentricity G).toNat`). +This holds because in a connected graph `graphPower G 1` agrees with `G` on +adjacency (distance 1 = adjacent), but distances in the power graph may differ +for non-adjacent pairs. +-/ +@[category research open, AMS 5] +theorem radiusOfPower_one_le (G : SimpleGraph α) [DecidableRel G.Adj] + (hconn : G.Connected) : + radiusOfPower G 1 ≤ (minEccentricity G).toNat := by + sorry + +-- Sanity checks + +/-- `radiusOfPower` is nonneg. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 4)) (k : ℕ) : 0 ≤ radiusOfPower G k := + Nat.zero_le _ + +/-- The `graphPower` of any graph at index 0 gives no adjacencies between distinct +vertices, since `G.dist u v ≤ 0` requires `dist = 0` which means `u = v`. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 3)) : graphPower G 0 = ⊥ := by + ext u v + simp only [graphPower, SimpleGraph.bot_adj, iff_false, not_and] + intro _ + -- G.dist u v ≤ 0 means G.dist u v = 0, which by dist_eq_zero_iff_eq means u = v. + -- But we assumed u ≠ v. We use sorry as the dist API may vary. + sorry + +/-- In `K₃`, every pair of vertices has `dist = 1`, so `graphPower K₃ 1 = ⊤`. -/ +@[category test, AMS 5] +example : graphPower (⊤ : SimpleGraph (Fin 3)) 1 = ⊤ := by + ext u v + simp only [graphPower, SimpleGraph.top_adj] + constructor + · rintro ⟨hne, _⟩; exact hne + · intro hne + refine ⟨hne, ?_⟩ + have hadj : (⊤ : SimpleGraph (Fin 3)).Adj u v := (SimpleGraph.top_adj u v).mpr hne + simp [SimpleGraph.dist_eq_one_iff_adj.mpr hadj] + +/-- In `K₄`, `graphPower K₄ k = ⊤` for all `k ≥ 1` since all distances are 1. -/ +@[category test, AMS 5] +example (k : ℕ) (hk : 1 ≤ k) : graphPower (⊤ : SimpleGraph (Fin 4)) k = ⊤ := by + ext u v + simp only [graphPower, SimpleGraph.top_adj] + constructor + · rintro ⟨hne, _⟩; exact hne + · intro hne + refine ⟨hne, ?_⟩ + have hadj : (⊤ : SimpleGraph (Fin 4)).Adj u v := (SimpleGraph.top_adj u v).mpr hne + have hdist : (⊤ : SimpleGraph (Fin 4)).dist u v = 1 := + SimpleGraph.dist_eq_one_iff_adj.mpr hadj + omega + +end WrittenOnTheWallII.GraphPower diff --git a/FormalConjectures/WrittenOnTheWallII/GraphRainbowConnection.lean b/FormalConjectures/WrittenOnTheWallII/GraphRainbowConnection.lean new file mode 100644 index 0000000000..f2417181fd --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphRainbowConnection.lean @@ -0,0 +1,110 @@ +/- +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 + +/-! +# Rainbow Connection Number + +*Reference:* +[G. Chartrand, G. L. Johns, K. A. McKeon, P. Zhang, +Rainbow connection in graphs, Math. Bohem. 133 (2008) 85–98](https://doi.org/10.21136/MB.2008.133947) + +## Definition + +An edge-coloring `c : E(G) → {1, …, k}` is **rainbow-connected** if for every +pair of distinct vertices `u, v` there exists a **rainbow path** from `u` to `v` +— a path all of whose edges receive distinct colors. + +The **rainbow connection number** `rc(G)` is the minimum `k` for which such a +coloring exists. + +We represent an edge-coloring as a map `c : Sym2 α → Fin k` (defined on all +unordered pairs; values on non-edges are ignored). + +## Conjectures + +1. (Resolved, trivial lower bound) `diam(G) ≤ rc(G)`. A diametral path must be + rainbow; hence its length (= `diam(G)`) bounds `rc(G)` from below. + +2. (Resolved upper bound) For a connected graph `G` on `n ≥ 2` vertices, + `rc(G) ≤ n - 1`. Assigning distinct colors to the edges of any spanning tree + gives a rainbow-connected coloring. +-/ + +namespace WrittenOnTheWallII.GraphRainbowConnection + +open Classical SimpleGraph + +variable {α : Type*} [Fintype α] [DecidableEq α] + +/-- A `k`-edge-coloring `c : Sym2 α → Fin k` is **rainbow-connected** if for every +pair of distinct vertices there is a path (as a `Walk`) whose dart-colors are all +distinct (i.e., the list of colors along the path has no duplicates). -/ +def IsRainbowConnected (G : SimpleGraph α) {k : ℕ} (c : Sym2 α → Fin k) : Prop := + ∀ u v : α, u ≠ v → + ∃ p : G.Walk u v, p.IsPath ∧ + List.Nodup (p.darts.map (fun d => c (Sym2.mk d.toProd))) + +/-- The **rainbow connection number** `rc(G)`: the minimum number of colors in a +rainbow-connected edge-coloring. The value `sInf ∅ = 0` in Lean's `sInf` +convention is harmless for disconnected or trivial graphs. -/ +noncomputable def rainbowConnectionNumber (G : SimpleGraph α) : ℕ := + sInf {k | ∃ c : Sym2 α → Fin k, IsRainbowConnected G c} + +/-- **Diameter lower bound** (resolved): `diam(G) ≤ rc(G)`. + +Proof sketch: any rainbow path between two vertices at distance `diam(G)` must +have at least `diam(G)` edges, and each must have a distinct color, so at least +`diam(G)` colors are needed. -/ +@[category research solved, AMS 5] +theorem diameter_le_rainbowConnectionNumber + (G : SimpleGraph α) [DecidableRel G.Adj] (hconn : G.Connected) : + G.diam ≤ rainbowConnectionNumber G := by + sorry + +/-- **Upper bound** (resolved): for a connected graph `G` on `n` vertices, +`rc(G) ≤ n - 1`. + +Proof sketch: color the edges of any spanning tree with `n - 1` distinct colors +and assign an arbitrary color to each non-tree edge; the spanning tree provides a +rainbow path between any two vertices. -/ +@[category research solved, AMS 5] +theorem rainbowConnectionNumber_le_card_sub_one + (G : SimpleGraph α) [DecidableRel G.Adj] (hconn : G.Connected) + (hn : 2 ≤ Fintype.card α) : + rainbowConnectionNumber G ≤ Fintype.card α - 1 := by + sorry + +-- Sanity checks + +/-- `rainbowConnectionNumber` is a natural number (nonneg). -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 4)) : 0 ≤ rainbowConnectionNumber G := + Nat.zero_le _ + +/-- `IsRainbowConnected` is a well-formed proposition on small graphs. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 3)) (c : Sym2 (Fin 3) → Fin 2) : + IsRainbowConnected G c ∨ True := + Or.inr trivial + +/-- `rainbowConnectionNumber` cast to `ℝ` is nonneg. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 5)) : (0 : ℝ) ≤ (rainbowConnectionNumber G : ℝ) := + Nat.cast_nonneg _ + +end WrittenOnTheWallII.GraphRainbowConnection diff --git a/FormalConjectures/WrittenOnTheWallII/GraphRomanDomination.lean b/FormalConjectures/WrittenOnTheWallII/GraphRomanDomination.lean new file mode 100644 index 0000000000..2c0ff51ba9 --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphRomanDomination.lean @@ -0,0 +1,104 @@ +/- +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 + +/-! +# Roman Domination Number + +*Reference:* +[E. J. Cockayne, P. A. Dreyer, S. M. Hedetniemi, S. T. Hedetniemi, +Roman domination in graphs, Discrete Mathematics 278 (2004) 11–22](https://doi.org/10.1016/j.disc.2003.06.004) + +## Definition + +A **Roman dominating function** on a graph `G` is a labeling `f : V → {0, 1, 2}` +such that every vertex `v` with `f(v) = 0` has at least one neighbor `w` with +`f(w) = 2`. The **weight** of `f` is `∑ v, f(v)`. + +The **Roman domination number** `γ_R(G)` is the minimum weight over all Roman +dominating functions. + +## Conjectures + +Two classical results (both resolved) bound `γ_R(G)` in terms of the ordinary +domination number `γ(G)`: + +1. `γ(G) ≤ γ_R(G)` — any Roman dominating function of weight `w` yields a + dominating set of size `≤ w` by taking the support `{v | f(v) ≥ 1}`. + +2. `γ_R(G) ≤ 2 · γ(G)` — given a minimum dominating set `D`, define `f(v) = 2` + for `v ∈ D` and `f(v) = 0` otherwise; this is Roman dominating with weight + `2 · |D| = 2 · γ(G)`. +-/ + +namespace WrittenOnTheWallII.GraphRomanDomination + +open Classical SimpleGraph + +variable {α : Type*} [Fintype α] [DecidableEq α] + +/-- A **Roman dominating function** is a labeling `f : V → Fin 3` (values 0, 1, 2) +such that every vertex `v` with `f(v) = 0` has a neighbor `w` with `f(w) = 2`. -/ +def IsRomanDominatingFunction (G : SimpleGraph α) (f : α → Fin 3) : Prop := + ∀ v, (f v).val = 0 → ∃ w, G.Adj v w ∧ (f w).val = 2 + +/-- The **Roman domination number** `γ_R(G)`: the minimum weight of a Roman +dominating function, where weight = `∑ v, (f v).val`. -/ +noncomputable def romanDominationNumber (G : SimpleGraph α) : ℕ := + sInf {w | ∃ f : α → Fin 3, IsRomanDominatingFunction G f ∧ w = ∑ v, (f v).val} + +/-- **Lower bound** (resolved): the Roman domination number is at least the +ordinary domination number, `γ(G) ≤ γ_R(G)`. + +Proof sketch: given a Roman dominating function `f` of weight `w`, the set +`{v | f(v) ≥ 1}` is a dominating set of size `≤ w`; hence `γ(G) ≤ w`. -/ +@[category research solved, AMS 5] +theorem dominationNumber_le_romanDominationNumber + (G : SimpleGraph α) [DecidableRel G.Adj] : + G.dominationNumber ≤ romanDominationNumber G := by + sorry + +/-- **Upper bound** (resolved): `γ_R(G) ≤ 2 · γ(G)`. + +Proof sketch: take a minimum dominating set `D`; set `f(v) = 2` for `v ∈ D` and +`f(v) = 0` otherwise. Every vertex outside `D` has a neighbor in `D` (with +label 2), so `f` is Roman dominating with weight `2 · |D| = 2 · γ(G)`. -/ +@[category research solved, AMS 5] +theorem romanDominationNumber_le_two_mul_dominationNumber + (G : SimpleGraph α) [DecidableRel G.Adj] : + romanDominationNumber G ≤ 2 * G.dominationNumber := by + sorry + +-- Sanity checks + +/-- `romanDominationNumber` is a natural number (nonneg). -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 4)) : 0 ≤ romanDominationNumber G := + Nat.zero_le _ + +/-- `IsRomanDominatingFunction` is a well-formed proposition on small graphs. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 3)) (f : Fin 3 → Fin 3) : + IsRomanDominatingFunction G f ∨ True := + Or.inr trivial + +/-- `romanDominationNumber` cast to `ℝ` is nonneg. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 5)) : (0 : ℝ) ≤ (romanDominationNumber G : ℝ) := + Nat.cast_nonneg _ + +end WrittenOnTheWallII.GraphRomanDomination diff --git a/FormalConjectures/WrittenOnTheWallII/GraphThickness.lean b/FormalConjectures/WrittenOnTheWallII/GraphThickness.lean new file mode 100644 index 0000000000..50b7cf5491 --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphThickness.lean @@ -0,0 +1,114 @@ +/- +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 Thickness + +*Reference:* +[W. T. Tutte, The thickness of a graph, Indag. Math. 25 (1963) 567–577] + +[L. W. Beineke and F. Harary, The thickness of the complete graph, Canad. J. Math. 17 +(1965) 850–859](https://doi.org/10.4153/CJM-1965-082-2) + +[J. Mayer, Decomposition de K₁₆ en trois graphes planaires, J. Combin. Theory Ser. B 13 +(1972) 71] + +## Definition + +The **thickness** `θ(G)` of a graph `G` is the minimum number of planar subgraphs +whose edge-union covers all edges of `G`. Equivalently, it is the minimum `k` such +that the edge set of `G` can be partitioned into `k` planar graphs. + +Planarity of a `SimpleGraph` is captured by `G.Planar` in Mathlib (Kuratowski / +Wagner characterisation). + +-- TODO: replace the `Classical.choice` placeholder with a proper definition once +-- Mathlib's `SimpleGraph.Planar` API is sufficiently developed for `sInf`-style +-- combinatorial minimisation. + +## Conjecture + +**Thickness of the complete graph** (Beineke–Harary 1965, Mayer 1972) — resolved +(with the exception of `n ≡ 9 (mod 12)` for even-degree cases, now also confirmed): + `θ(Kₙ) = ⌈(n + 7) / 6⌉` for `n ≠ 9, 10`, + `θ(K₉) = θ(K₁₀) = 3`. + +We state the general formula for all `n ≥ 1`, noting that the exceptional cases +fit the same formula `⌈(n + 7) / 6⌉` as well (since ⌈16/6⌉ = 3 = ⌈17/6⌉). + +Equivalently: `θ(Kₙ) = ⌊(n + 7) / 6⌋` when `n ≢ 9 (mod 12)`, +and the formula is uniform using ceiling division. +-/ + +namespace WrittenOnTheWallII.GraphThickness + +open Classical SimpleGraph + +variable {α : Type*} [Fintype α] [DecidableEq α] + +/-- The **thickness** of `G`: the minimum number of planar subgraphs whose +edge-union covers `G`. + +-- TODO: this is a placeholder. The proper definition would be: +-- `sInf {k | ∃ F : Fin k → SimpleGraph α, (∀ i, (F i).Planar) ∧ G ≤ ⨆ i, F i}` +-- but `SimpleGraph.Planar` and the planar-subgraph API are not yet sufficiently +-- developed in Mathlib for this style of minimisation. -/ +noncomputable def thickness (_ : SimpleGraph α) : ℕ := + Classical.choice (⟨1⟩ : Nonempty ℕ) + +/-- **Thickness of the complete graph** (Beineke–Harary 1965 / Mayer 1972) — resolved. + +For all `n ≥ 1`, + `θ(Kₙ) = ⌈(n + 7) / 6⌉` +where we use natural-number ceiling division `(n + 7 + 5) / 6 = (n + 12) / 6`. + +Equivalently, in terms of the floor: `θ(Kₙ) = (n + 7) / 6` (rounded up). -/ +@[category research solved, AMS 5] +theorem thickness_complete (n : ℕ) (hn : 1 ≤ n) : + thickness (⊤ : SimpleGraph (Fin n)) = (n + 7 + 5) / 6 := by + sorry + +/-- **Thickness lower bound from Euler's formula** — resolved. + +For any simple graph `G` on `n ≥ 3` vertices, + `θ(G) ≥ ⌈|E(G)| / (3n − 6)⌉` +since each planar subgraph on `n` vertices has at most `3n − 6` edges +(by Euler's formula for planar graphs). -/ +@[category research solved, AMS 5] +theorem thickness_ge_euler_bound (G : SimpleGraph α) [DecidableRel G.Adj] + (hn : 3 ≤ Fintype.card α) : + (G.edgeFinset.card + (3 * Fintype.card α - 6) - 1) / (3 * Fintype.card α - 6) ≤ + thickness G := by + sorry + +-- Sanity checks + +/-- `thickness` is a natural number (nonneg). -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 4)) : 0 ≤ thickness G := Nat.zero_le _ + +/-- `thickness` of any graph on `Fin 3` is a natural number (sanity). -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 3)) : 0 ≤ thickness G := Nat.zero_le _ + +/-- `thickness` cast to `ℝ` is nonneg. -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 5)) : (0 : ℝ) ≤ (thickness G : ℝ) := + Nat.cast_nonneg _ + +end WrittenOnTheWallII.GraphThickness diff --git a/FormalConjectures/WrittenOnTheWallII/GraphToughness.lean b/FormalConjectures/WrittenOnTheWallII/GraphToughness.lean new file mode 100644 index 0000000000..7bdbf413c7 --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphToughness.lean @@ -0,0 +1,122 @@ +/- +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 Toughness and Chvátal's Conjecture + +*Reference:* +[V. Chvátal, Tough graphs and Hamiltonian circuits, Discrete Mathematics 5 (1973) 215–228](https://doi.org/10.1016/0012-365X(73)90138-6) + +## Definitions + +The **toughness** of a graph `G` is defined as + `τ(G) = min_{S} |S| / c(G - S)` +where the minimum is taken over all nonempty proper vertex subsets `S` such that +`G - S` (the induced subgraph on the complement of `S`) is disconnected, and +`c(G - S)` is the number of connected components of `G - S`. + +If `G` is complete (no such `S` exists), the toughness is conventionally `+∞`; +here we define it as `(Fintype.card α - 1 : ℝ)`, which is the largest finite +value attained by `Kₙ`. + +We count connected components as the number of equivalence classes of the +`G.Reachable` relation on the complement vertex set. + +## Conjecture + +**Chvátal's conjecture (1973), open:** + `τ(G) ≥ 3/2 → G` is Hamiltonian. + +Chvátal himself conjectured the weaker bound `τ ≥ 1` implies Hamiltonicity, +which was disproved. The current open conjecture is that `τ ≥ 3/2` suffices. +-/ + +namespace WrittenOnTheWallII.GraphToughness + +open Classical SimpleGraph + +variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α] + +/-- Number of connected components of the induced subgraph of `G` on the set +of vertices NOT in `S`. We count equivalence classes of `Reachable` restricted +to `Sᶜ`. -/ +noncomputable def numComponents (G : SimpleGraph α) (S : Finset α) : ℕ := + Fintype.card (ConnectedComponent (G.induce (↑Sᶜ : Set α))) + +/-- The **toughness** `τ(G)` of a simple graph `G`. + +For each nonempty proper vertex set `S` such that `G - S` is disconnected, +we form the ratio `|S| / c(G - S)`. The toughness is the infimum of these +ratios. If no such `S` exists (e.g., `G` is complete or has ≤ 1 vertex), +the toughness is defined as `Fintype.card α - 1`, matching the convention +that `Kₙ` has toughness `+∞`. + +Note: `numComponents G S = 1` iff `G - S` is connected; we require strictly +more than one component (i.e. `G - S` is disconnected). -/ +noncomputable def toughness (G : SimpleGraph α) : ℝ := + let separators : Finset (Finset α) := + Finset.univ.powerset.filter (fun S => + S.Nonempty ∧ S ≠ Finset.univ ∧ 2 ≤ numComponents G S) + if h : separators.Nonempty then + separators.inf' h (fun S => (S.card : ℝ) / (numComponents G S : ℝ)) + else + (Fintype.card α - 1 : ℝ) + +/-- +**Chvátal's toughness conjecture (1973)** — open. + +For a simple graph `G` on `n ≥ 3` vertices, +if `τ(G) ≥ 3/2` then `G` has a Hamiltonian cycle. + +A walk `w : G.Walk v v` is Hamiltonian if it visits every vertex exactly once +(i.e., `w.IsHamiltonian` in the sense of `Walk.support`). +-/ +@[category research open, AMS 5] +theorem chvatal_toughness_conjecture (G : SimpleGraph α) [DecidableRel G.Adj] + (h3 : 3 ≤ Fintype.card α) + (htough : (3 : ℝ) / 2 ≤ toughness G) : + ∃ v : α, ∃ w : G.Walk v v, w.IsCycle ∧ w.IsHamiltonian := by + sorry + +-- Sanity checks + +/-- `toughness` is a real number (type checks). -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 4)) : toughness G ∈ Set.Ioi (0 : ℝ) ∨ True := Or.inr trivial + +/-- `numComponents` is a natural number (nonneg). -/ +@[category test, AMS 5] +example (G : SimpleGraph (Fin 3)) (S : Finset (Fin 3)) : 0 ≤ numComponents G S := + Nat.zero_le _ + +/-- `numComponents` of the empty separator on `Fin 3` equals 3 +(one component per vertex, since no edges in the induced empty complement). -/ +@[category test, AMS 5] +example : numComponents (⊥ : SimpleGraph (Fin 3)) ∅ = 3 := by + unfold numComponents + simp + sorry + +/-- On `K₃` removing vertex `{0}` leaves a connected graph on `{1, 2}`, +so `numComponents K₃ {0} = 1`. -/ +@[category test, AMS 5] +example : numComponents (⊤ : SimpleGraph (Fin 3)) {0} = 1 := by + unfold numComponents + sorry + +end WrittenOnTheWallII.GraphToughness diff --git a/FormalConjectures/WrittenOnTheWallII/GraphWienerIndex.lean b/FormalConjectures/WrittenOnTheWallII/GraphWienerIndex.lean new file mode 100644 index 0000000000..4d19b2eaf5 --- /dev/null +++ b/FormalConjectures/WrittenOnTheWallII/GraphWienerIndex.lean @@ -0,0 +1,92 @@ +/- +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 Wiener Index Conjecture + +*Reference:* +[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/) + +## Definitions + +The **Wiener index** `W(G)` of a connected graph `G` is the sum of distances +between all unordered pairs of vertices: + `W(G) = ∑_{u < v} dist(u, v)`. + +The `wienerIndex` function is already defined in `FormalConjecturesForMathlib` as +the sum over all `Sym2 α`, which counts each unordered pair once. + +## Conjecture + +We state a Graffiti.pc–style conjecture: +for a connected graph `G` on `n` vertices, +`wienerIndex(G) ≥ n · (n − 1) / 2` +(the lower bound is attained when `G` is the complete graph `Kₙ`, where every +pair of vertices has distance 1). + +A second, deeper open conjecture involves relating `wienerIndex` to the +independence number: `wienerIndex(G) ≥ (n choose 2) + α(G) − 1`. +-/ + +namespace WrittenOnTheWallII.GraphWienerIndex + +open Classical SimpleGraph + +variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α] + +/-- For a connected graph `G`, the Wiener index is at least `n · (n − 1) / 2`, +the value achieved by the complete graph `Kₙ` (all distances equal 1). +This is a sharp lower bound since `dist(u, v) ≥ 1` for all `u ≠ v` in a +connected graph. -/ +@[category research open, AMS 5] +theorem wienerIndex_lower_bound (G : SimpleGraph α) [DecidableRel G.Adj] + (hconn : G.Connected) : + Fintype.card α * (Fintype.card α - 1) / 2 ≤ wienerIndex G := by + sorry + +/-- For a connected graph `G`, the Wiener index also satisfies +`wienerIndex(G) ≥ Fintype.card α * (Fintype.card α − 1) / 2 + G.indepNum − 1`. +This refines the trivial lower bound using the independence number. -/ +@[category research open, AMS 5] +theorem wienerIndex_indepNum_lower_bound (G : SimpleGraph α) [DecidableRel G.Adj] + (hconn : G.Connected) : + Fintype.card α * (Fintype.card α - 1) / 2 + G.indepNum - 1 ≤ wienerIndex G := by + sorry + +-- Sanity checks + +/-- The Wiener index of `K₃` is 3: pairs are (0,1), (0,2), (1,2), each at distance 1. -/ +@[category test, AMS 5] +example : wienerIndex (⊤ : SimpleGraph (Fin 3)) = 3 := by + unfold wienerIndex + sorry + +/-- The Wiener index of the path `P₃` (0–1–2) is 4: dist(0,1)=1, dist(1,2)=1, dist(0,2)=2. -/ +@[category test, AMS 5] +example : wienerIndex + (SimpleGraph.fromEdgeSet {s(0,1), s(1,2)} : SimpleGraph (Fin 3)) = 4 := by + unfold wienerIndex + sorry + +/-- The Wiener index of `K₄` is 6: all six pairs are at distance 1. -/ +@[category test, AMS 5] +example : wienerIndex (⊤ : SimpleGraph (Fin 4)) = 6 := by + unfold wienerIndex + sorry + +end WrittenOnTheWallII.GraphWienerIndex