Detect duplicate Lean source definitions without selecting private shadows #170

Problem

The lexical Lean source index can keep the wrong occurrence when multiple files use the same written declaration name. A built public declaration may be shadowed in links and impact reports by an earlier unbuilt/private draft occurrence, while verification audits a different compiled declaration.

Draft #140 combined a partial check with unrelated Pages gating. Its obsolete base also leaves an earlier-private/later-public bug: ambiguity is cleared, but the index still returns the private occurrence.

Required contract

• Record every source occurrence relevant to one written declaration name with deterministic path/line diagnostics.
• Select the unique public declaration when private source spellings coexist with it; never retain an earlier private occurrence as the winner.
• Reject genuinely ambiguous public definitions and the private-only ambiguous case with deterministic diagnostics.
• Preserve distinct short names in different namespaces.
• Keep this source-index integrity check separate from article-level primary-ownership detection in Add blueprint search and reuse: a description contract, autoform search, and search-before-add rules #143.
• Ensure render, check, audit, doctor, skeleton, and impact consumers observe the same selected declaration.

Delivery

Rebuild as a focused current-main PR after #165 lands or stack explicitly on it, because both touch the source-index/publication integration. Refresh the bundled example's immutable pin only after the feature is on main.

Provenance: the source-index half of draft #140.

Acceptance

• Regressions cover earlier-private/later-public, later-private/earlier-public, two public definitions, two private-only spellings, and same short name in distinct namespaces.
• Assertions verify the selected declaration path and line, not only that an ambiguity set is empty.
• A generated-project workflow executes the landed duplicate check rather than an older pinned CLI.
• Exact-head focused, full, and generated-example CI pass.