[oxura]

Fixes #1131. Fixes #1247.

name_tt turns a bend2 key into a BendTT identifier, and those identifiers are also the constructor and recursive-group labels. It was not injective in two ways:

• it spelled B.name_key(k), which turns : into ., so an imported ns:name and a local ns.name (distinct since A file's names are keyed ns:name inside the compiler, so no declaration lands in another file's namespace and a foreign CID(None) keeps meaning Base's None (#1045) #1156) got one label (ns:name keys collapse back to ns.name in --verdict, bypassing #1216 #1247);
• it left _ unescaped, so a source name could spell an escape: a-b and a_2d_b both became a_2d_b (BendTT name escaping merges distinct constructor labels across module paths #1131).

Def names were already made unique by fresh; labels were not.

The fix spells the internal key itself, with _ as __ and any other non-name character as _hex_ (whole code points, u flag). Every _ in the output now opens either __ or _hex_, so the spelling decodes to exactly one key. Names without _ (most of Base) are unchanged; Cmp.is_eq becomes Cmp.is__eq.

This is a preventive fix. On current main the known reproducers no longer reach a wrong verdict: #1131's group no longer forms, the #1212 misroute is fixed (#1215), and #1247's case stops at "out of scope". The label collision itself still shows in -o: an imported label_namespace_lib:K and a local label_namespace_lib.K both get .label_namespace_lib.K on main, and .label__namespace__lib_3a_K / .label__namespace__lib.K here. It would matter again the moment a group or a specialized recursion reached the kernel with such names.

The earlier regression tests are dropped: they pass on main too, since a collision only makes the kernel accept more and a #| verdict line cannot see it.

Gates on main 3b3f02e: repo 54/54 (safe.ts 23,994/24k ttok), test 1818/1818, perf 124/124, ping 81/81, safe 1160 agree / 0 false reject / 0 timeout (same as main).

🤖 Generated with Claude Code

[oxura]

Joint verification of #1215, #1216, #1218, #1219 and #1220 against main commit 0187512:

• All five independent PR branches merge cleanly in one octopus merge. Documentation hunks were separated and shared wording shortened so the combined guide stays within the original cap.
• Combined bun gates/repo.ts: PASS 49/49; no caps changed.
• Real Lean 4.34.0-built BendTT kernel accepts all three new positive proof regressions, unchanged vec_safe_lookup, and the five reported grouping/label/model-search witnesses.
• Four runtime regressions produce 5n, 6n, 7n, 204 on interpreter, emitted JS and native C. All four C programs were exercised with AddressSanitizer and UndefinedBehaviorSanitizer; no diagnostics.
• The merged emitted fb3 value passes an added {main == (.False, ()) : Bool} oracle. The corresponding .True oracle fails in the actual kernel, so successful type-checking is not the only evidence of value preservation.
• Kind-only and empty-datatype unsafe dependencies still reject with exit 1 and the expected dependency sets.
• The genuinely required unavailable model rejects promptly; -o explicitly reports no model for reflexive~n as out of scope. Search-limit exhaustion remains fail-closed, not an unchecked placeholder.

The cluster-wide corpus gates were not run; this evidence is the local repository gate, actual CLI/compiler runs and actual kernel checks.

[oxura]

Refreshed the existing branch onto current main f76c251a without rewriting its history. The namespace-identity fix was already in branch head 18fb8fd3, but the PR body had not mentioned #1247; the body/title now describe both bugs. The three punctuation/escape/namespace regressions pass the current real Lean 4.34.0-built kernel, and the repository gate is 50/50. No replacement PR, kernel/core edit or cap change.

[oxura]

Joint verification on main f76c251a with #1216, #1371, #1382 and #1383 combined:

• Repository gate: PASS 50/50.
• Actual current Lean 4.34.0-built kernel accepts the three label regressions plus let_put_depth and the maintainer-extended refined_proof_copy (including walk).
• Paired run of all 94 existing tests/proof/*.bend: both main and the combined branch have 59 successful verdicts, 35 unsuccessful, zero timeouts. No success-to-failure regression. This does not claim that all existing proofs pass.
• Actual CLI IO and emitted JS retain the deep-Array ok result, all 16 Process.run booleans, closed-stdin behavior and the new closure capture outputs. The namespace runtime regression remains 6n on Bun and Node.
• Three native-C emission artifacts are byte-identical before/after the JS lowering change (js_tail_closure, closure_capture_once, shared_match_word).

No physical macOS/GPU/cluster gate claim.