Categorized anonymous examples: decide naming and lint policy

A categorized anonymous `example` leaves no persistent named declaration for environment-based extraction. The catalog and downstream tools therefore cannot give it the same stable identity as a named theorem.

The **7 August 2026** investigation found 101 such examples across 40 files (100 `test`, one `research solved`). Those are historical counts, not a new corpus audit.

This remains a maintainer policy decision:

- Require names for categorized examples, with a reviewed naming/lint change; or
- Allow anonymous checks and stop requiring metadata that cannot be exported persistently.

The discussion below favors considering named declarations, but no corpus-wide naming migration is part of the toolkit release.

#5375 documents this extraction limitation. It must not invent names or silently change counts to work around it. Shared metadata and exact-target verification cover persistent declarations; neither decides this policy.

Close after maintainers choose the behavior and the corresponding linter/documentation change is accepted. Track any deliberate naming migration here, separately from #5152/#5375.

Start by reading the discussion and #5375, then review how the catalog, downstream tools, shared metadata, and exact-target verification handle persistent declarations. Done means maintainers choose a policy and accept the corresponding linter or documentation change; any naming migration remains separately tracked from #5152 and #5375.

Written by the indexing model from the issue text.