Erdős Problem 993 (unimodality of the independence sequence of a forest) is missing — candidate statement enclosed

Erdős Problem 993 does not appear to be formalised here — 990, 996 and 997 are present, but 993 is not — and I couldn't find a formal statement of it anywhere else.

I have a candidate formalisation below and would value a check that it is faithful before I open a PR.

### The problem

From [erdosproblems.com/993](https://www.erdosproblems.com/993):

> The independent set sequence of any tree or forest is unimodal.
>
> In other words, if $i_k(G)$ counts the number of independent sets of vertices of size $k$ in a graph $G$, and $T$ is any tree or forest, then for some $m \geq 0$
> $$i_0(T) \le i_1(T) \le \cdots \le i_m(T) \ge i_{m+1}(T) \ge i_{m+2}(T) \ge \cdots$$

Asked by Alavi, Malde, Schwenk and Erdős, *The vertex independence sequence of a graph is not constrained*, Congr. Numer. **58** (1987), 15–23, who showed that the independence sequence of a general graph can be arbitrarily far from unimodal.

### Candidate statement

```lean
open SimpleGraph

namespace Erdos993

/--
A sequence `a : ℕ → ℕ` is *unimodal* if for some `m` it is nondecreasing up to `m` and
nonincreasing from `m` onwards:
`a 0 ≤ a 1 ≤ ⋯ ≤ a m ≥ a (m+1) ≥ a (m+2) ≥ ⋯`.
-/
def Unimodal (a : ℕ → ℕ) : Prop :=
∃ m : ℕ, (∀ k : ℕ, k < m → a k ≤ a (k + 1)) ∧ (∀ k : ℕ, m ≤ k → a (k + 1) ≤ a k)

@[category research open, AMS 5]
theorem erdos_993 {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V)
[DecidableRel G.Adj] (hG : G.IsAcyclic) :
Unimodal (fun k => (G.indepSetFinset k).card) := by
sorry

end Erdos993
```

It elaborates against current Mathlib with only the expected `sorry` warning.

### Notes on the three definitional choices

These are the places where a formalisation of this problem could go wrong, so I want to be explicit about them:

1. **Forests.** `SimpleGraph.IsAcyclic` is exactly "no cycles", i.e. forest. The informal statement says "any tree or forest"; since a tree is a connected forest, quantifying over acyclic graphs covers both, and is the more general of the two readings.

2. **The counting convention.** `(G.indepSetFinset k).card` unfolds to counting `s` with `IsNIndepSet k s = (s.Pairwise (¬ G.Adj) ∧ s.card = k)`. In particular $i_0 = 1$, because the empty set is vacuously pairwise non-adjacent. I believe that is the intended convention (it is what makes the independence polynomial have constant term 1), but flagging it since an off-by-one here would silently change the problem.

3. **Unimodality, and the tail.** I've transcribed the displayed formula literally, over all of `ℕ`, rather than truncating at the independence number. The truncated version is equivalent — $i_k = 0$ beyond the independence number, and the sequence is nonincreasing into those zeros — but the untruncated form matches the source and spares the reader that argument.

Separately, as a check that the peak-based predicate isn't an idiosyncratic reading of "unimodal", I've proved it equivalent in Lean to an independently phrased predicate ("there are no indices `i < j < k` with `a j` strictly below both `a i` and `a k`"). Happy to contribute that equivalence as an `API` lemma if useful; it's around 60 lines, which I think exceeds the guidance for inlined proofs, so I left it out here.

I'd be glad to open a PR if this looks right, or to adjust anything to house style first.

*Disclosure: this formalisation was produced with AI assistance, and checked against Mathlib source definition by definition.*

Start by checking the candidate `Erdos993.erdos_993` against the current Mathlib definitions of `SimpleGraph.IsAcyclic` and `G.indepSetFinset`. Confirm that the counting convention and `Unimodal` predicate match the intended problem, then identify the repository location and contribution conventions before opening a PR; done means the statement is accepted and the missing proof work is clearly scoped.

Written by the indexing model from the issue text.