feat(docs): seed a checked results and reference registry

.github/workflows/lean_action_ci.yml

@@ -160,6 +160,8 @@ jobs:
           test -d .lake/packages
           python3 -B -m unittest scripts/test_check_tidy_surface.py
           python3 -B scripts/check_tidy_surface.py
+      - name: "Result registry references"
+        run: python3 -B scripts/results_registry.py --compiled
       # Lints for the files a pull request adds or changes: names in module docstrings' "Main …"
       # lists exist, and a new test file does more than restate signatures. See
       # scripts/check_changed_files.py. The checkout is shallow, so the base commit is fetched

README.md

@@ -45,6 +45,10 @@ uses graph complementation; the [reduction index](Complexity/Computability/Compl
 points to the other proved problems and their reduction maps. The checked examples state these
 claims with plain `ComputableInPolyTime`.
 
+The [results and reference inventory](results/README.md) collects named results, exact Lean
+declarations and cited sources, including results without formal abstracts. It is an initial,
+incomplete collection with CI-checked declaration references.
+
 The [selected formal abstracts](abstracts/README.md) present a small set of major results with
 inspectable definitions and checked Lean statements. The [combined PDF](https://www.cslib.io/complexitylib/abstracts/catalogue.pdf)
 and individual PDFs are generated from those sources. Each states its model and limitations;

results/README.md

@@ -0,0 +1,58 @@
+# Results and reference inventory
+
+This is the first collection for [#2012](https://github.com/cslib-community/complexitylib/issues/2012),
+not a complete inventory of the library or a claim that every cited paper is fully formalized.
+Initial collection: Christian Reitwiessner, with Codex assistance.
+
+The collector reuses all 22 selected groups in [the abstract catalogue](../abstracts/catalogue.json)
+and adds eight groups in [registry.json](registry.json): oracle counting lowness, first-order
+model checking in L, NL ⊆ P, PPZ and Schöning success bounds, the OV-to-SAT transfer, and native
+sparsification. The existing catalogue owns abstract titles, scopes and theorem selections; they
+are not copied into a second manifest. The bibliography remains [references.bib](../references.bib).
+
+Run from the repository root:
+
+```bash
+python3 scripts/results_registry.py                  # IDs, modules and bibliography references
+python3 scripts/results_registry.py --markdown         # results grouped by topic
+python3 scripts/results_registry.py --papers           # results grouped by cited bibliography key
+python3 scripts/results_registry.py --compiled         # built public-theorem references
+```
+
+The generated Markdown contains declaration links, scope notes, recorded source locators,
+bibliography links, and optional abstract PDFs. Library declarations link to the API docs;
+abstract declarations link directly to their Lean sources because their modules are not part
+of the published API documentation. Source links follow `main`, so a proposed entry becomes
+available there after integration.
+
+The compiled check requires the registered modules to have been built. CI runs it after the
+library and tests, using the same Lean output reader as the existing declaration audits. It
+rejects missing or renamed declarations, private declarations, definitions or axioms presented
+as theorems, and declarations attributed to the wrong module. Static checks reject unknown
+bibliography keys, missing modules, invalid IDs and duplicate theorem registrations.
+
+## What the references mean
+
+- **`recorded`**: the initial collector inspected the Lean statement and copied the citation and
+  locator from existing repository documentation. This collection does not provide a new
+  independent check against the original paper. A null locator means that a precise locator
+  has not yet been collected; it must not be filled by guessing.
+- **`module-citations`**: bibliography keys extracted from an abstract's documentation. They may
+  describe background, definitions, alternative proofs or several distinct results. Grouping by
+  these keys is a discovery aid, not a claim that each theorem formalizes every cited source.
+
+The abstracts retain their existing checked bridges and review requirements. The registry
+checker establishes reference integrity; it establishes neither mathematical correspondence
+nor completeness. A result's explicit hypotheses and model restrictions remain authoritative.
+In particular, probability bounds do not imply certified native runtime, and a conditional
+result is not an unconditional endpoint.
+
+## Remaining collection work
+
+Collect precise paper-to-result correspondences and locators, record their source review, and
+audit coverage across the library. Algorithms, cryptography, proof complexity, circuit bounds,
+communication and descriptive complexity contain substantial additional results beyond this
+seed. The topic index currently groups catalogue-derived entries under “selected abstracts”;
+more detailed topic classification remains to be collected. Original results without an
+external source need an explicit representation before adding them. Publication and search are
+also tracked in #2012. None of these gaps is satisfied merely by a passing reference check.

results/registry.json

@@ -0,0 +1,154 @@
+{
+  "schema_version": 1,
+  "abstract_catalogue": "abstracts/catalogue.json",
+  "results": [
+    {
+      "id": "sharp-p-lowness",
+      "title": "Exact characterization of #P oracle lowness",
+      "topic": "counting classes",
+      "module": "Complexity.Computability.Complexity.Classes.SharpP.Lowness",
+      "theorems": [
+        "Cslib.Complexity.SharpPWithOracle_eq_SharpP_iff"
+      ],
+      "sources": [
+        {
+          "bib_key": "KoeblerSchoeningTodaToran1992",
+          "locator": null
+        }
+      ],
+      "source_review": "recorded",
+      "scope": "Equality of #P^A and #P on binary words iff A is in UP ∩ coUP. Uses strict polynomial-time adaptive word-oracle verifiers, with resource bounds for arbitrary replies; does not assert an oracle-machine counting characterization."
+    },
+    {
+      "id": "gap-p-spp-lowness",
+      "title": "GapP and SPP lowness characterize SPP",
+      "topic": "counting classes",
+      "module": "Complexity.Computability.Complexity.Classes.SharpP.Lowness",
+      "theorems": [
+        "Cslib.Complexity.GapPWithOracle_eq_GapP_iff",
+        "Cslib.Complexity.SPPWithOracle_eq_SPP_iff"
+      ],
+      "sources": [
+        {
+          "bib_key": "FennerFortnowKurtz1994",
+          "locator": "Section 5"
+        }
+      ],
+      "source_review": "recorded",
+      "scope": "Binary-word instances; strict adaptive oracle-verifier model. GapP is a difference of two unsigned witness counts."
+    },
+    {
+      "id": "first-order-logspace",
+      "title": "Fixed first-order queries are decidable in logarithmic space",
+      "topic": "descriptive complexity",
+      "module": "Complexity.Computability.Complexity.Classes.LogSpace.FirstOrder",
+      "theorems": [
+        "Cslib.Logic.Vocabulary.queryLanguage_mem_L",
+        "Cslib.Logic.FO.Definable.queryLanguage_mem_L"
+      ],
+      "sources": [
+        {
+          "bib_key": "Immerman1999",
+          "locator": "Theorem 3.1"
+        }
+      ],
+      "source_review": "recorded",
+      "scope": "Fixed first-order sentences over finite relational vocabularies, with explicit structure encoding and malformed-input rejection. Includes empty structures and nullary relations; excludes constants and built-in order/BIT from the cited FO convention."
+    },
+    {
+      "id": "nl-in-p",
+      "title": "NL is contained in P",
+      "topic": "space complexity",
+      "module": "Complexity.Computability.Complexity.Classes.LogSpace.PolyTime",
+      "theorems": [
+        "Cslib.Complexity.NL_subset_P",
+        "Cslib.Complexity.mem_P_of_recognizesInSpace"
+      ],
+      "sources": [
+        {
+          "bib_key": "Sipser2013",
+          "locator": "Section 8.5"
+        },
+        {
+          "bib_key": "AroraBarak09",
+          "locator": "Section 4.1"
+        }
+      ],
+      "source_review": "recorded",
+      "scope": "Finite-control native nondeterministic multi-tape machines and arbitrary injective encodings. The stronger recognizer result permits nonterminating branches with logarithmic workspace; deterministic polynomial-time configuration reachability decides acceptance."
+    },
+    {
+      "id": "ppz-success",
+      "title": "PPZ success probability for k-SAT",
+      "topic": "SAT algorithms",
+      "module": "Complexity.Computability.Complexity.FineGrained.PPZ",
+      "theorems": [
+        "Cslib.Complexity.PPZ.round_success_of_satisfiable",
+        "Cslib.Complexity.PPZ.round_success"
+      ],
+      "sources": [
+        {
+          "bib_key": "PPZ1997",
+          "locator": null
+        }
+      ],
+      "source_review": "recorded",
+      "scope": "CNF over Fin n, clauses of length at most k ≥ 1. One-round success probability at least 2^(-(1 - 1/k)n); also a unique-solution theorem. Probabilistic semantics only: these declarations do not certify native runtime."
+    },
+    {
+      "id": "schoening-success",
+      "title": "Schöning randomized k-SAT success bound",
+      "topic": "SAT algorithms",
+      "module": "Complexity.Computability.Complexity.FineGrained.Schoening",
+      "theorems": [
+        "Cslib.Complexity.Schoening.trial_success_of_length_le",
+        "Cslib.Complexity.Schoening.trial_success"
+      ],
+      "sources": [
+        {
+          "bib_key": "Schoening1999",
+          "locator": null
+        }
+      ],
+      "source_review": "recorded",
+      "scope": "Satisfiable CNF over a finite variable type, width at most k ≥ 3, uniform start and 3n local-search steps. Lower bound ((k-1)/k)^(k-3) · (k/(2(k-1)))^n / (3n+1). Explicit factors are this formalization’s constants; no native runtime assertion."
+    },
+    {
+      "id": "ov-sat-transfer",
+      "title": "Williams split-and-list transfer from OV to SAT",
+      "topic": "fine-grained complexity",
+      "module": "Complexity.Computability.Complexity.FineGrained.OrthogonalVectors",
+      "theorems": [
+        "Cslib.Complexity.DecidableInTimeO.decidableInExpTime_SAT"
+      ],
+      "sources": [
+        {
+          "bib_key": "Williams2005",
+          "locator": null
+        }
+      ],
+      "source_review": "recorded",
+      "scope": "An OV decider of time N^(2-ε) times a polynomial in dimension yields native SAT time of exponent 1 - min(ε,1)/2 in occurring variables, with polynomial encoded-input overhead. This records the transfer, not the separate conditional OVH result or logarithmic-dimension OVH."
+    },
+    {
+      "id": "native-sparsification",
+      "title": "Native algorithmic consequence of sparsification",
+      "topic": "fine-grained complexity",
+      "module": "Complexity.Computability.Complexity.FineGrained.Sparsification",
+      "theorems": [
+        "Cslib.Complexity.exists_decidableInExpTime_numVars_of_length"
+      ],
+      "sources": [
+        {
+          "bib_key": "ImpagliazzoPaturiZane2001",
+          "locator": null
+        }
+      ],
+      "source_review": "recorded",
+      "scope": "For fixed width k and ε > 0, some natural c transfers a k-SAT decider of clause-count exponent δ ≥ 0 to variable-count exponent ε + cδ. Native machines, encCNF and polynomial encoded-length overhead; no new sharp sparsification constant."
+    }
+  ],
+  "collection_authors": [
+    "Christian Reitwiessner"
+  ]
+}