Align overhaul scope and catalog lifecycle

docs/catalog-metadata.md

@@ -10,7 +10,7 @@ python scripts/validate_catalog.py
 ## Current fields
 
 - `group` is one of `formalization-evaluation`, `software-verification`, or
-  `open-conjectures`.
+  `open-problems`.
 - `status` is one of `draft`, `active`, or `archived`.
 - `visible` controls public catalog presentation independently of lifecycle.
 - `statement_revision` is a positive integer and never decreases.

docs/overhaul-execution-runbook.md

@@ -74,28 +74,28 @@ request.
 
 Goal: make the repositories describe only the approved remaining program.
 
-- [ ] Inventory every open PR, active workflow, remote branch, and relevant
+- [x] Inventory every open PR, active workflow, remote branch, and relevant
       local worktree in the allowlisted repositories.
-- [ ] Confirm the already identified escaped external branches are absent and
+- [x] Confirm the already identified escaped external branches are absent and
       the stale LeanEval PRs are closed.
-- [ ] Review any uncommitted local cleanup attempt as an untrusted candidate
+- [x] Review any uncommitted local cleanup attempt as an untrusted candidate
       diff. Keep useful pieces only after comparing them with current upstream.
-- [ ] Delete the persistent model-identity qualification harness, private
+- [x] Delete the persistent model-identity qualification harness, private
       qualification Workers, workflows, generated types, fixtures, tests, and
       rebuild/recovery instructions.
-- [ ] Delete experimental-kernel shadow smoke, Arena/Mathgraph assets,
+- [x] Delete experimental-kernel shadow smoke, Arena/Mathgraph assets,
       checker-series and corpus-promotion machinery, wire/attestation protocols,
       candidate adapters, and tests that exist only for them.
-- [ ] Remove exact-byte solution-export capture hooks that existed only to feed
+- [x] Remove exact-byte solution-export capture hooks that existed only to feed
       the removed experimental-kernel lane.
-- [ ] Retain the existing official Lean build and nanoda replay path, its
+- [x] Retain the existing official Lean build and nanoda replay path, its
       generic checker identity/revision fields, and its focused tests.
-- [ ] Preserve source-bound agent sessions, authorization boundaries,
+- [x] Preserve source-bound agent sessions, authorization boundaries,
       idempotency, CAS conflict handling, and other generally useful security
       hardening.
 - [ ] Remove superseded run narratives, diagnostic artifacts, and tests whose
       only purpose is preserving those narratives.
-- [ ] Retain canonical replay inventories, final plans, exact toolchain/source
+- [x] Retain canonical replay inventories, final plans, exact toolchain/source
       maps, unavailable-candidate data, current rollback contracts, and current
       infrastructure identifiers.
 - [ ] Retain an older canonical input set only while a live execution profile
@@ -115,33 +115,46 @@ Goal: establish one exact safe baseline before launch work resumes.
 
 ### 5.1 Repositories and automation
 
-- [ ] Record current protected `main` commits for every allowlisted repository.
-- [ ] List open PRs and cross-referenced work; close or classify stale overhaul
+- [x] Record current protected `main` commits for every allowlisted repository.
+- [x] List open PRs and cross-referenced work; close or classify stale overhaul
       PRs.
-- [ ] Confirm no unplanned workflow dispatch is queued or running.
+- [x] Confirm no unplanned workflow dispatch is queued or running.
 - [ ] Confirm required checks, protected branches, and immutable dispatch-tag
       protections match current operating needs.
 
+Current `main` baseline:
+
+| Repository | Commit | Protection state |
+| --- | --- | --- |
+| `lean-eval` | `de48559590eb8cff2125e8e933b3e13bb8a3ff98` | Required `verify` |
+| `lean-eval-submissions` | `2bdeb2be1d1cd504a567dd01a3b040ae6e341827` | Required `verify` |
+| `lean-eval-leaderboard` | `aef3269c7dd4a98781d7f2d9b23db3c196e14766` | Required `build` |
+| `lean-eval-state` | `b0a30e3a64aa5c05660040405b32135dea4b7f1d` | Required `validate`; append-only |
+| `lean-eval-state-staging` | `8d8ef8d1e30ac617d848c705907a941209aeb23c` | Required `validate`; append-only |
+| `lean-eval-releases` | `90dadc872d624b8e6d171caf439313d185fc3e7f` | Required `validate` |
+| `lean-eval-generator` | `77373a539b31f8f304c852f288d7d8469cceebff` | Required `check` |
+| `lean-eval-audit` | `ad356e7bc5a2d650d9902ac3f6d352a0164360bc` | Protection approval required |
+
 ### 5.2 Deployed services
 
-- [ ] Read staging and production intake health.
-- [ ] Read staging and production broker/replay health and current versions.
-- [ ] Verify production intake is configured and effectively disabled.
-- [ ] Verify general and production replay are disabled.
-- [ ] Verify publication is disabled.
-- [ ] Verify public lifecycle feature gates are disabled before their launch
+- [x] Read staging and production intake health.
+- [x] Read staging and production broker/replay health and current versions.
+- [x] Verify production intake is configured and effectively disabled.
+- [x] Verify general and production replay are disabled.
+- [x] Verify publication is disabled.
+- [x] Verify public lifecycle feature gates are disabled before their launch
       smoke and approval.
-- [ ] Verify deployed commits, container image digests, and protected State pins
+- [x] Verify deployed commits, container image digests, and protected State pins
       form one coherent current unit.
 
 ### 5.3 State, credentials, and presentation
 
-- [ ] Verify protected State heads and validation status.
+- [x] Verify protected State heads and validation status.
 - [ ] Inventory credential names, owners, scopes, expiry, rotation, and
       revocation without exposing values.
-- [ ] Confirm production State contains no unexpected accepted server
+- [x] Confirm production State contains no unexpected accepted server
       submission or due release work.
-- [ ] Smoke the live leaderboard root, group tabs, stable problem URLs,
+- [x] Smoke the live leaderboard root, group tabs, stable problem URLs,
       problem statements, and representative solution metadata.
 
 Exit condition: current documentation states one coherent disabled baseline.
@@ -163,12 +176,12 @@ These lanes can proceed in parallel after Phase 1.
 
 ### 6.2 Release and archive repository preparation
 
-- [ ] Reconfirm the exact staging release OIDC trust mismatch.
-- [ ] Prepare the smallest reviewed infrastructure patch or operator command;
+- [x] Reconfirm the exact staging release OIDC trust mismatch.
+- [x] Prepare the smallest reviewed infrastructure patch or operator command;
       do not apply it yet.
 - [ ] Reconfirm the production archive Wrap-only role requirement and prove the
       desired policy excludes unwrap.
-- [ ] Verify the release controller reconstructs deterministically with
+- [x] Verify the release controller reconstructs deterministically with
       publication disabled using credential-free fixtures.
 - [ ] Verify submitter-facing license, release delay, and opt-out language.
 
@@ -410,15 +423,14 @@ Update this table in place; do not append a history beneath it.
 
 | Phase | State | Current blocker |
 | --- | --- | --- |
-| 0. Rebaseline cleanup | Not started | Review and merge scoped deletions |
-| 1. Disabled baseline | Not started | Phase 0 |
-| 2. Repository launch preparation | Not started | Phase 1 |
-| Approval A. Staging credentials | Blocked on explicit approval | Exact mutation not yet presented |
+| 0. Rebaseline cleanup | In progress | Stale-instruction cleanup PRs and final validation |
+| 1. Disabled baseline | In progress | Audit-repository protection and credential inventory |
+| 2. Repository launch preparation | In progress | Entry page, lifecycle gates, and bounded fixtures |
+| Approval A. Staging credentials | Blocked on explicit approval | Exact staging trust mutation prepared but unapplied |
 | 3. Final staging acceptance | Not started | Approval A |
 | Approval B. Production launch | Blocked on explicit approval | Go/no-go packet incomplete |
 | 4. Launch | Not started | Approval B |
 | 5. Four-week overlap | Not started | Production launch |
 | 6. Historical completion | Not started | May begin after Phase 1; infrastructure steps approval-gated |
 | 7. Remaining product completion | Not started | Independent lanes; issue closure waits for overlap and final delta |
 | Final audit | Not started | All phases |
-

manifests/problems/coc_strong_normalization.toml

@@ -1,7 +1,7 @@
 id = "coc_strong_normalization"
 title = "Strong normalization and consistency for the calculus of constructions with a universe hierarchy"
 group = "software-verification"
-status = "active"
+status = "draft"
 visible = true
 statement_revision = 1
 tags = []
@@ -11,3 +11,8 @@ submitter = "Kim Morrison"
 source = "Coquand and Huet, 'The calculus of constructions' (1988); Zhaohui Luo, 'An Extended Calculus of Constructions' (1990); Bruno Barras, 'Sets in Coq, Coq in Sets' (2010)."
 notes = "Strong normalization requires Girard's reducibility candidates, and the impredicative `Prop` rule `(s, prop, prop)` is what makes a naive induction on types fail. The three anti-vacuity guards require a nonempty typing relation and exercise polymorphic typing, `Typing.app`, beta reduction, and substitution. Mathlib does not provide the requested Lean theorem; earlier Coq mechanizations and semantic models of CC and CCω are acknowledged in the module documentation."
 informal_solution = "Use reducibility candidates in the style of Girard, extended to dependent types and the predicative universe hierarchy. A smaller λC rehearsal replaces the hierarchy by `Prop` and a top sort `Type 0`; it is a different typing relation, not literally the restriction of this CCω syntax to two sorts."
+
+[[status_history]]
+status = "draft"
+effective_date = "2026-08-25"
+reason = "correction"

manifests/problems/rcf_quantifier_elimination.toml

@@ -1,7 +1,7 @@
 id = "rcf_quantifier_elimination"
 title = "Quantifier elimination for the theory of real closed fields"
 group = "software-verification"
-status = "active"
+status = "draft"
 visible = true
 statement_revision = 1
 tags = []
@@ -11,3 +11,8 @@ submitter = "Kim Morrison"
 source = "Tarski, 'A Decision Method for Elementary Algebra and Geometry' (1951); Collins, 'Quantifier elimination for real closed fields by cylindrical algebraic decomposition' (1975); Mahboubi, 'Programming and certifying a CAD algorithm in the Coq system' (2006); Cohen and Mahboubi, 'Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination' (2012)."
 notes = "`isQF_qe` and `holds_qe` are jointly load-bearing; either alone admits a trivial implementation (`fun _ => .fals` and `id` respectively). Enumerating quantifier-free syntax is not a shortcut because recognizing an equivalent candidate already requires the substantive quantifier-elimination argument. The `holds_ex_sq` guard pins the intended de Bruijn and semantic interpretation. The pinned Mathlib dependency supplies real-closed-field algebra but not this `qe`; `Classical.choice` still requires first proving existence of a quantifier-free equivalent. A separate `valid?` hole was rejected as vulnerable to a one-line noncomputable implementation; see the module documentation."
 informal_solution = "The Cohen-Hormander route has a comparatively small formalization footprint; Cohen and Mahboubi's Coq development uses an algebraic pseudo-remainder route. Cylindrical algebraic decomposition is another practical route and has been formalized in Coq, including Mahboubi's work and the current MathComp CAD development."
+
+[[status_history]]
+status = "draft"
+effective_date = "2026-08-25"
+reason = "correction"

scripts/validate_catalog.py

@@ -15,7 +15,7 @@
 PROBLEM_ID_RE = re.compile(r"^[A-Za-z0-9][A-Za-z0-9_-]*$")
 TAG_RE = re.compile(r"^[a-z0-9][a-z0-9-]*$")
 DIGEST_RE = re.compile(r"^sha256:[0-9a-f]{64}$")
-GROUPS = {"formalization-evaluation", "software-verification", "open-conjectures"}
+GROUPS = {"formalization-evaluation", "software-verification", "open-problems"}
 STATUSES = {"draft", "active", "archived"}
 REASONS = {
     "initial",

tests/python/test_validate_catalog.py

@@ -67,6 +67,21 @@ def test_valid_catalog(self):
         with temporary:
             self.assertEqual(VALIDATOR.validate(root), (1, 1, 0))
 
+    def test_open_problems_is_the_neutral_catalog_group(self):
+        temporary, root = self.make_catalog(
+            PROBLEM.replace('group = "formalization-evaluation"', 'group = "open-problems"')
+        )
+        with temporary:
+            self.assertEqual(VALIDATOR.validate(root), (1, 1, 0))
+
+        temporary, root = self.make_catalog(
+            PROBLEM.replace(
+                'group = "formalization-evaluation"', 'group = "open-conjectures"'
+            )
+        )
+        with temporary, self.assertRaisesRegex(VALIDATOR.CatalogError, "unknown group"):
+            VALIDATOR.validate(root)
+
     def test_unknown_tag_is_rejected(self):
         temporary, root = self.make_catalog(PROBLEM.replace('"annals"', '"unknown"'))
         with temporary, self.assertRaisesRegex(VALIDATOR.CatalogError, "unregistered tags"):