Depend on Tau Ceti and include it in novelty review

[Vilin97]

Make Tau Ceti available as a pinned Lake dependency, so pool projects can import its modules instead of vendoring projects already in Tau Ceti or Mathlib. Pin TauCetiProject/TauCeti at 5189e8a380bdf5740cc1fe4123cc9cbe635724c2 and update both root and documentation manifests. Mathlib remains at v4.35.0-rc3, and its transitive dependency pins take precedence.

Extend novelty review to compare against Mathlib, Tau Ceti, and the pool. Text-only reviewers receive current Tau Ceti module-path candidates and bounded source excerpts at the inventory commit, including immutable permalinks. The rubric requires an actual declaration before blocking and treats keyword gaps, failed fetches, truncated inventories, and omitted source as unchecked rather than proof of novelty. Update contributor guidance accordingly.

Validation: upstream TauCeti.RepresentationTheory.Lie.Ado.CharacteristicZero builds successfully against Lean Pool’s unchanged Lean/Mathlib pins (2790 jobs); lake exe mk_all --check, Lake resolution, and documentation manifest update succeed; Ruff lint and format checks pass; the full Python suite passes 533 tests with two skipped. A local sysctl-backed nproc shim supplies the Linux utility expected by existing profile tests on macOS. A live GitHub lookup includes the upstream Ado theorem statement. Root and documentation manifests preserve every existing package pin byte-for-byte at the parsed entry level. No CI or lint gate is changed.

Separate content removal: #594. The six automation prompts were updated, merged, and deployed independently in Vilin97/lean-pool-automation#1.

The pinned production worker can supply the PR base SHA so newly accepted projects are not mistaken for new claims against an older engine checkout. Both successful and unavailable base lookups have regression coverage. The deployed worker integration is Vilin97/lean-pool-automation#2.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[High risk] Adds a new Lake dependency and integrates it into the review process.

The PR appears safe to merge; no blocking finding remains.

Summary

Adds Tau Ceti as a pinned Lake dependency and includes its source declarations in novelty review.

• Root and documentation manifests use the same Tau Ceti revision.
• Novelty guidance treats missing or omitted evidence as unchecked.
• Changes since the previous review limit optional Tau Ceti requests to 15 seconds and cover timeout failures.
• Both numbered previous findings are addressed. No new actionable issues were found.

_{Reviews (4) · Last reviewed commit: "Bound optional Tau Ceti review lookups" · Reviewed by Greptile}

[Vilin97]

Independent source review of PR595 at c1ff75a624653e0de248d9efe46f2d9397902f6b.

I reviewed the twelve-file change against main 68aa6ee and applied a small runtime repair in c1ff75a6. The new optional Tau Ceti commit, inventory and source requests now have a 15-second timeout. Inventory timeouts produce an explicit “prior art unchecked” notice; a source timeout leaves that statement unchecked and allows later candidates to be inspected. Existing run_gh callers retain their original subprocess arguments.

Validation: 21 focused tests passed in 0.95s without network requests. The published files differ from the tested version only in signature formatting, with complete AST equality for all three modules. Ruff check and format check pass for all three files using the repository’s canonical paths and unchanged configuration. The branch update preserves its previous parent and modifies only the helper, review.py, and the focused tests; all three published blobs were read back byte-for-byte.

The novelty lookup uses immutable source revisions, keeps lexical candidates distinct from verified theorem matches, and records incomplete evidence as unverifiable. The additional corpus intentionally changes the scope of novelty review. Existing package pins and lint settings are preserved alongside the new pinned dependency. I have not independently reproduced the PR body’s full upstream-build or Python-suite counts.

The timeout finding is resolved in this source scope. Full dependency/build validation and required checks must pass at the new head. Integration remains held under the infrastructure-priority assignment until current-main CI is verified green.