Close six small review leftovers across TCP tests, law citation, and diagnostics

[jasisz]

Six independent review leftovers, one commit.

Fix — dependency-module laws are never admitted when the module name is a reserved Lean token. The admissibility gate reads a dep law's mentions off the emitted statement, where every path segment carries the reserved-token guard (Type'.qrev), but the membership index, the simp-orientation program-fn set, and the citation name were all built from the raw module prefix (Type.qrev). Nothing matched, the mention set came back empty, and the law silently degraded to not-admitted — no theorem emitted, no citation in the consumer. Measured on the split probe from cross_file_consumer_proves_via_dep_law with Lib renamed to Type: before, Type'.lean carried no law theorem and Consumer.lean no citation; after, both match the Lib-named fixture and the consumer keeps its universal credit. Output for ordinary module names is byte-identical (verified by diffing the whole emitted project). New test cross_file_reserved_module_name_dep_law_is_admitted_and_cited is red before the change.

Also:

• New wasip2 regression wasip2_tcp_close_without_connect_keeps_the_close_helper: a function taking an existing Tcp.Connection that declares only ! [Tcp.close], with no Tcp.connect in the program, must compile with the close helper present. Red when the shared parse_id gate is narrowed to exclude TcpClose.
• Comment refresh in the generated-Rust backend: the borrow-overlap branch cited value - highNibble(value) * 16, which no longer exists in the standard library. Now cites n * factorial(n - 1), confirmed by instrumenting the branch against examples/core/big_integers.av, examples/formal/recursive_monotone.av, and examples/games/eggcatch/core.av.
• The Lean token-table guard test retries the probe once when it dies fetching the pinned toolchain. Any other probe failure, and every token-table mismatch, still fails on the first attempt.
• Documented the stdlib-shadow suppression asymmetry (structured finding honours [[check.suppress]], loader stderr warning does not) in docs/diagnostics-slugs.md and at the warning site.
• New test asserting the loader's stdlib-shadow warning is printed exactly once per command; without the dedup aver check --deps prints it four times.

Tests: proof_spec (232), wasip2_codegen_regression --features wasip2 (7), stdlib_spec (4), --lib (976), rust_codegen_regression, eval_spec, compile_spec — all green. cargo fmt; cargo clippy --all-targets and --features wasm,wasip2 clean on touched files.

🤖 Generated with Claude Code