Depend on Tau Ceti and include it in novelty review

.github/REVIEW_RULES.md

@@ -2,7 +2,7 @@
 
 You are reviewing a pull request to **Lean Pool**, a curated repository of formalization projects sitting between mathlib (very high human-review bar) and merely-true (anything that compiles). The pool is mathematics **and related disciplines** — about a quarter of it is theoretical computer science, information theory, mathematical physics, and game theory, each judged by its own field's standards.
 
-A project PR is reviewed on **five dimensions, each by its own independent review**: faithfulness (does the Lean prove what the card claims), novelty (is it already in Mathlib or the pool), significance (is it worth having), sources (does the citation hold up), and code quality (advisory). Each review sees only its own rubric, appended below this shared core. Stay inside your rubric's dimension: the others are someone else's job, and strength on their dimension must not soften yours.
+A project PR is reviewed on **five dimensions, each by its own independent review**: faithfulness (does the Lean prove what the card claims), novelty (is it already in Mathlib, Tau Ceti, or the pool), significance (is it worth having), sources (does the citation hold up), and code quality (advisory). Each review sees only its own rubric, appended below this shared core. Stay inside your rubric's dimension: the others are someone else's job, and strength on their dimension must not soften yours.
 
 The overall verdict is **computed, not asked of you**: any blocking rubric verdict yields `request_changes`, any `discuss` yields `needs_discussion`, and a review of an elided (partial) diff cannot yield `approve`. Your job is your dimension's verdict, its few structured fields, and findings with evidence.
 

.github/review-rubrics/novelty.md

@@ -1,23 +1,24 @@
 # Rubric: novelty — is it already done?
 
-You are reviewing **one dimension** of this PR: whether its headline results already exist in Mathlib or in the pool. Faithfulness, significance, sources, and code quality are judged by separate reviews — do not spend words on them, and however good the Lean is, good Lean is not a reason to keep a duplicate.
+You are reviewing **one dimension** of this PR: whether its headline results already exist in Mathlib, Tau Ceti, or in the pool. Faithfulness, significance, sources, and code quality are judged by separate reviews — do not spend words on them, and however good the Lean is, good Lean is not a reason to keep a duplicate.
 
 This dimension has been missed at real cost: #275 was approved with zero findings and closed by hand because its headline follows in a few lines from Mathlib's `SimpleGraph.nonempty_hom_of_forall_finite_subgraph_hom`, and #225 was closed as subsumed by the pool's own `Incompleteness` project.
 
 ## What to judge
 
-A **Prior art** section above the diff carries a Mathlib search for every headline this PR adds, plus the complete list of pooled projects. Work from it:
+A **Prior art** section above the diff carries a Mathlib search for every headline this PR adds, a bounded Tau Ceti module-path search with source excerpts, and the complete list of pooled projects. Work from it:
 
 - For each headline, read the search hits against the claim. A hit is a *candidate*, not a verdict — shared vocabulary is not duplication. Check what the hit's declaration actually says before calling anything a duplicate, and name the declaration when you do.
+- Compare every headline against Tau Ceti as well as Mathlib. Read the supplied Tau Ceti source declarations, including their hypotheses and conclusion; a roadmap or module title alone is not proof of a duplicate. Name the existing declaration when blocking. Tau Ceti keyword candidates are incomplete: no lexical match, a failed source fetch, or omitted source means that comparison is unchecked, never evidence of novelty. Say `unverifiable` where the statements supplied do not settle it.
 - Compare against the pool list the same way. Prior art in the pool counts the same as prior art in Mathlib.
-- If the section says the search ran and nothing matched, that is genuine evidence of novelty — say so and leave `already_formalized` empty. If it says the search did not run or failed for a headline, prior art for that headline is *unchecked*: say `unverifiable` in your prose, and never write it into `already_formalized`, which holds a bare declaration name or nothing.
+- If the section says the search ran and nothing matched, that is evidence only for the corpus actually searched, not a settled Tau Ceti comparison — say so and leave `already_formalized` empty. If it says the search did not run or failed for a headline, prior art for that headline is *unchecked*: say `unverifiable` in your prose, and never write it into `already_formalized`, which holds a bare declaration name or nothing.
 
 Not every overlap is duplication. A different proof of a known theorem, a sharper constant, a generalization, or a restatement in a genuinely different setting can all be worth having — distinguish, and say precisely what is new. A project that extends or strengthens a pooled project is a judgment call for the maintainer, not an automatic reject.
 
 ## Verdict
 
 - `pass` — the headlines are not already formalized, or the overlap is a genuine extension you have named.
-- `block` — a headline result is already in Mathlib or the pool, named declaration in hand.
+- `block` — a headline result is already in Mathlib, Tau Ceti, or the pool, named declaration in hand.
 - `discuss` — real overlap that is arguably an extension, or prior art you suspect but cannot pin to a declaration.
 
 ## Output
@@ -28,13 +29,13 @@ Return a single JSON object:
 {
   "verdict": "pass" | "block" | "discuss",
   "bottom_line": "<one sentence for the maintainer>",
-  "already_formalized": "<the Mathlib or pool declaration that already proves a headline — a bare declaration name and nothing else; EMPTY if none found or unchecked>",
+  "already_formalized": "<the Mathlib, Tau Ceti, or pool declaration that already proves a headline — a bare declaration name and nothing else; EMPTY if none found or unchecked>",
   "novelty_note": "<one sentence: what is new here relative to the closest existing work, or what duplicates what>",
   "findings": [
     {
       "file": "<repo-relative path, or empty if PR-wide>",
       "line": <int, post-change line; 0 if not file-specific>,
-      "rule": "<e.g. 'duplicate-of-mathlib', 'duplicate-of-pool', 'partial-overlap'>",
+      "rule": "<e.g. 'duplicate-of-mathlib', 'duplicate-of-tauceti', 'duplicate-of-pool', 'partial-overlap'>",
       "comment": "<what duplicates what, and what if anything is still new>",
       "evidence": "<the existing declaration name and what it states>"
     }

AGENTS.md

@@ -15,7 +15,7 @@ This file is a concatenation of README.md and CONTRIBUTING.md.
 [![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.20513444.svg)](https://doi.org/10.5281/zenodo.20513444)
 [![arXiv](https://img.shields.io/badge/arXiv-2609.25199-b31b1b)](https://arxiv.org/abs/2609.25199)
 
-Lean Pool sits between [`mathlib`](https://github.com/leanprover-community/mathlib4) and [`merely-true`](https://github.com/merely-true/merely-true), preserving Lean 4 formalizations that don't fit mathlib's scope. Instead of mathlib's high-bar human review, it relies on deterministic linters and LLM judgment, so it can grow faster while staying `sorry`-free and pinned to the latest Mathlib. See [`MOTIVATION.md`](MOTIVATION.md) for the why, browse the API docs at <https://leanpool.github.io/lean-pool/>, and explore each project's dependency graph and declarations in the [exposition site](https://leanpool.github.io/lean-pool/exposition/).
+Lean Pool sits between [`mathlib`](https://github.com/leanprover-community/mathlib4) and [`merely-true`](https://github.com/merely-true/merely-true), preserving Lean 4 formalizations that don't fit mathlib's scope. Instead of mathlib's high-bar human review, it relies on deterministic linters and LLM judgment, so it can grow faster while staying `sorry`-free and pinned to the latest Mathlib. Tau Ceti is also a pinned Lake dependency; import its modules directly instead of vendoring projects already in Tau Ceti or Mathlib. See [`MOTIVATION.md`](MOTIVATION.md) for the why, browse the API docs at <https://leanpool.github.io/lean-pool/>, and explore each project's dependency graph and declarations in the [exposition site](https://leanpool.github.io/lean-pool/exposition/).
 
 Semantic search is also available via the [API](https://search.octo.axiomatic-ai.com/api/search).
 
@@ -107,6 +107,11 @@ If you would like to withdraw your project from Lean Pool, open an issue.
 
 ## Submitting a project
 
+Do not vendor projects that are already in TauCeti or Mathlib. Both are Lake
+dependencies: reuse their modules directly, and submit independent formalizations
+or substantive extensions instead. Novelty review compares against Mathlib, Tau
+Ceti, and the pool.
+
 There are two paths:
 
 - **Propose a repo.** Open an issue with the GitHub URL and a maintainer can import it. Repos that Reservoir does not index can be added to [`candidates/manual.txt`](candidates/manual.txt).

CLAUDE.md

@@ -15,7 +15,7 @@ This file is a concatenation of README.md and CONTRIBUTING.md.
 [![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.20513444.svg)](https://doi.org/10.5281/zenodo.20513444)
 [![arXiv](https://img.shields.io/badge/arXiv-2609.25199-b31b1b)](https://arxiv.org/abs/2609.25199)
 
-Lean Pool sits between [`mathlib`](https://github.com/leanprover-community/mathlib4) and [`merely-true`](https://github.com/merely-true/merely-true), preserving Lean 4 formalizations that don't fit mathlib's scope. Instead of mathlib's high-bar human review, it relies on deterministic linters and LLM judgment, so it can grow faster while staying `sorry`-free and pinned to the latest Mathlib. See [`MOTIVATION.md`](MOTIVATION.md) for the why, browse the API docs at <https://leanpool.github.io/lean-pool/>, and explore each project's dependency graph and declarations in the [exposition site](https://leanpool.github.io/lean-pool/exposition/).
+Lean Pool sits between [`mathlib`](https://github.com/leanprover-community/mathlib4) and [`merely-true`](https://github.com/merely-true/merely-true), preserving Lean 4 formalizations that don't fit mathlib's scope. Instead of mathlib's high-bar human review, it relies on deterministic linters and LLM judgment, so it can grow faster while staying `sorry`-free and pinned to the latest Mathlib. Tau Ceti is also a pinned Lake dependency; import its modules directly instead of vendoring projects already in Tau Ceti or Mathlib. See [`MOTIVATION.md`](MOTIVATION.md) for the why, browse the API docs at <https://leanpool.github.io/lean-pool/>, and explore each project's dependency graph and declarations in the [exposition site](https://leanpool.github.io/lean-pool/exposition/).
 
 Semantic search is also available via the [API](https://search.octo.axiomatic-ai.com/api/search).
 
@@ -107,6 +107,11 @@ If you would like to withdraw your project from Lean Pool, open an issue.
 
 ## Submitting a project
 
+Do not vendor projects that are already in TauCeti or Mathlib. Both are Lake
+dependencies: reuse their modules directly, and submit independent formalizations
+or substantive extensions instead. Novelty review compares against Mathlib, Tau
+Ceti, and the pool.
+
 There are two paths:
 
 - **Propose a repo.** Open an issue with the GitHub URL and a maintainer can import it. Repos that Reservoir does not index can be added to [`candidates/manual.txt`](candidates/manual.txt).

CONTRIBUTING.md

@@ -8,6 +8,11 @@ If you would like to withdraw your project from Lean Pool, open an issue.
 
 ## Submitting a project
 
+Do not vendor projects that are already in TauCeti or Mathlib. Both are Lake
+dependencies: reuse their modules directly, and submit independent formalizations
+or substantive extensions instead. Novelty review compares against Mathlib, Tau
+Ceti, and the pool.
+
 There are two paths:
 
 - **Propose a repo.** Open an issue with the GitHub URL and a maintainer can import it. Repos that Reservoir does not index can be added to [`candidates/manual.txt`](candidates/manual.txt).

README.md

@@ -13,7 +13,7 @@
 [![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.20513444.svg)](https://doi.org/10.5281/zenodo.20513444)
 [![arXiv](https://img.shields.io/badge/arXiv-2609.25199-b31b1b)](https://arxiv.org/abs/2609.25199)
 
-Lean Pool sits between [`mathlib`](https://github.com/leanprover-community/mathlib4) and [`merely-true`](https://github.com/merely-true/merely-true), preserving Lean 4 formalizations that don't fit mathlib's scope. Instead of mathlib's high-bar human review, it relies on deterministic linters and LLM judgment, so it can grow faster while staying `sorry`-free and pinned to the latest Mathlib. See [`MOTIVATION.md`](MOTIVATION.md) for the why, browse the API docs at <https://leanpool.github.io/lean-pool/>, and explore each project's dependency graph and declarations in the [exposition site](https://leanpool.github.io/lean-pool/exposition/).
+Lean Pool sits between [`mathlib`](https://github.com/leanprover-community/mathlib4) and [`merely-true`](https://github.com/merely-true/merely-true), preserving Lean 4 formalizations that don't fit mathlib's scope. Instead of mathlib's high-bar human review, it relies on deterministic linters and LLM judgment, so it can grow faster while staying `sorry`-free and pinned to the latest Mathlib. Tau Ceti is also a pinned Lake dependency; import its modules directly instead of vendoring projects already in Tau Ceti or Mathlib. See [`MOTIVATION.md`](MOTIVATION.md) for the why, browse the API docs at <https://leanpool.github.io/lean-pool/>, and explore each project's dependency graph and declarations in the [exposition site](https://leanpool.github.io/lean-pool/exposition/).
 
 Semantic search is also available via the [API](https://search.octo.axiomatic-ai.com/api/search).
 

docbuild/lake-manifest.json

@@ -79,6 +79,16 @@
    "inputRev": "v4.35.0-rc3",
    "inherited": true,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/TauCetiProject/TauCeti",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "5189e8a380bdf5740cc1fe4123cc9cbe635724c2",
+   "name": "TauCeti",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "5189e8a380bdf5740cc1fe4123cc9cbe635724c2",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,

lake-manifest.json

@@ -11,6 +11,16 @@
    "inputRev": "v4.35.0-rc3",
    "inherited": false,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/TauCetiProject/TauCeti",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "5189e8a380bdf5740cc1fe4123cc9cbe635724c2",
+   "name": "TauCeti",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "5189e8a380bdf5740cc1fe4123cc9cbe635724c2",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,

lakefile.toml

@@ -10,6 +10,12 @@ relaxedAutoImplicit = false
 weak.linter.mathlibStandardSet = true
 maxSynthPendingDepth = 3
 
+[[require]]
+name = "TauCeti"
+git = "https://github.com/TauCetiProject/TauCeti"
+rev = "5189e8a380bdf5740cc1fe4123cc9cbe635724c2"
+
+# Keep Mathlib last so its transitive dependency pins take precedence.
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"