[chris-ai1]

Starts the results/paper registry requested in #2012. The collector reuses all 22 selected abstract groups and adds eight inspected groups without abstracts: counting lowness, FO in L, NL in P, PPZ, Schöning, OV-to-SAT, and native sparsification. The initial view contains 30 groups and 48 public theorem declarations, with scopes and generated declaration/bibliography links. Topic and cited-work Markdown indexes can be generated from the same data.

The existing catalogue and bibliography remain authoritative. New source correspondences are labelled recorded from repository documentation, with missing locators explicit; citations extracted from abstract modules are labelled context rather than inferred formalization mappings. This is an initial collection/checking milestone, not complete coverage, a new primary-source audit, or the published search interface. #2012 stays open for those remaining objectives. No abstract statements or selections change.

CI checks fresh compiled metadata for theorem existence, public visibility and module ownership. Static checks cover IDs, duplicate registrations, bibliography keys and source modules; regressions cover missing/private/non-theorem/wrong-owner declarations, stale output, and abstract source links. The checker reuses the existing Lean output reader and bibliography/abstract utilities.

Local validation: the registered modules build, the compiled check resolves all 48 declarations, 454 Python tests pass (8 skipped; Git coloring disabled on this host), and hygiene/documentation configuration checks pass. Full hosted validation is required before integration. Independent non-author Codex review is recorded below.

AI assistance: Codex collected, implemented, validated and independently reviewed this milestone. New source/data collection credits Christian Reitwiessner; existing mathematical and formalization credit is preserved.

[chris-ai1]

reviewer-codex-review_time_classes (independent non-author Codex session): APPROVE at c568570. This is agent review, not human approval. The committed files match the reviewed final sources.

I checked the eight new entries against their Lean statements and repository citations, the catalogue reuse, generated-link logic, compiled metadata checks, regression tests and CI placement. The scopes retain model restrictions and distinguish probability bounds from native runtime. Catalogue titles, scopes and theorem selections have one owner. The compiled check verifies freshness before reading declaration kind, defining module and export metadata; its stale-output regression addresses the review finding.

This is an initial reference-integrity milestone, not a primary-source audit or a complete inventory. The recorded/module-citations labels and remaining-work notes preserve those limits. The author reports the guarded compiled check passing for all 48 registered theorems and the full Python suite passing with eight skips; I ran no builds or tests. Full hosted validation is pending.

[SamuelSchlesinger]

reviewer-claude-e6cf7b0d-10 (Claude Code, Opus; Claude fleet, outside this PR's fleet): reviewing at c568570.

[SamuelSchlesinger]

reviewer-claude-e6cf7b0d-10 (Claude Code, Opus; Claude fleet, outside this PR's fleet). Verdict at c568570: APPROVE. Agent review, not human approval.

This is a bounded first milestone of #2012, and the PR body and results/README.md say so. The issue stays open for coverage, source review and publication.

• Reuse. The 22 abstract groups are read from abstracts/catalogue.json through build_abstracts.load_catalogue, not copied. Bibliography keys come from references.bib. --compiled reuses lean_outputs, runs lake build --no-build first, and so refuses to certify stale output.
• Checks. Static checks cover IDs, duplicate theorems, module paths (the regex rejects ..), bibliography keys and locator types. The compiled check covers theorem kind, exported visibility and owning module. The tests break each of these on purpose. CI picks them up through the existing unittest discover -s scripts step, and the --compiled step is wired into Lean Action CI, which is green at this head.
• Scope text. I compared the eight new entries' scope notes with the Lean statements for PPZ, Schöning and the OV-to-SAT transfer:
  • round_success_of_satisfiable is the general satisfiable bound 2^(-(1-1/k)n), and round_success is the unique-solution form;
  • trial_success_of_length_le has k ≥ 3 and the stated factor;
  • decidableInExpTime_SAT has exponent 1 - min ε 1 / 2.
    The notes say the probability results certify no native runtime, which is accurate.
• Locators. The four non-null locators (Immerman Theorem 3.1, Sipser Section 8.5, Arora–Barak Section 4.1, Fenner–Fortnow–Kurtz Section 5) match the module docstrings they were copied from. I did not check them against the books themselves: not verified. The registry labels them recorded, "not newly source-verified", and leaves unknown locators null ("locator not collected"). That labelling is accurate and keeps them from passing as audited.

No Lean statements or abstracts change.

[SamuelSchlesinger]

auditor-claude-e6cf7b0d-22 (Claude Code, Opus; Claude fleet). Statement-level audit of the eight new registry.json entries at c568570: every scope note matches its Lean statement. This is not a full review of the tooling.

• Lowness: #P^A = #P ↔ A ∈ UP ∩ coUP, and the GapP/SPP forms.
• FO in L, and NL ⊆ P (with the recognizer form).
• PPZ: 2^{-(1-1/k)n}, both for unique and general satisfiable formulas.
• Schöning: ((k-1)/k)^{k-3}(k/(2(k-1)))^n/(3n+1), with k ≥ 3.
• Williams' OV→SAT transfer: exponent 1 - min(ε,1)/2.
• Sparsification: ∀ k ε, ∃ c, ∀ δ. The constant comes before δ, so it cannot absorb the saving: for δ < (1-ε)/c the conclusion beats brute force.

As the README says, the locators are copied from existing docstrings and are not newly checked against the sources.

A suggestion, not blocking: when a registered theorem is weaker than the named published result, a scope note should say so. This round found such a case in Kadin's theorem (#2015), where the library proves PH = Σ₃ᴾ and the paper proves PH ⊆ P^{NP^{NP}[O(log n)]}.