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

3 declarations, 0 contain sorry, 0 declared as axioms

TxGraffiti Conjecture 4: the saturation number versus the harmonic index

Reference: arxiv/2507.17780 In Reverie Together: Ten Years of Mathematical Discovery with a Machine Collaborator by Randy Davila, Boris Brimkov, Ryan Pepper

TxGraffiti is an automated conjecturing program, a successor of Fajtlowicz's Graffiti and DeLaViña's Graffiti.pc. Conjecture 4 in the cited collection asserts a bound between two graph invariants:

the saturation number $\mu^*(G)$ (SimpleGraph.saturationNumber), the minimum number of edges in a maximal matching of $G$;
the harmonic index $H(G)$ (SimpleGraph.harmonicIndex), $\sum_{uv \in E(G)} 2 / (\deg u + \deg v)$.

The conjecture is false. It was first refuted by Bıyıkoğlu, who exhibited a family of counterexamples — a disjoint union of edges joined to an independent set — with unbounded ratio $\mu^*/H$. That the smallest counterexample has order $9$, namely the friendship graph $F_4$ formalised below, and that the windmill family has an exact limiting ratio, are established in Gupta.

References:

A Note on the TxGraffiti Conjecture about Harmonic Index and Minimum Maximal Matching Number, Türker Bıyıkoğlu, MATCH Commun. Math. Comput. Chem. 96 (2026), no. 3, 1097–1099 — the first refutation.
The saturation number is not bounded by the harmonic index, C. Gupta — the order-$9$ minimality of $F_4$ (formalised below) and the exact windmill limit.

Imports (4)

def Arxiv.«2507.17780».friendshipF4 The friendship graph $F_4$: a hub vertex $0$ joined to four triangles, whose rims are the pairs $\{1,2\}, \{3,4\}, \{5,6\}, \{7,8\}$ line 64 source
Source documentation
The friendship graph $F_4$: a hub vertex $0$ joined to four triangles, whose rims are the pairs $\{1,2\}, \{3,4\}, \{5,6\}, \{7,8\}$. It has $12$ edges on $9$ vertices ($8$ spokes and $4$ rim edges).

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.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def friendshipF4 : SimpleGraph (Fin 9) := fromEdgeSet {
…
```
instance Arxiv.«2507.17780».(instance at line 68) line 68 source
theorem Arxiv.«2507.17780».tx_graffiti_conjecture_4 TxGraffiti Conjecture 4: for every nontrivial connected graph $G$, the saturation number is at most the harmonic index, $\mu^*(G) \le H(G)$ line 95 source
Source documentation
TxGraffiti Conjecture 4: for every nontrivial connected graph $G$, the saturation number is at most the harmonic index, $\mu^*(G) \le H(G)$.
This conjecture is FALSE.
Counterexample. The friendship graph $F_4$ (friendshipF4) is connected and nontrivial, with $\mu^*(F_4) = 4$ and $H(F_4) = 18/5$. Indeed the four rim edges $\{1,2\}, \{3,4\}, \{5,6\}, \{7,8\}$ form a maximal matching of size $4$, and no maximal matching is smaller, so $\mu^*(F_4) = 4$; the eight spokes contribute $2/(8+2) = 1/5$ each and the four rim edges contribute $2/(2+2) = 1/2$ each, giving $H(F_4) = 8 \cdot 1/5 + 4 \cdot 1/2 = 18/5$. Since $4 > 18/5$, the bound fails.
More generally the friendship graphs $F_k$ satisfy $\mu^*(F_k) = k$ and $H(F_k) = 2k/(k+1) + k/2$, so the conjecture fails for every $k \ge 4$. An exhaustive search confirms that $F_4$ is the smallest counterexample (order $9$). The unbounded separation was first shown by Bıyıkoğlu, whose family of edges joined to an independent set makes $\mu^*/H$ arbitrarily large; the windmill generalisation and its exact limit appear in arXiv:2606.15761.

L4DEL explanation
TxGraffiti Conjecture 4: for every nontrivial connected graph $G$, the saturation number is at most the harmonic index, $\mu^*(G) \le H(G)$. This conjecture is FALSE. Counterexample. The friendship graph $F_4$ (friendshipF4) is connected and nontrivial, with $\mu^*(F_4) = 4$ and $H(F_4) = 18/5$. Indeed the four rim edges $\{1,2\}, \{3,4\}, \{5,6\}, \{7,8\}$ form a maximal matching of size $4$, and no maximal matching is smaller, so $\mu^*(F_4) = 4$; the eight spokes contribute $2/(8+2) = 1/5$ each and the four rim edges contribute $2/(2+2) = 1/2$ each, giving $H(F_4) = 8 \cdot 1/5 + 4 \cdot 1/2 = 18/5$. Since $4 > 18/5$, the bound fails. More generally the friendship graphs $F_k$ satisfy $\mu^*(F_k) = k$ and $H(F_k) = 2k/(k+1) + k/2$, so the conjecture fails for every $k \ge 4$. An exhaustive search confirms that $F_4$ is the smallest counterexample (order $9$). The unbounded separation was first shown by Bıyıkoğlu, whose family of edges joined to an independent set makes $\mu^*/H$ arbitrarily large; the windmill generalisation and its exact limit appear in arXiv:2606.15761.
Sources and attribution: Pinned Lean source (1646ca16afd6)

extra axioms: _private.0.Arxiv.«2507.17780».tx_graffiti_conjecture_4._native.native_decide.ax_1, _private.0.Arxiv.«2507.17780».tx_graffiti_conjecture_4._native.native_decide.ax_2 what this means
Statement uses: Iff, False, Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, LE.le, Rat, SimpleGraph.saturationNumber, SimpleGraph.harmonicIndex
Proof uses: iff_of_false, of_eq_true, Not, not_false_eq_true, Fin, OfNat.ofNat, Nat, Arxiv.«2507.17780».friendshipF4, of_decide_eq_true, SimpleGraph.computableSaturationNumber, Eq.mp, congrArg, SimpleGraph.saturationNumber_eq_computable
19 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem tx_graffiti_conjecture_4 : answer(False) ↔
    ∀ (V : Type) [Fintype V] [DecidableEq V] [Nontrivial V] (G : SimpleGraph V)
      [DecidableRel G.Adj] (_hConn : G.Connected),
      (G.saturationNumber : ℚ) ≤ G.harmonicIndex := by
…
```