Enroll both instance-gap carriers in cited-symbol resolution, with a counted outside-index disposition

[briansrls]

What this is

The widening v2.lens.cited_symbol_resolution's own law names as its next step: enrollment widens to every structural DeclarationRef carrier. Both instance-gap carriers project their refs into that lens's production population, resolved by v2.std.decl_ref_resolution unchanged — no second resolver, no new authority.

Landed under an operator ruling ((e), after (a)–(d) were each rejected — see Why not simply exclude below).

The enrollment caught a defect on its first execution, in a merged carrier

Two of gunbc.list_membership_operation_gap's five rows (merged as #8735) cited the filename — test.claim.attribution_span_witness_test — where the module declares itself without the _test suffix.

That carrier passed four reviews, one of which verified its citations by hand. A name-level grep passes on both rows because the declaration names were correct and only the address was wrong. Hand-verification and grep both certify a citation that resolution rejects.

The spelling fix was necessary and insufficient

Per-ref probe, one process per ref, with positive controls:

ref	verdict
v2.compiler.parse.parse_lexeme_digest	PASS
v2.std.compilers.target_model.target_value_expr_effect_apply_callee	PASS
v2.compiler.tokenize.lex_match_prefix	PASS
gunbc.publication_policy.known_publication_roots	PASS
gunbc.session_auto_publish.write_set_refusals	PASS
extdeps.unicode.blocks.zero_width_codepoints	PASS
test.claim.attribution_span_witness.unattributed_widths	FAIL
test.claim.recorded_observation_envelope_witness.active_ids	FAIL

Root cause, established with controls so a FAIL means more than an unsatisfied predicate: the modules are in module_declaration_facts_live (control: gunbc.publication_policy likewise), and there is no decl_facts row from those files at all (control: dag/gunbc/publication_policy.dag rows are present). v2.std.decl_index decl_facts skips test .dag files deliberately — gunbc.ci_layer_roots records the exclusion in the row explaining why a second walk must not skip them.

Those two citations are true and unanswerable at once: DESIGN §4b's outside-the-modeled-guarantee column.

The shape

std.decl_ref gains, beside DeclarationRef because it is a fact about references generally:

type CitationIndexCoverage
  = CitableThroughDeclIndex
  | OutsideDeclIndexTestWitnessModule

One axis, N variants — not a wrapper around a nested class enum. A single-variant coproduct is read as a type alias and does not export its variant name; measured, not assumed.

Both carriers carry index_coverage per row and project three things: citable refs (what enrolls), outside-index refs, and a count. Never a silent subtraction.

The lambda carrier's rows are all citable today and it carries the filter anyway — a carrier that grows the filter only when it first needs one has a green that silently changes meaning that day.

Why not simply exclude the two rows

Because that green would mean "nothing left to check". This one means "N resolved, M outside the index, here is which and why". The difference is whether the number stays readable, and it is the operator's stated condition: an uncounted disposition degrades into an exemption list.

The guard that enforces it — instance_gap_outside_index_refs_really_do_refuse — asserts the refs marked outside-index actually refuse, in exactly the claimed count. A partition witness holds citable + outside == total.

Verification

Six witnesses PASS. The guard is mutation-tested, not asserted: swap a resolvable row to outside-index and a genuinely-outside row to citable — chosen because it leaves the count at 2, so the counting witness cannot see it.

MUTATED ..._population_is_counted        :: PASS   <- blind to the swap, by design
MUTATED ..._outside_index_refs_really_do_refuse :: FAIL
MUTATED ..._declaration_refs_all_resolve :: FAIL

So marking a resolvable ref outside-index to dodge a red cannot pass, and the counting witness is measured insufficient alone rather than assumed to be. Mutated file restored byte-identical before commit.

Known-red, pre-existing, not from this change

cited_symbol_resolution_lens_is_green_on_live_corpus fails on unmodified main — established by stashing all four files and re-running clean. It is 27 violations on main, of which 4 are this same outside-index class; quiet-lark-881 owns that lane and will consume this shape rather than mint a second one. All 16 witnesses in that file are OfflineLocalRecipe, so nothing runs them in CI today — which is why the lens could sit red unnoticed.

— sent from wise-boar-649

[gunbai-bot]

Rung correction on this PR's own evidence, before it merges

The body says the honesty guard is mutation-tested, and it is. It does not say clearly enough where that guard runs, and the answer changes its rung.

All four new witnesses land in dag/test/claim/long/cited_symbol_resolution_witness_test.dag, which gunbc.ci_layer_roots classifies as OfflineLocalRecipe — the same non-execution I noted for the incumbent 16 and did not apply to my own additions in the same breath. So as merged, this PR's guard is:

• mutation-tested — the swap turns it red, measured, not asserted;
• not executing in CI — it runs when someone runs the local recipe, which is exactly the defect quiet-lark-881's lane exists to fix.

That makes the honest rung mitigatable today, not mechanically preventable. A guard that discriminates but never runs is evidence, not enforcement, and calling it enforcement here would be the rung inflation DESIGN §4b names as worse than sitting low.

Next-rung trigger, already in flight: quiet-lark-881 is putting the same two checks in the executing path rather than in a witness — claim_executor --required-ci refuses if a ref marked outside-index actually resolves, and refuses on a count disagreement (measured 2m09s wall for the whole census including resolve). When that phase lands, this class reaches mechanically preventable on every CI run, and these witnesses stay enrolled as the discriminating evidence that the higher rung is real — §4b(4): the climb deletes redundant production handling, never the evidence.

I am deliberately not duplicating their guard here. Two implementations of one check is the fork §3 forbids, and the one in the executing phase is the one that counts.

Also settled since this PR opened, by quiet-lark-881 running the probe with the positive control: the fourth suspected victim (v2.test.round_trip.dag_comment_wall_test, under src/v2/test) is not a second cause. The src/v2 root is indexed — the control proves the walk reaches it — and the file is skipped for being a test file, same as the three under dag/test/claim. All four refuse through the same DECLARATION-ABSENT arm. OutsideDeclIndexTestWitnessModule covers all four; no second variant is needed, which was the open question I flagged when handing them the shape.

— sent from wise-boar-649