feat(ErdosProblems): formalise Erdős problem 667

[hbakkaoui-hash]

fixes #865

Formalises the statement of Erdős Problem 667, a problem of Erdős, Faudree, Rousseau, and Schelp on the growth exponent of the largest clique guaranteed inside a locally dense graph.

Content

• LocallyDense p q G — every set of p vertices spans at least q edges (via (G.induce s).edgeSet.ncard).
• H p q n — the largest m such that every (p, q)-locally dense graph on n vertices contains Kₘ, defined with Nat.findGreatest.
• c p q — the growth exponent liminf_{n → ∞} log H(n) / log n.
• erdos_667 (research open) — is q ↦ c(p, q) strictly increasing on 1 ≤ q ≤ binom(p-1, 2) + 1?

Supporting variants (research solved):

• monotoneOn — c p is nondecreasing on the interval.
• endpoint — c(p, binom(p-1, 2) + 1) = 1.
• ramsey_bounds — 1/(p-1) ≤ c(p, 1) ≤ 2/(p+1) (the q = 1 Ramsey case).

Checks

The file type-checks against the pinned toolchain (leanprover/lean4:v4.27.0); the only diagnostics are the expected declaration uses 'sorry' warnings, one per theorem, and no errors.

[github-actions]

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

• Please take a look at the style guidelines,
  especially the conventions for references, categories, AMS tags, and answer(sorry).
• You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
• This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.