A name collision that resolves per-entry and refuses whole-corpus: a lens for the check the gate can make and the author cannot

[gunbai-bot]

Independent of my emission-ratchet stack. Branched off main, and it exists because of a defect that stack hit.

The class

Two modules declaring one bare name is not an error at either declaration. It becomes an error at a call site, and only under a closure containing both declarers.

• gunbc compile --entry <caller> contains one declarer → the call resolves, the entry reports 0 blocking.
• The floor's whole-corpus preparation contains both → the same call fails to resolve.

So the class is invisible to the check an author naturally runs and visible only to the one that gates. The cheap check cannot see it; the check that can costs a CI round trip.

Measured specimen (2026-08-25, #9213, run 32896104450): dag/tools/frontier_ingestion_probe declares roster_identity; a second module declared the same name over a different subject returning a different type. Per-entry compile: clean. Floor: function 'roster_identity' not found in scope.

And the diagnostic does not say what happened — two declarers and zero declarers arrive as the same message, which is state-space conflation: different states, opposite remedies (rename one of two authorities / write the missing one), rendered identically. That is why the lens reports the peer declarers rather than the bare fact of a fork.

What this is

gunbc.bare_name_fork_lens — a pure reader over decl_facts, storing nothing — plus one entry point:

gunbc run --source-root dag --source-root src/v2 \
  --entry dag/tools/bare_name_fork_check.dag --function check --arg subject=<rel path>

Scoped to one subject module: do the names this module declares already have a declarer elsewhere. Deliberately not a corpus-wide collision census — that is a different artifact with a different cost, and a count would not be the valuable part anyway.

Three properties that keep it from being a decoration

An unread subject refuses. If the subject path contributes no declarations — mistyped path, file outside the roots, module the index could not classify — the verdict is SubjectContributedNoDeclarations, not clean. A lens whose only failure mode is found something reads clean whenever it could not read at all: the strongest verdict from the weakest observation, and the one shape that would make this worse than absent.

The coverage bound is declared and printed on the clean arm. decl_facts carries top-level declarations. A coproduct's variant arms are bare names that can also fork, and they are not in this population. So a passing run states what it did not check, with the next-rung trigger named — variant constructors carried as their own facts, at which point the bound is deleted rather than widened here.

The pure core reads a projection, not DeclFact. DeclFact carries a Node, so every fixture over it would have to mint a syntax node in order to say something about a name — a fixture that expensive is one nobody writes, which is how a lens ends up with a host call and no evidence. The host boundary projects once; the nine claims below it are hermetic and authored.

Two constraints recorded in the carrier, not here

Both are stated in the .dag source rather than the PR body, since a PR body does not survive the merge.

(a) It is not wired into floor witness discovery, and the entry point says why: two corpus-wide censuses were deleted from there in August for exactly this cost shape — the unit of computation was the whole corpus, the unit of fact was one module's declarations, and every consumer that wanted a witness roster paid for a whole-corpus module graph.

(b) It is the interim, not the terminal. The terminal answer is that a declaration fact belongs on the module's own declaration, checked at ingestion where the module is parsed anyway. This lens is the corpus-wide reconstruction that trigger exists to retire, and saying so here is what stops it being cited later as the finished thing.

Evidence

Both entries compile with 0 blocking; all nine claims execute, joined declared-against-PASS.