From c568570a3db2a4ebe30c2aca802e53b574ccfe1a Mon Sep 17 00:00:00 2001 From: chris-ai1 Date: Sat, 31 Oct 2026 11:13:59 +0000 Subject: [PATCH] feat(docs): seed a checked results and reference registry Collect eight named result groups beyond the 22 selected abstract groups, reusing catalogue and bibliography metadata. Generate topic and cited-work indexes with theorem/source links and explicit scope/source-review labels. Validate fresh compiled public theorem ownership in CI using the existing Lean output reader. Validation: registered Lean modules build; the actual compiled check resolves 48 public theorems; 454 Python tests pass (8 skipped) with Git coloring disabled to match CI. Hygiene and documentation configuration pass. Independent Codex review covers data, checker and workflow; full hosted validation remains required. Initial collection milestone of #2012, not complete coverage or a new primary-source audit. AI-assisted with Codex; new collection credits Christian Reitwiessner. --- .github/workflows/lean_action_ci.yml | 2 + README.md | 4 + results/README.md | 58 +++++++++ results/registry.json | 154 ++++++++++++++++++++++ scripts/results_registry.py | 187 +++++++++++++++++++++++++++ scripts/test_results_registry.py | 94 ++++++++++++++ 6 files changed, 499 insertions(+) create mode 100644 results/README.md create mode 100644 results/registry.json create mode 100644 scripts/results_registry.py create mode 100644 scripts/test_results_registry.py diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 7f1527a867..9e8d37f918 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.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 diff --git a/README.md b/README.md index 7bbf3fe9d6..40cf9cae5d 100644 --- a/README.md +++ b/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; diff --git a/results/README.md b/results/README.md new file mode 100644 index 0000000000..8f943b370e --- /dev/null +++ b/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. diff --git a/results/registry.json b/results/registry.json new file mode 100644 index 0000000000..1573b53c87 --- /dev/null +++ b/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" + ] +} diff --git a/scripts/results_registry.py b/scripts/results_registry.py new file mode 100644 index 0000000000..fab0f7d5a8 --- /dev/null +++ b/scripts/results_registry.py @@ -0,0 +1,187 @@ +#!/usr/bin/env python3 +# Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +# Released under Apache 2.0 license as described in the file LICENSE. +# Authors: Christian Reitwiessner +"""Collect named results alongside the selected abstracts; validate their declaration links. + +This checks references, not mathematical correspondence or completeness of coverage. +`--compiled` uses the same Lean output reader as the tidy/declaration audits. +""" +from __future__ import annotations + +import argparse +import json +from pathlib import Path +import re +import subprocess +from urllib.parse import quote + +import build_abstracts +import check_hygiene +import lean_outputs + +ROOT = Path(__file__).resolve().parents[1] +REPOSITORY = "https://github.com/cslib-community/complexitylib/blob/main/" +API = "https://www.cslib.io/complexitylib/" + + +def module_path(module: str, root: Path) -> Path: + if not re.fullmatch(r"(?:Complexity|ComplexityAbstracts)(?:\.[A-Za-z_][A-Za-z0-9_]*)+", module): + raise ValueError(f"Unsupported module: {module}") + relative = Path(module.replace(".", "/") + ".lean") + return root / (Path("abstracts") / relative if module.startswith("ComplexityAbstracts.") + else relative) + + +def module_citations(path: Path) -> list[str]: + """Module citations are discovery context, never inferred theorem/source equivalences.""" + return sorted({key for _, doc in check_hygiene.extract_docstrings(path.read_text()) + for _, key in check_hygiene.docstring_citations(doc)}) + + +def collect(root: Path = ROOT) -> list[dict]: + manifest = json.loads((root / "results/registry.json").read_text()) + if not isinstance(manifest, dict) or manifest.get("schema_version") != 1: + raise ValueError("Unsupported registry schema") + if manifest.get("abstract_catalogue") != "abstracts/catalogue.json": + raise ValueError("The registry must reuse abstracts/catalogue.json") + entries = [] + for abstract in build_abstracts.load_catalogue(root / manifest["abstract_catalogue"], root): + module = abstract["module"] + entries.append({"id": abstract["id"], "title": abstract["title"], + "topic": "selected abstracts", "module": module, + "theorems": abstract["headline_theorems"], "scope": abstract["scope"], + "abstract_id": abstract["id"], "source_review": "module-citations", + "sources": [{"bib_key": key, "locator": None} + for key in module_citations(module_path(module, root))]}) + if not isinstance(manifest.get("results"), list): + raise ValueError("Registry results must be a list") + for entry in manifest["results"]: + if not isinstance(entry, dict) or entry.get("source_review") != "recorded": + raise ValueError("New inventory entries must identify source_review as recorded") + entries.append(entry) + validate(entries, root) + return entries + + +def validate(entries: list[dict], root: Path) -> None: + bib_keys = set(check_hygiene.BIB_KEY_RE.findall((root / "references.bib").read_text())) + ids, declarations = set(), set() + for entry in entries: + for key in ("id", "title", "topic", "module", "scope"): + if not isinstance(entry.get(key), str) or not entry[key].strip(): + raise ValueError(f"Result needs a nonempty {key}") + if not re.fullmatch(r"[a-z0-9]+(?:-[a-z0-9]+)*", entry["id"]) or entry["id"] in ids: + raise ValueError(f"Invalid or duplicate result id: {entry['id']}") + ids.add(entry["id"]) + source = module_path(entry["module"], root) + if not source.is_file(): + raise ValueError(f"Missing result module: {entry['module']}") + if not isinstance(entry.get("theorems"), list) or not entry["theorems"]: + raise ValueError(f"No theorems for {entry['id']}") + for name in entry["theorems"]: + if not isinstance(name, str) or not name or any(c.isspace() for c in name): + raise ValueError(f"Invalid theorem name: {name!r}") + if name in declarations: + raise ValueError(f"Duplicate theorem: {name}") + declarations.add(name) + if not isinstance(entry.get("sources"), list): + raise ValueError(f"Sources must be a list: {entry['id']}") + if entry["source_review"] == "recorded" and not entry["sources"]: + raise ValueError(f"Recorded sources required: {entry['id']}") + seen = set() + for reference in entry["sources"]: + if not isinstance(reference, dict) or reference.get("bib_key") not in bib_keys: + raise ValueError(f"Unknown bibliography reference: {reference!r}") + key = reference["bib_key"] + if key in seen: + raise ValueError(f"Duplicate reference: {key}") + seen.add(key) + locator = reference.get("locator") + if locator is not None and (not isinstance(locator, str) or not locator.strip()): + raise ValueError(f"Invalid source locator: {key}") + + +def validate_constants(entries: list[dict], constants: dict[str, dict]) -> None: + for entry in entries: + for name in entry["theorems"]: + row = constants.get(name) + if not row or row["m"] != entry["module"] or row["k"] != "thm" or not row["e"]: + raise ValueError(f"Not a public theorem defined in {entry['module']}: {name}") + + + +def compiled_constants(entries: list[dict]) -> dict[str, dict]: + modules = sorted({e["module"] for e in entries}) + # Do not certify a renamed/removed declaration from stale local output. CI has already + # built these modules, so this is a cheap freshness assertion rather than another build. + lean_outputs.run(["lake", "build", "--no-build", *modules], capture_output=True) + constants, _ = lean_outputs.load_constants(lean_outputs.DEFAULT_BUILD_DIR, modules) + return constants + +def bibliography_links(root: Path) -> dict[str, str]: + text = (root / "references.bib").read_text() + return {m.group(1): REPOSITORY + "references.bib#L" + str(text.count("\n", 0, m.start()) + 1) + for m in check_hygiene.BIB_KEY_RE.finditer(text)} + + +def markdown(entries: list[dict], root: Path = ROOT, papers: bool = False) -> str: + links = bibliography_links(root) + title = "Referenced works: initial inventory" if papers else "Formalized results: initial inventory" + lines = ["# " + title, "", + "Incomplete coverage. Source locators are recorded from repository documentation,", + "not newly source-verified. Abstract module citations are context, not result mappings.", ""] + groups: dict[str, list[dict]] = {} + for entry in entries: + keys = [r["bib_key"] for r in entry["sources"]] if papers else [entry["topic"]] + for key in keys: + groups.setdefault(key, []).append(entry) + for group, results in sorted(groups.items()): + label = f"[{group}]({links[group]})" if papers else group + lines.extend([f"## {label}", ""]) + for entry in results: + lines.extend([f"### {entry['title']}", "", entry["scope"], ""]) + for name in entry["theorems"]: + if entry["module"].startswith("ComplexityAbstracts."): + source = module_path(entry["module"], root) + line = build_abstracts.declaration_line(source.read_text(), name) + target = REPOSITORY + source.relative_to(root).as_posix() + f"#L{line}" + else: + target = API + entry["module"].replace(".", "/") + ".html#" + quote(name) + lines.append(f"- [`{name}`]({target})") + if entry.get("abstract_id"): + lines.append(f"- [Formal abstract]({API}abstracts/{entry['abstract_id']}.pdf)") + sources = [f"[{r['bib_key']}]({links[r['bib_key']]})" + + (f" ({r['locator']})" if r.get("locator") else " (locator not collected)") + for r in entry["sources"]] + lines.extend(["", f"References ({entry['source_review']}): " + (", ".join(sources) or + "none collected; inspect the abstract and bridge documentation"), ""]) + return "\n".join(lines) + + +def main() -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--compiled", action="store_true", help="require built public theorem metadata") + parser.add_argument("--markdown", action="store_true", help="print the result/topic index") + parser.add_argument("--papers", action="store_true", help="print the index grouped by bibliography key") + args = parser.parse_args() + try: + entries = collect() + if args.compiled: + validate_constants(entries, compiled_constants(entries)) + if args.markdown or args.papers: + print(markdown(entries, papers=args.papers)) + else: + keys = {r["bib_key"] for e in entries for r in e["sources"]} + print(f"{len(entries)} result groups; {sum(len(e['theorems']) for e in entries)} " + f"theorems; {len(keys)} bibliography keys. Coverage/source review remain incomplete.") + except subprocess.CalledProcessError as error: + parser.exit(1, "Registry metadata check failed; build the registered modules first.\n" + + (error.stderr or str(error))) + except (ValueError, OSError, KeyError, TypeError) as error: + parser.exit(1, f"Registry error: {error}\n") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/test_results_registry.py b/scripts/test_results_registry.py new file mode 100644 index 0000000000..a02833210c --- /dev/null +++ b/scripts/test_results_registry.py @@ -0,0 +1,94 @@ +# Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +# Released under Apache 2.0 license as described in the file LICENSE. +# Authors: Christian Reitwiessner +"""Broken-reference regressions for the initial results inventory.""" +import copy +import json +from pathlib import Path +import tempfile +import subprocess +import unittest +from unittest.mock import patch + +import results_registry as registry + + +class RegistryTests(unittest.TestCase): + def setUp(self): + self.temp = tempfile.TemporaryDirectory(prefix="codex-results-registry-") + self.addCleanup(self.temp.cleanup) + self.root = Path(self.temp.name) + (self.root / "Complexity").mkdir() + (self.root / "Complexity/Example.lean").write_text("/-! [Example2026] -/\n") + (self.root / "references.bib").write_text("@article{Example2026, title={An example}}\n") + self.entry = {"id": "example", "title": "A result", "topic": "examples", + "module": "Complexity.Example", "theorems": ["Cslib.example"], + "scope": "One bounded model.", "source_review": "recorded", + "sources": [{"bib_key": "Example2026", "locator": "Theorem 1"}]} + self.constant = {"m": "Complexity.Example", "k": "thm", "e": "axiom"} + + def test_missing_paper_module_and_duplicate(self): + for change in (lambda e: e.update(module="Complexity.Missing"), + lambda e: e["sources"][0].update(bib_key="Missing2026"), + lambda e: e.update(module="Complexity../Example")): + entry = copy.deepcopy(self.entry) + change(entry) + with self.assertRaises(ValueError): + registry.validate([entry], self.root) + with self.assertRaisesRegex(ValueError, "duplicate result id"): + registry.validate([self.entry, self.entry], self.root) + other = dict(self.entry, id="other") + with self.assertRaisesRegex(ValueError, "Duplicate theorem"): + registry.validate([self.entry, other], self.root) + + def test_compiled_rejects_missing_private_definition_axiom_and_wrong_owner(self): + registry.validate_constants([self.entry], {"Cslib.example": self.constant}) + variants = [{}, {"Cslib.example": dict(self.constant, e="")}, + {"Cslib.example": dict(self.constant, k="def")}, + {"Cslib.example": dict(self.constant, k="axiom")}, + {"Cslib.example": dict(self.constant, m="Complexity.Other")}] + for constants in variants: + with self.subTest(constants=constants), self.assertRaises(ValueError): + registry.validate_constants([self.entry], constants) + + def test_stale_output_is_rejected_before_metadata_is_read(self): + with patch.object(registry.lean_outputs, "run", side_effect= + subprocess.CalledProcessError(1, ["lake", "build", "--no-build"])), \ + patch.object(registry.lean_outputs, "load_constants") as load: + with self.assertRaises(subprocess.CalledProcessError): + registry.compiled_constants([self.entry]) + load.assert_not_called() + + def test_abstract_metadata_is_reused_and_citations_are_context(self): + source = self.root / "abstracts/ComplexityAbstracts/ExampleAbstract.lean" + source.parent.mkdir(parents=True) + source.write_text("/-! [Example2026] -/\nnamespace Abstract\n" + "theorem example : True := trivial\nend Abstract\n") + (self.root / "results").mkdir() + (self.root / "results/registry.json").write_text(json.dumps({ + "schema_version": 1, "abstract_catalogue": "abstracts/catalogue.json", "results": []})) + abstract = {"id": "example", "title": "Current catalogue title", "scope": "Current scope", + "module": "ComplexityAbstracts.ExampleAbstract", + "headline_theorems": ["Abstract.example"]} + with patch.object(registry.build_abstracts, "load_catalogue", return_value=[abstract]): + entries = registry.collect(self.root) + self.assertEqual(entries[0]["title"], abstract["title"]) + self.assertEqual(entries[0]["scope"], abstract["scope"]) + self.assertEqual(entries[0]["source_review"], "module-citations") + self.assertEqual(entries[0]["sources"], [{"bib_key": "Example2026", "locator": None}]) + rendered = registry.markdown(entries, self.root) + self.assertIn("abstracts/ComplexityAbstracts/ExampleAbstract.lean#L3", rendered) + self.assertNotIn("ComplexityAbstracts/ExampleAbstract.html", rendered) + + def test_indexes_resolve_declaration_and_bibliography_targets(self): + text = registry.markdown([self.entry], self.root) + self.assertIn("Complexity/Example.html#Cslib.example", text) + self.assertIn("references.bib#L1", text) + self.assertIn("Theorem 1", text) + self.assertIn("not newly source-verified", text) + papers = registry.markdown([self.entry], self.root, papers=True) + self.assertIn("## [Example2026]", papers) + + +if __name__ == "__main__": + unittest.main()