GraphConjecture101.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

7 declarations, 1 contain sorry, 0 declared as axioms

Written on the Wall II - Conjecture 101

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

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."

Imports (1)

FormalConjecturesUtil

def WrittenOnTheWallII.GraphConjecture101.indepNumDeleteVertex The independence number of the subgraph induced on $V \setminus \{v\}$ (i.e., the graph $G - v$) line 46 source
Source documentation
The independence number of the subgraph induced on $V \setminus \{v\}$ (i.e., the graph $G - v$).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Nat
Proof uses: SimpleGraph.indepNum, SDiff.sdiff, Set, Set.univ, Singleton.singleton, SimpleGraph.induce
3 instances, coercions and auxiliary constants left out.
```
noncomputable def indepNumDeleteVertex (G : SimpleGraph α) (v : α) : ℕ :=
…
```
def WrittenOnTheWallII.GraphConjecture101.alphaCore The $\alpha$-core of $G$: the set of vertices whose removal strictly decreases the independence number line 51 source
Source documentation
The $\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)$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Finset
Proof uses: Finset.filter, LT.lt, Nat, WrittenOnTheWallII.GraphConjecture101.indepNumDeleteVertex, SimpleGraph.indepNum, Finset.univ
2 instances, coercions and auxiliary constants left out.
```
noncomputable def alphaCore (G : SimpleGraph α) : Finset α :=
…
```
theorem WrittenOnTheWallII.GraphConjecture101.conjecture101 WOWII Conjecture 101 For a simple connected graph sorry line 66 source
Source documentation
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.

L4DEL explanation
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.
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, LE.le, Nat, SimpleGraph.indepNum, HDiv.hDiv, HAdd.hAdd, Fintype.card, Finset.card, WrittenOnTheWallII.GraphConjecture101.alphaCore, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
12 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem conjecture101 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) :
    G.indepNum ≤ (Fintype.card α + (alphaCore G).card) / 2 := by
…
```
Mentions: WrittenOnTheWallII.GraphConjecture101.alphaCore
example WrittenOnTheWallII.GraphConjecture101.(example at line 74) line 74 source
Source documentation
The $\alpha$-core has cardinality at most $n$ (the number of vertices).
```
example (G : SimpleGraph (Fin 3)) : (alphaCore G).card ≤ 3 := by
…
```
Mentions: WrittenOnTheWallII.GraphConjecture101.alphaCore
example WrittenOnTheWallII.GraphConjecture101.(example at line 79) line 79 source
Source documentation
The $\alpha$-core is always a subset of all vertices.
```
example (G : SimpleGraph (Fin 5)) : alphaCore G ⊆ Finset.univ :=
…
```
Mentions: WrittenOnTheWallII.GraphConjecture101.alphaCore
example WrittenOnTheWallII.GraphConjecture101.(example at line 84) line 84 source
Source documentation
If a vertex $v$ is NOT in the $\alpha$-core, then removing $v$ does not decrease $\alpha$.
```
example (G : SimpleGraph (Fin 3)) (v : Fin 3)
    (hv : v ∉ alphaCore G) :
    G.indepNum ≤ indepNumDeleteVertex G v := by
…
```
Mentions: WrittenOnTheWallII.GraphConjecture101.alphaCore, WrittenOnTheWallII.GraphConjecture101.indepNumDeleteVertex
example WrittenOnTheWallII.GraphConjecture101.(example at line 93) line 93 source
Source documentation
If a vertex $v$ IS in the $\alpha$-core, then removing $v$ strictly decreases $\alpha$.
```
example (G : SimpleGraph (Fin 3)) (v : Fin 3)
    (hv : v ∈ alphaCore G) :
    indepNumDeleteVertex G v < G.indepNum := by
…
```
Mentions: WrittenOnTheWallII.GraphConjecture101.alphaCore, WrittenOnTheWallII.GraphConjecture101.indepNumDeleteVertex