/-
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 101
Definitions
The $\alpha$-core of a graph $G$, written alphaCore G, is the set of vertices
$v$ such that removing $v$ strictly decreases the independence number:
$$\mathrm{alphaCore}(G) = {v \mid \alpha(G - v) < \alpha(G)}$$
where $G - v$ is the subgraph of $G$ induced on $V(G) \setminus {v}$.
These vertices are also called "critical vertices for independence."
namespace WrittenOnTheWallII.GraphConjecture101
open Classical SimpleGraph
variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]The independence number of the subgraph induced on $V \setminus {v}$ (i.e., the graph $G - v$).
noncomputable def indepNumDeleteVertex (G : SimpleGraph α) (v : α) : ℕ :=
(G.induce (Set.univ \ {v})).indepNumThe $\alpha$-core of $G$: the set of vertices whose removal strictly decreases the independence number. A vertex $v$ is in the $\alpha$-core if $\alpha(G - v) < \alpha(G)$.
noncomputable def alphaCore (G : SimpleGraph α) : Finset α :=
Finset.univ.filter (fun v => indepNumDeleteVertex G v < G.indepNum)
WOWII Conjecture 101
For a simple connected graph $G$, $\alpha(G) \le \lfloor (n + |\mathrm{alphaCore}(G)|) / 2 \rfloor$ where $\alpha(G) = G.\mathrm{indepNum}$ is the independence number, $n$ is the number of vertices, and $\mathrm{alphaCore}(G)$ is the set of vertices whose removal decreases the independence number.
This is a theorem known to follow from inclusion-exclusion principles.
@[category research solved, AMS 5]
theorem conjecture101 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :
G.indepNum ≤ (Fintype.card α + (alphaCore G).card) / 2 := α:Type u_1inst✝³:Fintype αinst✝²:DecidableEq αinst✝¹:Nontrivial αG:SimpleGraph αinst✝:DecidableRel G.Adjh:G.Connected⊢ α(G) ≤ (Fintype.card α + (alphaCore G).card) / 2
All goals completed! 🐙
-- Sanity checks
/-- The $\alpha$-core has cardinality at most $n$ (the number of vertices). -/
@[category test, AMS 5]
example (G : SimpleGraph (Fin 3)) : (alphaCore G).card ≤ 3 := α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αinst✝:Nontrivial αG:SimpleGraph (Fin 3)⊢ (alphaCore G).card ≤ 3
All goals completed! 🐙
/-- The $\alpha$-core is always a subset of all vertices. -/
@[category test, AMS 5]
example (G : SimpleGraph (Fin 5)) : alphaCore G ⊆ Finset.univ :=
Finset.filter_subset _ _
/-- If a vertex $v$ is NOT in the $\alpha$-core, then removing $v$ does not decrease $\alpha$. -/
@[category test, AMS 5]
example (G : SimpleGraph (Fin 3)) (v : Fin 3)
(hv : v ∉ alphaCore G) :
G.indepNum ≤ indepNumDeleteVertex G v := α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αinst✝:Nontrivial αG:SimpleGraph (Fin 3)v:Fin 3hv:v ∉ alphaCore G⊢ α(G) ≤ indepNumDeleteVertex G v
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αinst✝:Nontrivial αG:SimpleGraph (Fin 3)v:Fin 3hv:v ∉ {v | indepNumDeleteVertex G v < α(G)}⊢ α(G) ≤ indepNumDeleteVertex G v
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αinst✝:Nontrivial αG:SimpleGraph (Fin 3)v:Fin 3hv:α(G) ≤ indepNumDeleteVertex G v⊢ α(G) ≤ indepNumDeleteVertex G v
All goals completed! 🐙
/-- If a vertex $v$ IS in the $\alpha$-core, then removing $v$ strictly decreases $\alpha$. -/
@[category test, AMS 5]
example (G : SimpleGraph (Fin 3)) (v : Fin 3)
(hv : v ∈ alphaCore G) :
indepNumDeleteVertex G v < G.indepNum := α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αinst✝:Nontrivial αG:SimpleGraph (Fin 3)v:Fin 3hv:v ∈ alphaCore G⊢ indepNumDeleteVertex G v < α(G)
α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αinst✝:Nontrivial αG:SimpleGraph (Fin 3)v:Fin 3hv:v ∈ {v | indepNumDeleteVertex G v < α(G)}⊢ indepNumDeleteVertex G v < α(G)
All goals completed! 🐙
end WrittenOnTheWallII.GraphConjecture101