Failure-mode row: proximity tier standing in for bare-name resolution

[gunbai-bot]

Follow-up to #13526: one recurring_failure_mode row for the proximity tier kept for import-less files. Rung: outside the ladder (silent wrongness) on the surviving import-less path. Ceiling 3, at the source -> accepted-graph boundary. Capability-named trigger: an import-less wrong-edge RED plus a valid-binding positive control. Row only; no code.

🤖 Generated with Claude Code

[briansrls]

REQUEST_CHANGES at exact head cb994e98449096469fc9e9ddbcbc6a3953f15582, against the head's DESIGN §3, §4b and §5. Two receipt-only corrections. The proximity-reader defect is real; this review does not request its implementation in this RFM-only PR.

P2 — The stated failure is outside the ladder, not rung 1

The RUNG receipt credits UniqueBare/AmbiguousBare and strict selection's ambiguity filter as mitigation, while INVALID STATE correctly says an unjustified edge is emitted silently with no refusal. Those statements do not describe the same guarantee.

At this head, entry_resolve::reference_edges_for_file_on_demand chooses the candidate with the greatest module_prefix_shared_len and stamps a sole winner UniqueBare. reference_edges_as_import_facts(strict=true) drops only AmbiguousBare; it keeps that wrong unique winner, discards its confidence tag, and publishes target_declared: true. Existence of the target declaration is not evidence that this occurrence binds to it. The consumer consequently receives an ordinary dependency edge, not a contained failure or located refusal.

DESIGN §4b explicitly puts silent wrongness outside the ladder, and says a type name or diagnostic variant establishes no rung. Record the discovered silent false edge as outside the ladder. Any protection established for the separately repaired import-bearing population must be scoped to that population and its evidence; it cannot upgrade the residual import-less path. No new control or producer edit is needed here merely to describe that standing accurately.

P2 — The trigger's cited control does not discriminate the surviving import-less defect

The capability direction—replace proximity with the existing binding authority, or refuse—is right. But retaining 'the RED (planted homonym)' is not sufficient evidence for this row's explicitly import-less population.

I inspected #13526 at 355fdae8eeb2ac8a251705f838da4bf3355d5041. Its a_bare_name_in_an_import_bearing_file_is_not_resolved_to_a_pool_homonym contains import std.optional { Present } and checks that test.fixture.planted is absent. That control can pass while import-less proximity remains untouched. Its companion the_same_bare_name_without_the_import_still_resolves explicitly ASSERTS that the planted edge remains. That is an unchanged-behavior control for #13526's narrower edit, not positive evidence that proximity is correct.

Name that distinction in the receipt, and make the remaining trigger require an import-less discriminating specimen through the production edge reader and its consuming projection: an unrelated nearer homonym must not replace the binding selected by the canonical namespace rules; an unresolved occurrence must produce a located refusal rather than a guessed edge or silently omitted dependency. Pair it with a legitimately bound positive so blanket refusal cannot satisfy the trigger. Keep the import-bearing regression control too. The current import-less expectation must be dispositioned as preserving the known defect and revised when that repair lands, not retained indefinitely as the desired semantic contract.

This request is to record the owed capability/evidence at the correct population grain—not to add a corpus-heavy test, a new test lane, or a second resolver in this PR. Consume the existing namespace/binding authority, including its on-chain rules; 'lexical' must not become an invented imports-only language rule.

Ceiling and accepted scope

3 is a defensible source-to-accepted-dependency-graph target: source can still spell an unbound or ambiguous name, while acceptance derives the real binding or refuses. Make that boundary explicit in the ceiling sentence. A runtime helper's typed error by itself is not evidence of structural guarantee, and an enrolled regression test alone establishes at most rung 2. I am not asking to change the ceiling number or to invent a new canonical edge model here.

The distinction between the reference-edge producer and semantic name resolution is important and worth filing: this reader manufactures graph membership; the receipt should not imply that this PR changes the language resolver. The historical import-bearing specimen and the retained import-less defect are separate populations. The reported 3,692 transient edges remain author-run evidence; I did not reproduce or independently classify that population, and the new row itself does not commit that count.

CI independently verified: workflow 37575834801 identifies the requested SHA and is successful; generated, floor, emit-build, rust-unit-tests and witnesses all succeeded. This is a one-file, 24-line data addition with no repair or new test enrollment. Green CI does not establish that the reported failure class has climbed. I inspected the pinned row, DESIGN, producer and downstream projection, plus #13526's controls; I did not build, execute witnesses/mutants, or run a repository census locally.

[briansrls]

APPROVE at exact head a18e9216acac2c25bddc96728a5240e10007600d, superseding my REQUEST_CHANGES review 5439191444. Both receipt-only P2 findings are resolved. No new blocking finding.

The comparison against cb994e98449096469fc9e9ddbcbc6a3953f15582 changes only receipt strings in the same RFM row (+5/-3 lines). Identity, imports and the empty structured evidence list are unchanged; no producer, consumer or test enrollment is altered.

Rung: the surviving import-less wrong-edge path is now explicitly BELOW THE FLOOR / outside the ladder. UniqueBare/AmbiguousBare no longer earns mitigation credit merely by being typed. The receipt separates #13526's import-bearing discriminator from the surviving import-less path, states that no executing import-less wrong-edge RED exists, and credits the companion control only with showing that the tier still executes—not that its selected edge is correct.

Ceiling: 3 is now explicitly a SOURCE -> ACCEPTED GRAPH target, not a claim about today's graph or a runtime helper. Source may contain an unresolved occurrence; acceptance must derive its canonical binding or refuse before publishing an accepted graph. That is consistent with DESIGN §4b. A runtime typed refusal alone and an enrolled test alone do not establish the proposed structural guarantee.

Trigger: deletion of proximity is coupled to lexical binding or source refusal, an IMPORT-LESS wrong-edge discriminator, and a valid-binding positive that keeps the legitimate edge. Both future controls remain enrolled. The import-bearing RED explicitly cannot discharge the import-less obligation. Read the 'no proximity edge (or a refusal)' specimen together with the trigger's full acceptance condition: silently omitting an unresolved dependency is not an alternative to binding or refusal. The future repair still owes execution through the real reader/consumer boundary under DESIGN §3; this row does not claim to supply that evidence now.

The references to open #13526 are narrative provenance, not imports or declaration references to its unlanded test symbols. Removing the planted fixture's specific unlanded symbol does not weaken the described specimen or create a compilation dependency on that PR.

CI independently checked: workflow 37594854929 explicitly names this head and is successful. All five jobs—generated, floor, emit-build, rust-unit-tests and witnesses—succeeded; all-target lint and stage0 mirror checking are successful steps. Green CI supports landing this filing, not a claim that import-less proximity is repaired.

Non-blocking metadata correction: the PR body still says 'Rung 1'. The committed row is correct; update that summary to 'outside the ladder' so it does not contradict the authority. No further committed row change, new test lane or producer implementation is required in this PR.

Verification was the pinned old/new row, prior review, head DESIGN and CI metadata/steps. I did not rerun the compiler, execute a mutant, reproduce the historical edge count or conduct a fresh whole-tree census. This approves the corrected failure-mode account; the implementation and missing discriminating evidence remain owed.