Follow-up to the tag-discriminating coherence key (debt #32, landed b1334df):
close the annotation-path miss the coordinator's end-to-end probe surfaced, and
land the blocked RUNTIME proof.

ROOT CAUSE of the annotation-path miss. `value_slot_tag` (the lift's
bare-variant→ConstValue::Tag rule) WAS reached and resolved correctly, but a
SECOND, independent pass — `param_args::check_type_expr`, the value-parameter
argument-form validator — fires **E0742** ("USD is not a literal") on ANY node
in a value slot, walking the CST directly and never consulting the tag rule. So
every `let a: Money<USD>` annotation (and turbofish) was rejected before the lift
mattered, cascading E0728/E0718. The fix: `check_type_expr` now asks the SAME
`value_slot_tag` predicate — a bare (or declared-type-qualified) nullary variant
of the parameter's declared `data` type is a concrete tag, legal; only a genuine
non-literal (a binder `n`, a type `Int`) still fires E0742. `value_slot_tag` also
gained the qualified `Currency::USD` spelling (verified by the declared type's
name), so both spellings work in every type-annotation and turbofish position.

RUNTIME PROOF (`tests/corpus/tag_dispatch`, exit 42, freestanding, in
RUNTIME_TESTED). `newtype Money<currency: Currency> = i64` with `data Currency {
USD, EUR }`; a local `trait Code<T>` with `impl Code<Money<USD>> { … = 20 }` and
`impl Code<Money<EUR>> { … = 22 }`. `main` CONSTRUCTS `Money::<USD>(0)` /
`Money::<EUR>(0)` and dispatches `a.code()`→20, `b.code()`→22 — each routed by
the concrete tag in the operand's type. A mis-route flips the exit (EUR→USD gives
20→exit 2; USD→EUR gives 22→exit 1). Green 42 IS the discrimination, end to end.
Before the tag-discriminating key both impls keyed as `Money` and collided.

Two UNRELATED gaps found and worked around (reported, not fixed here — outside
debt #32/#37):
  1. Cross-module trait-impl resolution: an app module cannot `impl Add<…>` for
     a stdlib-Prelude trait — `Add` does not resolve in the app scope
     (`register_impl`'s `lookup_trait` misses), so the impl silently drops. The
     proof uses a LOCAL trait `Code` (same-module → resolves), exercising the
     identical tag-dispatch mechanism.
  2. `.value` on a SCALAR-rep newtype (`= i64`): the newtype convention (a2901fd)
     only registers component fields for a `(| … |)` tuple rep, so `.value` on a
     scalar-rep newtype is E0718. The proof returns discriminating constants from
     the impl bodies, so it needs no `.value`.

Gates: fmt clean; clippy -D warnings clean; build clean; workspace suite — only
the 3 pre-existing reds (one_equals_two, strings_differ canaries + the
tensor_* runtime-coverage red, all present at a2901fd, none mine); architecture
22/22 (check_type_expr's tag arm extracted to `check_value_slot_node`, the test
helper split to `insert_money_over_currency`, the registry row kept terse — all
under R3/R4); conformance ratchet ≤94 (2 passed, not loose); stdlib_type_clean
green; tag_dispatch_run green (exit 42).

@@ -0,0 +195,4 @@
+            .is_ok_and(|s| s.success());
+        assert!(ok, "failed to build the `ckc` binary");
+    });
+    find_near_exe("ckc").expect("`ckc` binary next to the test executable")

@@ -0,0 +130,4 @@
+}
+
+/// `nm <binary>` output (all symbols; scanned for forbidden libc/`ck_rt` names).
+fn nm_all(binary: &Path) -> String {

@@ -623,0 +623,4 @@
+    let tag_name = match segments.as_slice() {
+        [tag] => *tag,
+        [head, tag] if *head == interner.resolve(interner.type_data(parent).name) => *tag,
+        _ => return None,