[mrphilo420]

What changed

• manifests/problems/rouche_zero_count_eq.toml: status changed from archived to active, with an append-only [[status_history]] row (active, 2026-10-27, restoration). statement_revision remains 1.
• generated/rouche_zero_count_eq/README.md: regenerated status line changed from archived to active.

No statement, module, or generated Lean file changes.

Why

rouche_zero_count_eq is listed and submission-enabled on math-challenge.org, but submissions fail at problem_catalog_verification before any Lean work:

{
  "error": "source_not_found",
  "request_id": "8a8a964e-2f9c-4abf-95f9-cb6bf4dfc5b7",
  "stage": "problem_catalog_verification",
  "provider_status": 404,
  "provider_operation": "benchmark manifest contents response"
}

The math-challenge verifier resolves a problem by fetching manifests/problems/<id>.toml from its benchmark repository. The public LeanEval manifest exists but is archived; a fetch of that manifest would produce 409 problem_not_open_for_submission (which the official LeanEval submission returns), not the 404 the math-challenge verifier returns. The math-challenge verifier is reading a different catalog that lacks the file. Restoring the canonical entry is the first step; the math-challenge maintainer can then mirror it or point the verifier at the canonical catalog.

Validation

From a checkout at current main with this manifest:

$ python3 scripts/validate_catalog.py
Catalog valid: 312 problems, 1 tags, 2 named sets.

The status-history dates increase and the final entry matches status = "active". The problem is not a member of the frozen v1 set; manifests/sets/ is untouched. The trusted module LeanEval/ComplexAnalysis/Rouche.lean and generated/rouche_zero_count_eq/ already exist at main.

Caveat

The math-challenge project's sync commit is 3f3786f3b4d9a4b64a5859b3036aca190cd25613 (Lean v4.32.2), while current main is 208b6b22d396f28771dba56414b19f47cae5f2a7 (Lean v4.35.0-rc3). The submitted proof was validated at the older pin; if the verifier uses current main, it must be revalidated there. This PR is catalog-only and makes no claim about the proof.

If maintaining the archived status is preferred, the alternative is for math-challenge to disable submissions for this row; the current page offers a submission that its verifier cannot catalog.

[mrphilo420]

Closing this: the v1 selection evidence shows rouche_zero_count_eq already has 12 solves, 6 public submissions, and 11 unique solvers (audits/v1/selection-2026-08-20.json), and it is not in the frozen v1 set. It was archived by policy on 2026-08-20 because it is already solved, not because it was a draft awaiting catalog work. Reopening it would allow duplicate solves.

The math-challenge 404 is a stale-site/catalog issue: its page is open and submission-enabled for an archived problem, and its verifier reads a catalog that does not contain the manifest. The right fix is for math-challenge to disable submissions for that row (or grade archived problems independently), not to restore the LeanEval entry.

The underlying proof is still a valid independent formalization; it just is not a new benchmark solve.