# Completed roadmaps

Roadmaps the maintainers have declared complete. Completion is a human judgment against
the roadmap's `README.md`, which is the definitive document; it is never inferred from
`Suggested.lean`, which only records suggested declaration forms for particular milestones
and is not exhaustive.

A declared-complete roadmap is archived here, outside `TauCetiRoadmap/`, so it no longer
appears in the list of active areas offered to contributors (human or AI): the worker
tooling, the issue-template dropdowns, and the root README all enumerate the directories
under `TauCetiRoadmap/` only.

The archived `Suggested.lean` files remain part of the default CI build. They elaborate against
the same Tau Ceti revision as the active roadmaps, so a discharged file continues to certify that
the current library realizes its archived statements. If a Tau Ceti API change breaks such a
certificate without changing the mathematics, the certificate is updated along with the
dependency pin. Git history and each revision's `lake-manifest.json` retain the exact dependency
revision against which an earlier version elaborated.

- [Effective arithmetic bounds and geometry of numbers](EffectiveBounds/README.md)
  (declared complete 2026-07-02)
- [Weighted orthogonal L² bases: completeness, Hilbert bases, and products of orthogonal systems](OrthogonalL2Bases/README.md)
  (declared complete 2026-08-16)
- [Contour integration and the Hungerbühler–Wasem generalized residue theorem](ContourIntegration/README.md)
  (declared complete 2026-08-29)
- [Integral lattices, discriminant forms, and overlattices](IntegralLattices/README.md)
  (declared complete 2026-09-09)