Formalize and refute TxGraffiti Conjecture 4 (saturation number vs. harmonic index)

Request to add (and settle):

**Source.** TxGraffiti Conjecture 4, from R. Davila, B. Brimkov, R. Pepper, *In Reverie Together: Ten Years of Mathematical Discovery with a Machine Collaborator* ([arXiv:2507.17780](https://arxiv.org/abs/2507.17780)). TxGraffiti is an automated conjecturing program in the lineage of Fajtlowiczs *Graffiti* and DeLaViñas *Graffiti.pc*.

**Statement.** For every nontrivial connected graph $G$, $`\mu^*(G) \le H(G),`$ where $`\mu^*(G)`$ is the *saturation number* — the minimum number of edges in a maximal matching (a.k.a. the lower matching number) — and $H(G) = \sum_{uv \in E(G)} \tfrac{2}{\deg u + \deg v}$ is the *harmonic index*.

**Status: false.** The friendship graph $F_4$ (a hub vertex joined to four triangles; 9 vertices, 12 edges) satisfies $\mu^*(F_4) = 4 > 18/5 = H(F_4)$. The conjecture was first refuted by T. Bıyıkoğlu, *A Note on the TxGraffiti Conjecture about Harmonic Index and Minimum Maximal Matching Number* (MATCH Commun. Math. Comput. Chem. 96(3):1097–1099, 2026), via a family of edges joined to an independent set with unbounded $\mu^*/H$. The minimality of order 9 and the exact windmill limit are established in C. Gupta, *The saturation number is not bounded by the harmonic index* ([arXiv:2606.15761](https://arxiv.org/abs/2606.15761)).

**Planned contribution.**
- `FormalConjecturesForMathlib`: `SimpleGraph.harmonicIndex` (computable ℚ edge sum) and `SimpleGraph.saturationNumber` (noncomputable `sInf` over maximal matchings, plus a computable companion and a kernel-verified bridge, mirroring the existing `dominationNumber` pattern).
- `FormalConjectures/Arxiv/2507.17780/`: a `@[category research solved]` theorem `answer(False) ↔ ∀ nontrivial connected G, μ*(G) ≤ H(G)`, proved by exhibiting $F_4$.

Start by reading the existing dominationNumber pattern in FormalConjecturesForMathlib. Add the planned harmonicIndex and saturationNumber formalizations, including the computable companion and kernel-verified bridge, then work in FormalConjectures/Arxiv/2507.17780/ on the research-solved theorem using the friendship graph F₄ as the counterexample.

Written by the indexing model from the issue text.