GraphConjecture146.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 146

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

Definitions

The square of a graph $G$, denoted $G^2$, is the graph on the same vertex set where two distinct vertices are adjacent if and only if their distance in $G$ is at most $2$.

The radius of $G^2$ is the minimum eccentricity of any vertex in $G^2$, i.e., $$\mathrm{rad}(G^2) = \min_{v \in V} \max_{u \in V} \mathrm{dist}_{G^2}(u, v).$$

Imports (1)

FormalConjecturesUtil

def WrittenOnTheWallII.GraphConjecture146.graphSquareRadius The radius of $G^2$ (the graph square): the minimum eccentricity over all vertices of graphSquare G line 46 source
Source documentation
The radius of $G^2$ (the graph square): the minimum eccentricity over all vertices of graphSquare G.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Nat
Proof uses: ENat.toNat, SimpleGraph.radius, SimpleGraph.graphSquare
```
noncomputable def graphSquareRadius (G : SimpleGraph α) : ℕ :=
…
```
theorem WrittenOnTheWallII.GraphConjecture146.conjecture146 WOWII Conjecture 146 For a simple connected graph sorry line 78 source
Source documentation
WOWII Conjecture 146
For a simple connected graph $G$, $\mathrm{tree}(G) \ge 2 \cdot \mathrm{ecc}(B) / \mathrm{rad}(G^2)$ where $\mathrm{tree}(G)$ is the number of vertices in a largest induced subtree, $\mathrm{ecc}(B)$ is the eccentricity of the boundary vertices of $G$ (eccSet and maxEccentricityVertices), and $\mathrm{rad}(G^2)$ is the radius of the square graph of $G$.
We state the inequality in the form $\mathrm{tree}(G) \cdot \mathrm{rad}(G^2) \ge 2 \cdot \mathrm{ecc}(B)$ to avoid division.
Informal proof
Write $t$ for the largest induced-tree order, $r$ and $d$ for the radius and diameter of $G$, and $p$ for the eccentricity of its peripheral set. First, the distance in the graph square is $\operatorname{dist}_{G^2}(u,v)=\lceil\operatorname{dist}_G(u,v)/2\rceil$, so $\operatorname{rad}(G^2)=\lceil r/2\rceil$. A diametral geodesic is an induced path, giving $t\ge d+1$, while $p\le d-1$. These bounds settle every case except $r=2$, $d=4$, and $p=3$. In that remaining configuration, choose a centre and shortest paths to two diametral vertices and to a vertex at distance three from the peripheral set. A finite case analysis on the two possible cross-arm edges (and then the possible chords) always produces an induced tree on at least six vertices. Hence $t\,\operatorname{rad}(G^2) \ge 2p$ in the exceptional case as well.

L4DEL explanation
WOWII Conjecture 146 For a simple connected graph $G$, $\mathrm{tree}(G) \ge 2 \cdot \mathrm{ecc}(B) / \mathrm{rad}(G^2)$ where $\mathrm{tree}(G)$ is the number of vertices in a largest induced subtree, $\mathrm{ecc}(B)$ is the eccentricity of the boundary vertices of $G$ (eccSet and maxEccentricityVertices), and $\mathrm{rad}(G^2)$ is the radius of the square graph of $G$. We state the inequality in the form $\mathrm{tree}(G) \cdot \mathrm{rad}(G^2) \ge 2 \cdot \mathrm{ecc}(B)$ to avoid division. ## Informal proof Write $t$ for the largest induced-tree order, $r$ and $d$ for the radius and diameter of $G$, and $p$ for the eccentricity of its peripheral set. First, the distance in the graph square is $\operatorname{dist}_{G^2}(u,v)=\lceil\operatorname{dist}_G(u,v)/2\rceil$, so $\operatorname{rad}(G^2)=\lceil r/2\rceil$. A diametral geodesic is an induced path, giving $t\ge d+1$, while $p\le d-1$. These bounds settle every case except $r=2$, $d=4$, and $p=3$. In that remaining configuration, choose a centre and shortest paths to two diametral vertices and to a vertex at distance three from the peripheral set. A finite case analysis on the two possible cross-arm edges (and then the possible chords) always produces an induced tree on at least six vertices. Hence $t\,\operatorname{rad}(G^2) \ge 2p$ in the exceptional case as well.
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, LT.lt, Nat, OfNat.ofNat, WrittenOnTheWallII.GraphConjecture146.graphSquareRadius, LE.le, HMul.hMul, SimpleGraph.eccSet, SimpleGraph.maxEccentricityVertices, SimpleGraph.largestInducedTreeSize
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
10 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
theorem conjecture146 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected)
    (hrad : 0 < graphSquareRadius G) :
    2 * eccSet G (maxEccentricityVertices G : Set α) ≤
    largestInducedTreeSize G * graphSquareRadius G := by
…
```
Mentions: WrittenOnTheWallII.GraphConjecture146.graphSquareRadius
example WrittenOnTheWallII.GraphConjecture146.(example at line 89) line 89 source
Source documentation
In graphSquare G, adjacent vertices in $G$ are also adjacent (edist is at most $1 \le 2$).
```
example (G : SimpleGraph (Fin 4)) (u v : Fin 4) (h : G.Adj u v) :
    (graphSquare G).Adj u v := by
…
```
example WrittenOnTheWallII.GraphConjecture146.(example at line 97) line 97 source
Source documentation
graphSquare is loopless: no vertex is adjacent to itself.
```
example (G : SimpleGraph (Fin 3)) (v : Fin 3) : ¬(graphSquare G).Adj v v := by
…
```
example WrittenOnTheWallII.GraphConjecture146.(example at line 102) line 102 source
Source documentation
The graphSquareRadius is nonneg for any graph.
```
example (G : SimpleGraph (Fin 3)) : 0 ≤ graphSquareRadius G := Nat.zero_le _
…
```
Mentions: WrittenOnTheWallII.GraphConjecture146.graphSquareRadius
example WrittenOnTheWallII.GraphConjecture146.(example at line 106) line 106 source
Source documentation
graphSquare G adjacency is symmetric.
```
example (G : SimpleGraph (Fin 4)) (u v : Fin 4) (h : (graphSquare G).Adj u v) :
    (graphSquare G).Adj v u := h.symm
…
```
example WrittenOnTheWallII.GraphConjecture146.(example at line 112) line 112 source
Source documentation
graphSquare does not join different connected components: the square of the edgeless graph on two vertices is still edgeless.
```
example : graphSquare (⊥ : SimpleGraph (Fin 2)) = ⊥ := by
…
```

FormalConjectures/WrittenOnTheWallII/GraphConjecture146.lean

Written on the Wall II - Conjecture 146

Definitions

Informal proof

`FormalConjectures/WrittenOnTheWallII/GraphConjecture146.lean`