/-
Copyright 2026 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 FormalConjecturesUtilWritten on the Wall II - Conjecture 160
Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc
Definitions
For a vertex $v$ in $G$, $T(v)$ is the number of triangles incident to $v$: $$T(v) = |{{u, w} \subseteq N(v) \mid u \sim w}|$$ i.e., the number of pairs of neighbors of $v$ that are themselves adjacent.
The invariant maxTrianglesAtVertex G is the maximum of $T(v)$ over all vertices.
Conjecture 160 uses both $\max_v T(v)$ and $\chi_{C_4}(G)$, the $C_4$-free
characteristic function: it is 1 when $G$ contains no cycle of length four
and 0 otherwise. The cycle need not be induced. These invariants lower-bound
the WOWII invariant $L_s(G)$, the maximum number of leaves over all spanning
trees of $G$ (exposed as SimpleGraph.Ls G : ℝ).
The earlier formalization used the number of induced four-cycles. The historical conjecture instead uses this binary $C_4$-free indicator.
namespace WrittenOnTheWallII.GraphConjecture160open SimpleGraphvariable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]The maximum number of triangles incident to any vertex in $G$.
noncomputable def maxTrianglesAtVertex (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=
(Finset.univ.image (numTrianglesAtVertex G)).max' (Finset.image_nonempty.mpr Finset.univ_nonempty)open scoped Classical inWOWII Conjecture 160
For a simple connected graph $G$, $L_s(G) \ge \max_v l(v) + \max_v T(v) \cdot \chi_{C_4}(G)$ where:
$L_s(G) = \mathrm{SimpleGraph.Ls}, G$ is the maximum number of leaves over all spanning trees of $G$,
$\max_v l(v)$ is the maximum local independence number over vertices,
$\max_v T(v)$ is the maximum number of triangles incident to any vertex,
$\chi_{C_4}(G)$ is 1 if $G$ has no cycle of length four and 0 otherwise.
@[category research open, AMS 5]
theorem conjecture160 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :
let maxL := (Finset.univ.image (indepNeighborsCard G)).max' (α:Type u_1inst✝³:Fintype αinst✝²:DecidableEq αinst✝¹:Nontrivial αG:SimpleGraph αinst✝:DecidableRel G.Adjh:G.Connected⊢ (Finset.image G.indepNeighborsCard Finset.univ).Nonempty All goals completed! 🐙)
let maxT := maxTrianglesAtVertex G
let cC4 : ℕ := if ∃ v : α, ∃ c : G.Walk v v, c.IsCycle ∧ c.length = 4 then 0 else 1
(maxL : ℝ) + (maxT : ℝ) * (cC4 : ℝ) ≤ Ls G := α:Type u_1inst✝³:Fintype αinst✝²:DecidableEq αinst✝¹:Nontrivial αG:SimpleGraph αinst✝:DecidableRel G.Adjh:G.Connected⊢ let maxL := (Finset.image G.indepNeighborsCard Finset.univ).max' ⋯;
let maxT := maxTrianglesAtVertex G;
let cC4 := if ∃ v c, c.IsCycle ∧ c.length = 4 then 0 else 1;
↑maxL + ↑maxT * ↑cC4 ≤ G.Ls
All goals completed! 🐙-- Sanity checks
In $K_3$, every vertex has $1$ triangle incident to it.
@[category test, AMS 5]
example : numTrianglesAtVertex (⊤ : SimpleGraph (Fin 3)) (0 : Fin 3) = 1 := α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αinst✝:Nontrivial α⊢ ⊤.numTrianglesAtVertex 0 = 1
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αinst✝:Nontrivial α⊢ {s ∈ ⊤.cliqueFinset 3 | 0 ∈ s}.card = 1
All goals completed! 🐙
In $K_3$, maxTrianglesAtVertex = 1.
@[category test, AMS 5]
example : maxTrianglesAtVertex (⊤ : SimpleGraph (Fin 3)) = 1 := α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αinst✝:Nontrivial α⊢ maxTrianglesAtVertex ⊤ = 1
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αinst✝:Nontrivial α⊢ (Finset.image (fun v ↦ {s ∈ ⊤.cliqueFinset 3 | v ∈ s}.card) Finset.univ).max' ⋯ = 1
All goals completed! 🐙In the path $P_3$, vertex $1$ is adjacent to $0$ and $2$, but $0$ and $2$ are not adjacent. So $T(1) = 0$.
@[category test, AMS 5]
example : numTrianglesAtVertex
(SimpleGraph.fromEdgeSet {s(0,1), s(1,2)} : SimpleGraph (Fin 3)) (1 : Fin 3) = 0 := α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αinst✝:Nontrivial α⊢ (fromEdgeSet {s(0, 1), s(1, 2)}).numTrianglesAtVertex 1 = 0
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αinst✝:Nontrivial α⊢ {s ∈ (fromEdgeSet {s(0, 1), s(1, 2)}).cliqueFinset 3 | 1 ∈ s}.card = 0
All goals completed! 🐙end WrittenOnTheWallII.GraphConjecture160