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

14 declarations, 0 contain sorry, 0 declared as axioms

Induced trees, neighbourhood independence, and girth

Supporting API for WOWII (Graffiti.pc) Conjecture 141. Main results:

SimpleGraph.indepNeighborsCard_add_one_le_largestInducedTreeSize: an independent set in a neighbourhood plus its centre induces a star, so indepNeighborsCard G v + 1 ≤ largestInducedTreeSize G.
SimpleGraph.isIndepSet_neighborSet_of_four_le_girth: girth at least four makes every neighbourhood independent.
SimpleGraph.maxDegree_add_girth_le_largestInducedTreeSize_add_three: for a connected cyclic graph of girth at least four, Δ(G) + girth(G) ≤ largestInducedTreeSize G + 3 — a maximum-order induced tree containing the closed neighbourhood of a maximum-degree vertex admits an outside vertex with two neighbours on the tree; the tree path joining them closes a cycle (so has length at least girth - 2) and shares at most three vertices with the closed neighbourhood.

Imports (2)

Imported by 1 file

FormalConjecturesForMathlib.lean

lemma SimpleGraph.path_start_unique_edge In a path, at most one edge is incident to the first vertex line 48 source
Source documentation
In a path, at most one edge is incident to the first vertex.
```
private lemma path_start_unique_edge {a b u₁ u₂ : β} {p : H.Walk a b}
    (hp : p.IsPath) (h₁ : s(a, u₁) ∈ p.edges) (h₂ : s(a, u₂) ∈ p.edges) :
    u₁ = u₂ := by
…
```
Mentions: SimpleGraph.b
lemma SimpleGraph.path_incident_edges_le_two In a path, at most two edges are incident to any fixed vertex w: among any three vertices joined to w by edges of the path, two coincide line 67 source
Source documentation
In a path, at most two edges are incident to any fixed vertex w: among any three vertices joined to w by edges of the path, two coincide.
```
private lemma path_incident_edges_le_two {a b w u₁ u₂ u₃ : β} {p : H.Walk a b}
    (hp : p.IsPath) (h₁ : s(w, u₁) ∈ p.edges) (h₂ : s(w, u₂) ∈ p.edges)
    (h₃ : s(w, u₃) ∈ p.edges) :
    u₁ = u₂ ∨ u₁ = u₃ ∨ u₂ = u₃ := by
…
```
Mentions: SimpleGraph.b
lemma SimpleGraph.exists_subpath_between A path visiting a and b contains a subpath between a and b (in one of the two directions) whose support and edges lie in the original path line 106 source
Source documentation
A path visiting a and b contains a subpath between a and b (in one of the two directions) whose support and edges lie in the original path.
```
private lemma exists_subpath_between {x y a b : β} {p : H.Walk x y} (hp : p.IsPath)
    (ha : a ∈ p.support) (hb : b ∈ p.support) :
    (∃ q : H.Walk a b, q.IsPath ∧ q.support ⊆ p.support ∧ q.edges ⊆ p.edges) ∨
    (∃ q : H.Walk b a, q.IsPath ∧ q.support ⊆ p.support ∧ q.edges ⊆ p.edges) := by
…
```
Mentions: SimpleGraph.b
lemma SimpleGraph.tree_isPath_eq_cons_nil In a tree, the unique path between two adjacent vertices is the single edge line 131 source
Source documentation
In a tree, the unique path between two adjacent vertices is the single edge.
```
private lemma tree_isPath_eq_cons_nil (hH : H.IsTree) {a b : β} (hab : H.Adj a b)
    {q : H.Walk a b} (hq : q.IsPath) :
    q = Walk.cons hab Walk.nil := by
…
```
Mentions: SimpleGraph.b
lemma SimpleGraph.tree_center_mem_support Documented declaration: tree_center_mem_support line 141 source
Source documentation
Two path-vertices adjacent (in a tree) to a common vertex v force v onto the path: the unique tree path between them is the two-edge path through v, and the subpath of p between them must be that path.
```
private lemma tree_center_mem_support (hH : H.IsTree)
    {v a b x y : β} (hva : H.Adj v a) (hvb : H.Adj v b) (hab : a ≠ b)
    {p : H.Walk x y} (hp : p.IsPath) (hap : a ∈ p.support) (hbp : b ∈ p.support) :
    v ∈ p.support := by
…
```
Mentions: SimpleGraph.b
lemma SimpleGraph.tree_edge_mem_of_center_mem Documented declaration: tree_edge_mem_of_center_mem line 166 source
Source documentation
If v lies on a path in a tree and a is a path-vertex adjacent to v, then the edge s(v, a) is an edge of the path: the subpath of p between v and a is the unique tree path, which is the single edge.
```
private lemma tree_edge_mem_of_center_mem (hH : H.IsTree)
    {v a x y : β} (hva : H.Adj v a)
    {p : H.Walk x y} (hp : p.IsPath) (hvp : v ∈ p.support) (hap : a ∈ p.support) :
    s(v, a) ∈ p.edges := by
…
```
lemma SimpleGraph.IsTree.girth_le_length_add_two_of_two_adj Documented declaration: girth_le_length_add_two_of_two_adj line 191 source
Source documentation
Mapping a path of an induced tree into G and closing it up through an outside vertex z adjacent to both endpoints produces a cycle of length p.length + 2, so the girth is at most p.length + 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Finset, SimpleGraph.IsTree, SimpleGraph.induce, Not, Membership.mem, Ne, SimpleGraph.Adj, SimpleGraph.Walk, Subtype.mk, Set, Iff.mpr, Finset.mem_coe, SimpleGraph.Walk.IsPath, LE.le, Nat, SimpleGraph.girth, HAdd.hAdd, SimpleGraph.Walk.length, OfNat.ofNat
Proof uses: SimpleGraph.Embedding, SimpleGraph.Embedding.induce, SimpleGraph.Walk.map, SimpleGraph.Embedding.toHom, id, SimpleGraph.Hom, Subtype, SimpleGraph.Walk.isPath_map_iff_of_injective, RelEmbedding.injective, Eq, SimpleGraph.Walk.length_map, List, SimpleGraph.Walk.support, And, Exists, Iff.mp, List.map, List.mem_map, Eq.mp, congrArg and 37 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
lemma IsTree.girth_le_length_add_two_of_two_adj
    {s : Finset α}
    (_hT : (G.induce (s : Set α)).IsTree)
    {z a b : α}
    (hz : z ∉ s) (ha : a ∈ s) (hb : b ∈ s)
    (hab : a ≠ b) (hza : G.Adj z a) (hzb : G.Adj z b)
    (p : (G.induce (s : Set α)).Walk ⟨a, Finset.mem_coe.mpr ha⟩ ⟨b, Finset.mem_coe.mpr hb⟩)
    (hp : p.IsPath) :
    G.girth ≤ p.length + 2 := by
…
```
Mentions: SimpleGraph.b
lemma SimpleGraph.isIndepSet_neighborSet_of_four_le_girth Triangle-free bridge: in a graph of girth at least 4, the neighborhood of any vertex is an independent set line 236 source
Source documentation
Triangle-free bridge: in a graph of girth at least 4, the neighborhood of any vertex is an independent set. An edge inside a neighborhood would close a 3-cycle with the two star edges.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, LE.le, Nat, OfNat.ofNat, SimpleGraph.girth, SimpleGraph.IsIndepSet, SimpleGraph.neighborSet
Proof uses: Membership.mem, Set, Ne, SimpleGraph.Adj, SimpleGraph.Adj.ne', SimpleGraph.Walk.IsPath, SimpleGraph.Walk.cons, SimpleGraph.Adj.symm, SimpleGraph.Walk.nil, SimpleGraph.Walk.IsPath.cons, SimpleGraph.Walk.IsPath.nil, of_eq_true, Not, List, SimpleGraph.Walk.support, Eq.trans, False, True, congrArg, List.cons and 30 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
lemma isIndepSet_neighborSet_of_four_le_girth (hg4 : 4 ≤ G.girth) (v : α) :
    G.IsIndepSet (G.neighborSet v) := by
…
```
lemma SimpleGraph.IsTree.card_support_inter_closedNeighborFinset_le_three Overlap lemma: on a path p in an induced tree on s, at most 3 vertices lie in the closed neighborhood of a fixed vertex v ∈ s line 272 source
Source documentation
Overlap lemma: on a path p in an induced tree on s, at most 3 vertices lie in the closed neighborhood of a fixed vertex v ∈ s. Here the path support is read off in α via Subtype.val.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Finset, SimpleGraph.IsTree, SimpleGraph.induce, Membership.mem, SimpleGraph.Walk, SimpleGraph.Walk.IsPath, LE.le, Nat, Finset.card, Inter.inter, List.toFinset, List.map, Subtype, Set, SimpleGraph.Walk.support and 4 more
Proof uses: Iff.mpr, Finset.mem_coe, Eq.mpr, id, Eq, congrArg, rfl, Iff, Exists, And, List, of_eq_true, Eq.trans, Subtype.mk, Iff.of_eq, Eq.refl, True, congr, List.unattach, congrFun' and 39 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 60 steps
Open to load the checked before-and-after goal states.
```
lemma IsTree.card_support_inter_closedNeighborFinset_le_three
    [DecidableRel G.Adj] {s : Finset α}
    (hT : (G.induce (s : Set α)).IsTree) {v : α} (hv : v ∈ s)
    {x y : ↥(s : Set α)} {p : (G.induce (s : Set α)).Walk x y} (hp : p.IsPath) :
    ((p.support.map Subtype.val).toFinset ∩ insert v (G.neighborFinset v)).card ≤ 3 := by
…
```
lemma SimpleGraph.exists_indepSet_finset_neighbors Extract an explicit independent neighbour set witnessing indepNeighborsCard line 342 source
Source documentation
Extract an explicit independent neighbour set witnessing indepNeighborsCard.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, SimpleGraph, Exists, Finset, And, Membership.mem, SimpleGraph.Adj, SimpleGraph.IsIndepSet, Eq, Nat, Finset.card, SimpleGraph.indepNeighborsCard
Proof uses: SimpleGraph.neighborSet, SimpleGraph.IsNIndepSet, SimpleGraph.induce, SimpleGraph.indepNum, SimpleGraph.exists_isNIndepSet_indepNum, Exists.intro, Finset.image, Subtype, Set, And.intro, Iff.mp, Finset.mem_image, Subtype.property, Ne, Not, Finset.mem_coe, SimpleGraph.IsNIndepSet.isIndepSet, congrArg, Eq.mpr, id and 3 more
12 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma exists_indepSet_finset_neighbors (G : SimpleGraph α) (v : α) :
    ∃ S : Finset α, (∀ s ∈ S, G.Adj v s) ∧ G.IsIndepSet (S : Set α) ∧
      S.card = indepNeighborsCard G v := by
…
```
Mentions: SimpleGraph.S, SimpleGraph.indepNeighborsCard
lemma SimpleGraph.isTree_induce_insert_indepSet_neighbors A vertex together with an independent set of its neighbours induces a star, hence a tree line 361 source
Source documentation
A vertex together with an independent set of its neighbours induces a star, hence a tree.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, SimpleGraph, Finset, Membership.mem, SimpleGraph.Adj, SimpleGraph.IsIndepSet, SimpleGraph.IsTree, Insert.insert, SimpleGraph.induce
Proof uses: Finset.induction_on, EmptyCollection.emptyCollection, Eq, Set, Singleton.singleton, of_eq_true, Eq.trans, True, congrFun', congrArg, LawfulSingleton.insert_empty_eq, Finset.coe_singleton, eq_self, Eq.mpr, id, Nonempty, Nonempty.intro, Subtype.mk, Subsingleton, Subsingleton.intro and 30 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
```
lemma isTree_induce_insert_indepSet_neighbors (v : α) (S : Finset α) :
    (∀ s ∈ S, G.Adj v s) → G.IsIndepSet (S : Set α) →
    (G.induce ((insert v S : Finset α) : Set α)).IsTree := by
…
```
Mentions: SimpleGraph.S
lemma SimpleGraph.indepNeighborsCard_add_one_le_largestInducedTreeSize The star bound: indepNeighborsCard G v + 1 ≤ largestInducedTreeSize G line 407 source
Source documentation
The star bound: indepNeighborsCard G v + 1 ≤ largestInducedTreeSize G.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, LE.le, Nat, HAdd.hAdd, SimpleGraph.indepNeighborsCard, OfNat.ofNat, SimpleGraph.largestInducedTreeSize
Proof uses: Finset, And, Membership.mem, SimpleGraph.Adj, SimpleGraph.IsIndepSet, Eq, Finset.card, Exists, SimpleGraph.exists_indepSet_finset_neighbors, Not, SimpleGraph.irrefl, SimpleGraph.IsTree, Insert.insert, SimpleGraph.induce, SimpleGraph.isTree_induce_insert_indepSet_neighbors, SimpleGraph.card_le_largestInducedTreeSize, Eq.mp, congrArg, Finset.card_insert_of_notMem
15 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma indepNeighborsCard_add_one_le_largestInducedTreeSize (G : SimpleGraph α) (v : α) :
    indepNeighborsCard G v + 1 ≤ largestInducedTreeSize G := by
…
```
Mentions: SimpleGraph.indepNeighborsCard, SimpleGraph.largestInducedTreeSize
lemma SimpleGraph.indepNeighborsCard_le_degree The independence number of a neighbourhood is at most the degree line 418 source
Source documentation
The independence number of a neighbourhood is at most the degree.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, LE.le, Nat, SimpleGraph.indepNeighborsCard, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet
Proof uses: Finset, SimpleGraph.IsNIndepSet, SimpleGraph.induce, SimpleGraph.indepNum, Exists, SimpleGraph.exists_isNIndepSet_indepNum, Trans.trans, Eq, Fintype.card, Finset.card, Eq.symm, SimpleGraph.IsNIndepSet.card_eq, Finset.card_le_univ, Eq.mpr, id, congrArg, SimpleGraph.card_neighborSet_eq_degree, Eq.refl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma indepNeighborsCard_le_degree (G : SimpleGraph α) [DecidableRel G.Adj] (v : α) :
    indepNeighborsCard G v ≤ G.degree v := by
…
```
Mentions: SimpleGraph.indepNeighborsCard
theorem SimpleGraph.maxDegree_add_girth_le_largestInducedTreeSize_add_three Main counting theorem: in a connected graph with a cycle and girth at least 4, Δ(G) + girth(G) ≤ largestInducedTreeSize G + 3 line 436 source
Source documentation
Main counting theorem: in a connected graph with a cycle and girth at least 4, Δ(G) + girth(G) ≤ largestInducedTreeSize G + 3.
Proof: grow a maximum induced tree s through the closed neighborhood of a maximum-degree vertex v; a boundary vertex z of s has two neighbors a ≠ b in s, and the tree path from a to b closes through z into a cycle, so it has at least girth − 2 edges; the path meets the closed neighborhood of v in at most 3 vertices, so inclusion–exclusion inside s gives the bound.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Nontrivial, SimpleGraph.Connected, Not, SimpleGraph.IsAcyclic, LE.le, Nat, OfNat.ofNat, SimpleGraph.girth, HAdd.hAdd, SimpleGraph.maxDegree, SimpleGraph.largestInducedTreeSize
Proof uses: Eq, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Exists, SimpleGraph.exists_maximal_degree_vertex, Finset, SimpleGraph.neighborFinset, Iff.mp, SimpleGraph.mem_neighborFinset, SimpleGraph.IsIndepSet, Eq.mpr, id, congrArg, SimpleGraph.coe_neighborFinset, SimpleGraph.isIndepSet_neighborSet_of_four_le_girth, SimpleGraph.IsTree, Insert.insert, SimpleGraph.induce and 65 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
theorem maxDegree_add_girth_le_largestInducedTreeSize_add_three
    (G : SimpleGraph α) [DecidableRel G.Adj] [Nontrivial α] (hG : G.Connected)
    (hcyc : ¬ G.IsAcyclic) (hg4 : 4 ≤ G.girth) :
    G.maxDegree + G.girth ≤ largestInducedTreeSize G + 3 := by
…
```
Mentions: SimpleGraph.largestInducedTreeSize