Report duplicate primary Lean-target ownership in autoform audit (duplicate-lean-target) #193

Split out of #143 (phase 1, item 4). #171 delivers the rest of phase 1 and leaves this item out, because it has to follow other open work.

Problem

load_graph rejects duplicate files, node IDs and durable IDs, but nothing reports two articles that both claim primary progress credit for the same Lean declaration. The same declaration can then earn progress credit for both, and neither article is flagged. autoform search (#171) helps an agent avoid creating such a pair; it does not detect one that already exists.

Proposal

Add a duplicate-lean-target finding to autoform audit, as specified in #143:

• Identity is the canonical Lean Name, not its spelling. _root_.Ns.foo, Ns.foo and Ns.«foo» are one declaration.
• Only primary ownership is checked. The first lean: name of an article is primary. Later names are supporting declarations and may recur across articles.
• Repeated names within one article are deduplicated and are not a finding.
• catalog: module inventory occurrences are a separate credit domain and do not conflict with article credit.
• mathlib_declaration gets the analogous check for Mathlib credit.
• The migration/retracted-placeholder exemption stays allowed, and is defined explicitly.

These are the requirements carried forward from draft #127 in the maintainer's comment on #143. #127's hard gate is not to be reused: it compares raw spellings, conflates primary ownership with supporting and catalog occurrences, and misses Mathlib credit.

Blocked on

• Scale roadmap inventories and the full DAG explorer #90 (roadmap inventories).
• The refreshed artifact layer of Bind formalized Lean targets to built artifacts in CI #119.

The maintainer's comment sequences this after both, so that the inventory and article credit domains are stable before the check is written against them.

Acceptance criteria

• autoform audit reports duplicate-lean-target when two articles claim primary credit for the same canonical Lean name, including names that differ only by _root_. or «» quoting.
• The analogous finding fires for duplicate mathlib_declaration credit.
• No finding for: a supporting (non-first) lean: name shared between articles, a catalog: module occurrence, a name repeated within one article, two distinct names, or the documented migration placeholder. Each case has a test.
• The exemption for migration and retracted placeholders is stated in the CLI reference.
• The finding gives no result on the bundled example, with its own test.
• make test, make lint and make check-example pass.

Related

• Add blueprint search and reuse: a description contract, autoform search, and search-before-add rules #143: the proposal this comes from; its acceptance list carries the same criterion.
• Support workspace-global article identity and cross-project dependencies #20: lists the workspace form of this criterion. This issue covers a single blueprint.
• Reject duplicate formalized Lean targets #127: the earlier draft, to be superseded.