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

5 declarations, 1 contain sorry, 0 declared as axioms

Written on the Wall II - Conjecture 160

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

Definitions

For a vertex $v$ in $G$, $T(v)$ is the number of triangles incident to $v$: $$T(v) = |\{\{u, w\} \subseteq N(v) \mid u \sim w\}|$$ i.e., the number of pairs of neighbors of $v$ that are themselves adjacent.

The invariant maxTrianglesAtVertex G is the maximum of $T(v)$ over all vertices.

Conjecture 160 uses both $\max_v T(v)$ and $\chi_{C_4}(G)$, the $C_4$-free characteristic function: it is 1 when $G$ contains no cycle of length four and 0 otherwise. The cycle need not be induced. These invariants lower-bound the WOWII invariant $L_s(G)$, the maximum number of leaves over all spanning trees of $G$ (exposed as SimpleGraph.Ls G : ℝ).

The earlier formalization used the number of induced four-cycles. The historical conjecture instead uses this binary $C_4$-free indicator.

Provenance. Statement corrected by Dominic Dabish.

Imports (1)

FormalConjecturesUtil

def WrittenOnTheWallII.GraphConjecture160.maxTrianglesAtVertex The maximum number of triangles incident to any vertex in $G$ line 57 source
Source documentation
The maximum number of triangles incident to any vertex in $G$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, Nat
Proof uses: Finset.max', Finset.image, SimpleGraph.numTrianglesAtVertex, Finset.univ
3 instances, coercions and auxiliary constants left out.
```
noncomputable def maxTrianglesAtVertex (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=
…
```
theorem WrittenOnTheWallII.GraphConjecture160.conjecture160 sorry line 84 source
depends on sorry what this means
Statement uses: Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, Nat, Finset.max', Finset.image, SimpleGraph.indepNeighborsCard, Finset.univ, WrittenOnTheWallII.GraphConjecture160.maxTrianglesAtVertex, ite, Exists, SimpleGraph.Walk, And, SimpleGraph.Walk.IsCycle, Eq, SimpleGraph.Walk.length and 7 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
24 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
example WrittenOnTheWallII.GraphConjecture160.(example at line 95) line 95 source
Source documentation
In $K_3$, every vertex has $1$ triangle incident to it.
```
example : numTrianglesAtVertex (⊤ : SimpleGraph (Fin 3)) (0 : Fin 3) = 1 := by
…
```
example WrittenOnTheWallII.GraphConjecture160.(example at line 101) line 101 source
Source documentation
In $K_3$, maxTrianglesAtVertex = 1.
```
example : maxTrianglesAtVertex (⊤ : SimpleGraph (Fin 3)) = 1 := by
…
```
Mentions: WrittenOnTheWallII.GraphConjecture160.maxTrianglesAtVertex
example WrittenOnTheWallII.GraphConjecture160.(example at line 108) line 108 source
Source documentation
In the path $P_3$, vertex $1$ is adjacent to $0$ and $2$, but $0$ and $2$ are not adjacent. So $T(1) = 0$.
```
example : numTrianglesAtVertex
    (SimpleGraph.fromEdgeSet {s(0,1), s(1,2)} : SimpleGraph (Fin 3)) (1 : Fin 3) = 0 := by
…
```