Erdős 23: weighted cycle background special case with an external Lean proof

Propose adding a solved weighted special case to `FormalConjectures/ErdosProblems/23.lean`, with a linked external Lean proof.

In the Mycielski lift of the Clebsch graph, give each original vertex weight r, add h on the cycle (0,1,3,7,15), give the apex weight z, and give the twins arbitrary nonnegative weights b_v. For every r,h,z ≥ 0, there is a cut with monochromatic edge weight at most (16r + 5h + sum b_v + z)^2 / 25. Each undirected edge is counted once. The result includes zero weights and every boundary case.

The [proof note](https://github.com/SproutSeeds/erdos-problems/blob/68fbae4b2f6eba86f1b28d62b1b370bfabd7d92a/packs/graph-theory/problems/23/publication/cycle-background/PROOF.md) gives five closed regions and exact rational certificates. The [standalone Lean project](https://github.com/SproutSeeds/erdos-problems/blob/68fbae4b2f6eba86f1b28d62b1b370bfabd7d92a/packs/graph-theory/problems/23/publication/cycle-background/README.md) includes a complete proof of the [precise statement](https://github.com/SproutSeeds/erdos-problems/blob/68fbae4b2f6eba86f1b28d62b1b370bfabd7d92a/packs/graph-theory/problems/23/publication/cycle-background/P23CycleBackgroundSubmission.lean#L50), pinned dependencies, axiom audits and exact replay. The full Problem 23 remains open.

I plan to submit a small draft PR adding this variant, its graph and weight definitions, and three basic tests. Would this scope fit the collection?

AI assistance: OpenAI Codex developed and formalized the proof and prepared this contribution under my direction. Independent expert review and publication novelty review are still pending.

Start with FormalConjectures/ErdosProblems/23.lean, then read the linked PROOF.md and P23CycleBackgroundSubmission.lean for the precise statement and proof structure. Add the weighted special case, graph and weight definitions, and three basic tests; the external proof should remain replayable with its pinned dependencies and audits.

Written by the indexing model from the issue text.