/-
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
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 $c_{C_4}(G)$ (the number of induced
4-cycles) to lower bound the WOWII invariant $L_s(G)$, the maximum number of
leaves over all spanning trees of $G$ (exposed as SimpleGraph.Ls G : ℝ).
namespace WrittenOnTheWallII.GraphConjecture160
open Classical SimpleGraph
variable {α : 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)
WOWII Conjecture 160
For a simple connected graph $G$, $L_s(G) \ge \max_v l(v) + \max_v T(v) \cdot c_{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,
$c_{C_4}(G)$ is the number of induced 4-cycles in $G$.
@[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 := countInducedC4 G
(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 := G.countInducedC4;
↑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! 🐙
/-- In $K_3$, `countInducedC4 = 0` (no induced 4-cycles in a 3-vertex graph). -/
@[category test, AMS 5]
example : countInducedC4 (⊤ : SimpleGraph (Fin 3)) = 0 := α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αinst✝:Nontrivial α⊢ ⊤.countInducedC4 = 0
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αinst✝:Nontrivial α⊢ (∑ a,
∑ b,
∑ c,
∑ d,
if
a ≠ b ∧
a ≠ c ∧
a ≠ d ∧
b ≠ c ∧
b ≠ d ∧
c ≠ d ∧
(have check := fun p q r s =>
decide (⊤.Adj p q) && decide (⊤.Adj q r) && decide (⊤.Adj r s) && decide (⊤.Adj s p) &&
!decide (⊤.Adj p r) &&
!decide (⊤.Adj q s);
check a b c d || check a b d c || check a c b d) =
true then
1
else 0) /
24 =
0
All goals completed! 🐙
end WrittenOnTheWallII.GraphConjecture160