rubrics: penalise hidden infrastructure, process narrative, and blocked dot notation

[kim-em]

Three defect classes turned up across a cleanup pass on TauCeti that no rubric currently catches. Two of them are produced by interactions between existing rubrics rather than by carelessness, which is why they recur.

api-design.md and placement.md: under-exposure is unpenalised. api-design fails an "over-exposed surface" but never an under-exposed one, and licenses private for anything with "no use outside the proof or file it serves". Meanwhile placement makes relocation expensive: update every import, delete the old path, all in one PR. So when a declaration turns out to be too general for the file it landed in, marking it private satisfies api-design and removes it from placement's reach. It is the locally cheapest move and the wrong one.

This is not hypothetical. Twelve files carry an explicit "kept private because…" docstring. The clearest read, before it was fixed:

The quotient by a product of submodules is linearly equivalent to the product of the quotients. This is kept private because the construction is general Mathlib infrastructure; only its Fredholm consequences form the public API of this file.

Mathlib has the setoid and ring-idempotent forms of that statement but no submodule form, so Tau Ceti proved a missing piece of general infrastructure and sealed it, giving its generality as the reason. Another gave the reason as "the general-topology statement belongs upstream rather than in a complex-analysis file" — identifying the correct home and hiding it there instead.

documentation.md: the "why" clause manufactures process narrative. The rubric asks each module docstring to say what lives there "and why", and scope.md requires new material to cite a roadmap target, so authors satisfy the "why" with the roadmap citation. 1370 of 2053 files (67%) now carry roadmap prose naming targets, layers and coordination status with in-flight upstream work, in the one place nothing will ever update it. This is newly fixable because AGENTS.md now mandates a Roadmap: line in every PR description, so the justification has a correct home.

naming.md: no rule for which namespace. The rubric says a name must not be "wrong for its namespace" but never says which namespace a declaration about a Mathlib type belongs in. 1860 of 2053 files open namespace TauCeti; 875 declarations across 168 files thereby block dot notation on a Mathlib type, and 395 files work around it with _root_. The bullet added here is deliberately narrow, excluding the three false-positive classes that a naive reading over-reports by roughly 40%: organisational namespaces, Tau Ceti's own types that share a Mathlib name, and declarations taking no argument of the type.

Five merged PRs have cleared roughly 400 of the 875, and a further round of findings on those PRs came from this angle, so the rule is already being applied by hand — it just is not written down.