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

15 declarations, 0 contain sorry, 0 declared as axioms

Written on the Wall II - Conjecture 65

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

Counterexample

The conjecture is false. Start with the path $v_0-v_1-\cdots-v_{12}$ and attach one triangle at $v_1$ and another at $v_{11}$. The resulting graph has $17$ vertices. Its Graph_6 string is PhCGGC@?G?_@?@O?G?G?G?@C. Its only minimum-degree vertices are $v_0$ and $v_{12}$, at distance $12$, while its only maximum-degree vertices are $v_1$ and $v_{11}$, at distance $10$. Thus the conjectured lower bound is $12 + \lceil 10/3 \rceil = 16$.

Every induced forest must omit at least one vertex from each of the two vertex-disjoint triangles, so it has at most $15$ vertices. Conversely, deleting one non-path vertex from each triangle leaves a tree on $15$ vertices.

Imports (1)

FormalConjecturesUtil

abbrev WrittenOnTheWallII.GraphConjecture65.Counterexample.graph The counterexample: a path on vertices $0,\ldots,12$, with triangles attached at vertices $1$ and $11$ line 56 source
Source documentation
The counterexample: a path on vertices $0,\ldots,12$, with triangles attached at vertices $1$ and $11$.
```
abbrev graph : SimpleGraph (Fin 17) :=
…
```
lemma WrittenOnTheWallII.GraphConjecture65.Counterexample.connected The counterexample is connected line 66 source
Source documentation
The counterexample is connected.
```
lemma connected : graph.Connected := by decide +kernel
…
```
lemma WrittenOnTheWallII.GraphConjecture65.Counterexample.min_degree_vertices The minimum-degree vertices of the counterexample are the two path endpoints line 70 source
Source documentation
The minimum-degree vertices of the counterexample are the two path endpoints.
```
lemma min_degree_vertices :
    {v | graph.degree v = graph.minDegree} = ({0, 12} : Set (Fin 17)) := by
…
```
lemma WrittenOnTheWallII.GraphConjecture65.Counterexample.max_degree_vertices The maximum-degree vertices of the counterexample are the two triangle attachment points line 77 source
Source documentation
The maximum-degree vertices of the counterexample are the two triangle attachment points.
```
lemma max_degree_vertices :
    {v | graph.degree v = graph.maxDegree} = ({1, 11} : Set (Fin 17)) := by
…
```
lemma WrittenOnTheWallII.GraphConjecture65.Counterexample.distMin_min_degree_vertices The minimum distance between minimum-degree vertices is $12$ line 84 source
Source documentation
The minimum distance between minimum-degree vertices is $12$.
```
lemma distMin_min_degree_vertices : distMin graph ({0, 12} : Set (Fin 17)) = 12 := by
…
```
Mentions: WrittenOnTheWallII.GraphConjecture65.Counterexample.graph
lemma WrittenOnTheWallII.GraphConjecture65.Counterexample.distMin_max_degree_vertices The minimum distance between maximum-degree vertices is $10$ line 91 source
Source documentation
The minimum distance between maximum-degree vertices is $10$.
```
lemma distMin_max_degree_vertices : distMin graph ({1, 11} : Set (Fin 17)) = 10 := by
…
```
Mentions: WrittenOnTheWallII.GraphConjecture65.Counterexample.graph
lemma WrittenOnTheWallII.GraphConjecture65.Counterexample.triangle_not_subset_of_isAcyclic An acyclic induced subgraph cannot contain all three vertices of a triangle line 98 source
Source documentation
An acyclic induced subgraph cannot contain all three vertices of a triangle.
```
lemma triangle_not_subset_of_isAcyclic (S : Finset (Fin 17))
    (hS : (graph.induce S).IsAcyclic) {a b c : Fin 17}
    (hab : graph.Adj a b) (hbc : graph.Adj b c) (hca : graph.Adj c a) :
    ¬({a, b, c} : Finset (Fin 17)) ⊆ S := by
…
```
Mentions: c
lemma WrittenOnTheWallII.GraphConjecture65.Counterexample.forest_card_le_fifteen Every induced forest in the counterexample has at most $15$ vertices line 124 source
Source documentation
Every induced forest in the counterexample has at most $15$ vertices.
```
lemma forest_card_le_fifteen (S : Finset (Fin 17)) (hS : (graph.induce S).IsAcyclic) :
    S.card ≤ 15 := by
…
```
lemma WrittenOnTheWallII.GraphConjecture65.Counterexample.largest_induced_forest_le_fifteen The largest induced forest in the counterexample has at most $15$ vertices line 150 source
Source documentation
The largest induced forest in the counterexample has at most $15$ vertices.
```
lemma largest_induced_forest_le_fifteen : graph.largestInducedForestSize ≤ 15 := by
…
```
theorem WrittenOnTheWallII.GraphConjecture65.conjecture65 WOWII Conjecture 65: Does every simple connected graph line 175 source
Source documentation
WOWII Conjecture 65:
Does every simple connected graph $G$ satisfy $f(G) \ge \operatorname{dist\_min}(A) + \lceil \operatorname{dist\_min}(M) / 3 \rceil$, where $A$ is the set of minimum-degree vertices, $M$ is the set of maximum-degree vertices, and $\operatorname{dist\_min}(S)$ is the minimum distance between two distinct vertices of $S$ (see distMin).
The answer is no. Counterexample.graph has a conjectured lower bound of $16$, but every induced forest in it has at most $15$ vertices.

L4DEL explanation
WOWII Conjecture 65: Does every simple connected graph $G$ satisfy $f(G) \ge \operatorname{dist\_min}(A) + \lceil \operatorname{dist\_min}(M) / 3 \rceil$, where $A$ is the set of minimum-degree vertices, $M$ is the set of maximum-degree vertices, and $\operatorname{dist\_min}(S)$ is the minimum distance between two distinct vertices of $S$ (see distMin). The answer is no. Counterexample.graph has a conjectured lower bound of $16$, but every induced forest in it has at most $15$ vertices.
Sources and attribution: Pinned Lean source (1646ca16afd6)
```
theorem conjecture65 : answer(False) ↔
    ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
      (G : SimpleGraph α) [DecidableRel G.Adj] (_hG : G.Connected),
      let A : Set α := {v | G.degree v = G.minDegree}
…
```
example WrittenOnTheWallII.GraphConjecture65.(example at line 199) line 199 source
Source documentation
The largestInducedForestSize is nonneg.
```
example (G : SimpleGraph (Fin 3)) : 0 ≤ G.largestInducedForestSize := Nat.zero_le _
…
```
example WrittenOnTheWallII.GraphConjecture65.(example at line 203) line 203 source
Source documentation
In the complete graph K₃, min degree equals max degree (regular graph).
```
example : (⊤ : SimpleGraph (Fin 3)).minDegree = (⊤ : SimpleGraph (Fin 3)).maxDegree := by
…
```
example WrittenOnTheWallII.GraphConjecture65.(example at line 208) line 208 source
Source documentation
distMin G S is always nonneg.
```
example (G : SimpleGraph (Fin 3)) (S : Set (Fin 3)) : 0 ≤ distMin G S := Nat.zero_le _
…
```
example WrittenOnTheWallII.GraphConjecture65.(example at line 212) line 212 source
Source documentation
In $K_2$, the minimum distance between its two vertices is $1$.
```
example : distMin (⊤ : SimpleGraph (Fin 2)) ({0, 1} : Set (Fin 2)) = 1 := by
…
```
example WrittenOnTheWallII.GraphConjecture65.(example at line 231) line 231 source
Source documentation
A singleton contains no distinct pair, so distMin uses its degenerate-case fallback.
```
example : distMin (⊤ : SimpleGraph (Fin 3)) ({0} : Set (Fin 3)) = 0 := by
…
```