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

9 declarations, 0 contain sorry, 0 declared as axioms

Written on the Wall II - Conjecture 36

The conjecture is false. The counterexample below has a subdivided triangle on vertices 0, 1, 9; vertices 7, 8 adjacent to all three triangle vertices; and leaves 3, 2 attached to 7, 8, respectively. It has radius three, one diametrical pair, and largest induced-path order five.

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

Imports (1)

FormalConjecturesUtil

def WrittenOnTheWallII.GraphConjecture36.dp dp G is the number of diametrical pairs of G: the number of unordered pairs {u, v} of vertices at distance diam(G) line 40 source
Source documentation
dp G is the number of diametrical pairs of G: the number of unordered pairs {u, v} of vertices at distance diam(G).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Nat
Proof uses: Finset.card, Sym2, Finset.filter, Equiv, Subtype, Eq, Sym2.lift, Subtype.mk, And, SimpleGraph.dist, SimpleGraph.diam, Ne, Classical.propDecidable, Finset.univ
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
noncomputable def dp {α : Type*} [Fintype α] (G : SimpleGraph α) : ℕ :=
…
```
abbrev WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample A 10-vertex counterexample to Conjecture 36 line 47 source
Source documentation
A 10-vertex counterexample to Conjecture 36.

standard axioms: Quot.sound, propext what this means
Statement uses: SimpleGraph, Fin, OfNat.ofNat, Nat
Proof uses: SimpleGraph.fromEdgeSet, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton
6 instances, coercions and auxiliary constants left out.
```
abbrev wowii36Counterexample : SimpleGraph (Fin 10) :=
…
```
theorem WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_connected The counterexample is connected line 57 source
Source documentation
The counterexample is connected.

extra axioms: _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_connected._native.decide.ax_1 what this means
Statement uses: SimpleGraph.Connected, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample
Proof uses: of_decide_eq_true, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem wowii36Counterexample_connected : wowii36Counterexample.Connected := by
…
```
theorem WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_radius The counterexample has radius three line 62 source
Source documentation
The counterexample has radius three.

extra axioms: _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_connected._native.decide.ax_1, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_radius._native.decide.ax_1 what this means
Statement uses: Eq, Nat, ENat.toNat, SimpleGraph.radius, Fin, OfNat.ofNat, WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample
Proof uses: Eq.mpr, ENat, SimpleGraph.computable_radius, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, id, congrArg, SimpleGraph.radius_eq_computable, WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_connected, of_decide_eq_true
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem wowii36Counterexample_radius : wowii36Counterexample.radius.toNat = 3 := by
…
```
theorem WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_no_inducedPath6 The counterexample contains no induced path on six vertices line 68 source
Source documentation
The counterexample contains no induced path on six vertices.

extra axioms: _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_no_inducedPath6._native.native_decide.ax_1 what this means
Statement uses: Not, Exists, Fin, OfNat.ofNat, Nat, And, Function.Injective, Iff, SimpleGraph.Adj, WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample, Or, Eq, HAdd.hAdd
Proof uses: of_decide_eq_true, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem wowii36Counterexample_no_inducedPath6 :
    ¬ ∃ e : Fin 6 → Fin 10, Function.Injective e ∧
      ∀ i j : Fin 6, wowii36Counterexample.Adj (e i) (e j) ↔
        i.val + 1 = j.val ∨ j.val + 1 = i.val := by
…
```
theorem WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path The largest induced path in the counterexample has exactly five vertices line 76 source
Source documentation
The largest induced path in the counterexample has exactly five vertices.

extra axioms: _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_no_inducedPath6._native.native_decide.ax_1, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_1, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_10, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_11, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_12, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_13, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_14, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_15, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_16, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_17, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_18, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_19, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_2, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_20, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_21, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_22, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_23, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_24, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_25, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_3, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_4, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_5, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_6, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_7, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_8, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_9 what this means
Statement uses: Eq, Nat, SimpleGraph.path, Fin, OfNat.ofNat, WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample
Proof uses: Nat.le_antisymm, SimpleGraph.path_le_of_not_exists_inducedPath_succ, WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_no_inducedPath6, SimpleGraph.isInducedPath, List.cons, List.nil, And.intro, List.Nodup, List.length, Iff, SimpleGraph.Adj, List.get, Or, HAdd.hAdd, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl and 30 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
theorem wowii36Counterexample_path : path wowii36Counterexample = 5 := by
…
```
Mentions: WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample
theorem WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp The counterexample has a unique diametrical pair, namely {2, 3} line 90 source
Source documentation
The counterexample has a unique diametrical pair, namely {2, 3}.

extra axioms: _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_connected._native.decide.ax_1, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.decide.ax_1, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_10, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_100, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_101, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_102, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_11, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_12, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_13, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_14, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_15, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_16, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_17, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_18, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_19, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_20, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_21, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_22, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_23, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_24, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_25, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_26, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_27, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_28, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_29, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_3, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_30, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_31, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_32, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_33, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_34, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_35, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_36, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_37, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_38, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_39, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_4, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_40, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_41, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_42, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_43, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_44, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_45, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_46, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_47, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_48, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_49, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_5, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_50, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_51, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_52, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_53, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_54, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_55, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_56, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_57, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_58, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_59, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_6, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_60, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_61, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_62, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_63, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_64, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_65, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_66, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_67, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_68, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_69, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_7, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_70, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_71, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_72, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_73, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_74, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_75, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_76, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_77, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_78, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_79, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_8, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_80, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_81, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_82, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_83, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_84, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_85, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_86, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_87, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_88, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_89, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_9, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_90, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_91, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_92, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_93, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_94, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_95, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_96, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_97, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_98, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_99 what this means
Statement uses: Eq, Nat, WrittenOnTheWallII.GraphConjecture36.dp, Fin, OfNat.ofNat, WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample
Proof uses: SimpleGraph.diam, id, Eq.mpr, ENat.toNat, SimpleGraph.ediam, ENat, SimpleGraph.computable_ediam, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, congrArg, SimpleGraph.ediam_eq_computable, WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_connected, of_decide_eq_true, Finset.card, Finset.filter, Equiv, Subtype and 42 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
theorem wowii36Counterexample_dp : dp wowii36Counterexample = 1 := by
…
```
Mentions: WrittenOnTheWallII.GraphConjecture36.dp, WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample
theorem WrittenOnTheWallII.GraphConjecture36.conjecture36 WOWII Conjecture 36: For every finite simple connected graph line 119 source
Source documentation
WOWII Conjecture 36:
For every finite simple connected graph $G$, $\operatorname{path}(G) \ge 2 \cdot \operatorname{rad}(G) / \operatorname{dp}(G)$, where $\operatorname{path}(G)$ is the number of vertices in a largest induced path, $\operatorname{rad}(G)$ is the radius of $G$, and $\operatorname{dp}(G)$ is the number of diametrical pairs of $G$ — that is, the number of pairs of vertices at distance $\operatorname{diam}(G)$.
Disproved by Waller in Oct 2003 (counterexample: path number 5, radius 3, dp 1).

L4DEL explanation
WOWII Conjecture 36: For every finite simple connected graph $G$, $\operatorname{path}(G) \ge 2 \cdot \operatorname{rad}(G) / \operatorname{dp}(G)$, where $\operatorname{path}(G)$ is the number of vertices in a largest induced path, $\operatorname{rad}(G)$ is the radius of $G$, and $\operatorname{dp}(G)$ is the number of diametrical pairs of $G$ — that is, the number of pairs of vertices at distance $\operatorname{diam}(G)$. Disproved by Waller in Oct 2003 (counterexample: path number 5, radius 3, dp 1).
Sources and attribution: Pinned Lean source (1646ca16afd6)

extra axioms: _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_connected._native.decide.ax_1, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.decide.ax_1, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_10, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_100, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_101, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_102, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_11, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_12, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_13, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_14, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_15, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_16, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_17, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_18, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_19, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_20, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_21, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_22, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_23, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_24, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_25, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_26, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_27, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_28, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_29, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_3, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_30, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_31, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_32, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_33, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_34, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_35, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_36, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_37, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_38, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_39, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_4, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_40, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_41, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_42, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_43, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_44, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_45, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_46, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_47, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_48, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_49, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_5, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_50, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_51, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_52, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_53, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_54, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_55, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_56, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_57, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_58, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_59, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_6, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_60, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_61, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_62, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_63, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_64, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_65, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_66, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_67, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_68, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_69, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_7, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_70, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_71, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_72, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_73, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_74, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_75, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_76, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_77, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_78, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_79, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_8, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_80, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_81, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_82, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_83, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_84, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_85, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_86, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_87, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_88, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_89, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_9, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_90, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_91, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_92, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_93, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_94, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_95, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_96, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_97, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_98, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp._native.native_decide.ax_99, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_no_inducedPath6._native.native_decide.ax_1, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_1, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_10, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_11, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_12, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_13, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_14, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_15, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_16, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_17, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_18, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_19, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_2, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_20, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_21, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_22, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_23, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_24, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_25, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_3, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_4, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_5, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_6, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_7, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_8, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_path._native.native_decide.ax_9, _private.0.WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_radius._native.decide.ax_1 what this means
Statement uses: Iff, False, Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, LT.lt, Nat, OfNat.ofNat, WrittenOnTheWallII.GraphConjecture36.dp, LE.le, Real, HDiv.hDiv, HMul.hMul, ENat.toNat, SimpleGraph.radius, SimpleGraph.path
Proof uses: id, Eq.mpr, Not, Eq, congrArg, false_iff, Fin, WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_connected, WrittenOnTheWallII.GraphConjecture36.wowii36Counterexample_dp, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false and 14 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem conjecture36 : answer(False) ↔
    ∀ {α : Type} [Fintype α] [DecidableEq α] [Nontrivial α],
      ∀ (G : SimpleGraph α) [DecidableRel G.Adj] (_ : G.Connected) (_ : 0 < dp G),
        (2 * G.radius.toNat : ℝ) / (dp G : ℝ) ≤ (path G : ℝ) := by
…
```
Mentions: WrittenOnTheWallII.GraphConjecture36.dp
example WrittenOnTheWallII.GraphConjecture36.(example at line 138) line 138 source
Source documentation
The path G invariant is nonneg.
```
example (G : SimpleGraph (Fin 3)) : 0 ≤ (path G : ℝ) := Nat.cast_nonneg _
…
```