Withdraw the String ProvenUniqueKernelBinding proof: its own emitter contradicts it

[gunbai-bot]

gunbc.rust_source_type_bindings carried the bare-table String row as
ProvenUniqueKernelBinding on a proof that reads, in full, that in a module
importing v2.std.text String every String reference IS the text carrier and
the kernel spelling is unreachable there by construction -- shadowing is the
identity on one token.

Two readers of one environment answer that differently in the shipped emitter,
so it is not established by construction anywhere:

• the type renderer asks per-reference declaration identity, and
  v1.compiler.coercion structural_declaration_modules_for gates the spelling
  to src/v2/std/text.dag and dag/std/string_type.dag, so the reference
  refuses this row and renders the declaration structurally;
• the use-line decision asks v1.compiler.infer_env lookup_type_by_name by
  bare name over the same module environment, gets the KERNEL identity, and
  deletes the pub use -- correct for what IT reads (Kernel-precedence repair: one shared type-env producer; kernel overlay independent of import cardinality #9813, emission follows
  resolution).

Both cannot be resolution's answer. Measured on the XL-0 self-host emit at
base d0009ca, entry src/v2/std/integer.dag (which imports String from
v2.std.text at line 33): the emitted v2_std_integer.rs binds String on no use
or pub use line at all, while siblings from the SAME authored import line
survive -- CharResult, string_head, string_tail -- which is the liveness arm
that makes the absence a measurement rather than a failed import block. The
same file then renders the spelling both ways, and rustc refuses the two call
sites into v2.std.text string_head with expected Rc<Vector> found String.

This is a 4b(1) rung-honesty repair only. The disposition becomes
StillBareNameDebt and the bare row keeps its place either way, so
test.claim.self_host_symbol_identity_binding is unaffected. The trigger names
the CAPABILITY -- one authority for the reference-identity question consumed by
BOTH readers -- not any single call site, because until one reader is derived
from the other the disagreement is authorable wherever the spelling collides.

What survives of the old proof: Symbol was captured because its token differed
from its spelling. That reasoning was sound and is why Symbol is
MigratedToExactBinding. It never generalised to String.

What this does NOT decide: which reader is right. That turns on whether the
.dag application string_head(s: s) is well-typed, which is a separate floor
question. The row is downgraded now because a Proven disposition may not stand
on an argument its own emitter contradicts, whichever way that decision goes.

Co-Authored-By: Claude Opus 5 noreply@anthropic.com
Claude-Session: https://claude.ai/code/session_01Vo22gFeUgs7vAVuhsmWqKk

---

POPULATION, at two grains, because they are different numbers and conflating them overclaims: 299 authored import lists name String from v2.std.text; the 49 E0308 rows are only the subset where the two types are made to MEET at a site rustc reaches. The failing count understates the binding defect and MOVES as the emitted closure widens — 49 is not the population and this PR does not close it.

RESIDUE THIS DOES NOT TOUCH: three declarations still share the spelling String — the kernel scalar, src/v2/std/text.dag:7 and dag/std/string_type.dag:6 — and the last two are a plain DESIGN §3 nickname of each other. That meaning fork is unowned here by ruling (it is the same carrier as #9907's A-vs-B question, which is with the operator).

🤖 Generated with Claude Code

https://claude.ai/code/session_01Vo22gFeUgs7vAVuhsmWqKk

[gunbai-bot]

Closing: SUPERSEDED by #9906, which landed the same correction better and by execution while this was in review.

This PR downgraded the String row to StillBareNameDebt on the ground that its proof was false. #9906 establishes that the VERDICT is right and only its ARGUMENT was inverted — kernel names are never overridden by imports, so a bare String in an importing module is always the kernel; #9906 enumerates all three routes and grounds them on an executed carrier_realization_census fixture rather than on reading precedence. That is a stronger repair than mine and it reaches the opposite disposition, so the downgrade here would be wrong on main.

What my measurement adds is a RESIDUAL that #9906's routes do not account for, and I am recording it here rather than acting on it: in the emitted v2_std_integer.rs at base d0009ca, the parameter of integer_string_to_decimal_digits_step renders as the BARE token String while the same file renders std::string::String elsewhere. Under #9906's route 1 that reference resolves to the kernel and should carry the host spelling in both places. I have not established why it does not, and it is not a reason to move a disposition.

— sent from bold-carp-449