Remaining test/API proofs: mathematical work and warning visibility

Updated against FC [`2a0126f6`](https://github.com/google-deepmind/formal-conjectures/blob/2a0126f6ec4132a0acf3b9562cb2c1f4cfa4041c) on 11 September 2026.

Two separate concerns were originally mixed here.

| Concern | Current state |
| --- | --- |
| Warning visibility | CI now runs `check_category_warnings.py` explicitly. Research-open contradictions fail; unfinished `test`/`API` declarations are reported without blocking. |
| Proof policy | [`PROOFS.md`](https://github.com/google-deepmind/formal-conjectures/blob/2a0126f6ec4132a0acf3b9562cb2c1f4cfa4041c/PROOFS.md) permits a long proof to remain `by sorry` in `FormalConjectures/`. Short useful tests are welcome; large proofs should not be added just to remove a placeholder. |
| Shared mathematics | `FormalConjecturesForMathlib/` still requires complete proofs. |

The original 59 and later 53 counts are August snapshots, not today's backlog or a release gate.

**Completed examples:** Erdős 36 now has the finite-search bridge `M_eq_min'` and proofs of `M_two` through `M_five`. Scholz's `additionChainLength_first_values` and its seven-case lower-bound lemma are also proved. These no longer belong on the unfinished list.

**Remaining mathematical work includes:**

- `WrittenOnTheWallII.Test`: spectral invariants such as `house_cvetkovic` still have placeholders; proving the relevant spectra is substantive mathematics.
- Erdős 91's small-configuration optimality claims.
- `Paper.DegreeSequencesTriangleFree` construction lemmas.
- For other noncomputable infimum/supremum definitions, identify any required finite-search or bounding lemma before attempting computation.

The successful bounding-lemma examples above are a useful pattern, not a requirement to turn every statement into a computation. Keep mathematical contributions independently scoped and source-faithful. Do not relabel declarations merely to remove warnings.

This issue tracks those mathematics tasks and their disposition. The metadata, review and verification toolkit does not depend on eliminating these placeholders.

Read PROOFS.md first to understand which placeholders may remain. Then inspect WrittenOnTheWallII.Test, Erdős 91, or Paper.DegreeSequencesTriangleFree and the corresponding declarations under FormalConjecturesForMathlib/. A contribution is complete when one independently scoped mathematical task has a complete, source-faithful proof and its verification passes.

Written by the indexing model from the issue text.