Retire std.string_type String: delete dag/std/string_type.dag (0 importers after #12512)

dag/gunbc/defork_type_name_census.dag

@@ -111,6 +111,7 @@ type SharedTypeNameRow {
 type ForkResolution
   = ResolvedByRenamingV2 { renamed_to: String, citation: String }
   | ResolvedByDeletingV2 { reason: String }
+  | ResolvedByDeletingDag { reason: String }
   | ResolvedByRenamingDag { renamed_to: String, citation: String }
   | ResolvedByRehomingBothToExtdeps { authority: String, citation: String }
 
@@ -190,15 +191,6 @@ data defork_census_rows: List<SharedTypeNameRow> = [
     },
     disposition: ForkOpen { reason: "next PR of the de-fork wave (the v2 side has ~40 consumer sites across `v2.extdeps.formatters.*`)" }
   },
-  SharedTypeNameRow {
-    names: ["String"],
-    reading: AuthoredResolutionReading {
-      dag_side: "`= FreeMonoid<Char>` → `std.algebra` `FreeMonoid`, `std.types` `Char`",
-      v2_side: "`v2.std.text` `String`: same referents; `v2.std.node` `String`: opaque kernel host text (gunbc#12760), a different type under the same name, bound only where no other String declaration is visible",
-      class: "the structural pair is one concept, two declarations (duplicate); the v2.std.node host-text String is a distinct concept, not a third copy (gunbc.recurring_failure_mode carrier_by_spelling)"
-    },
-    disposition: ForkAwaitingRuling { question: "seed kernel name — out of scope for the wave" }
-  },
   SharedTypeNameRow {
     names: ["List"],
     reading: AuthoredResolutionReading {
@@ -274,6 +266,11 @@ data defork_census_rows: List<SharedTypeNameRow> = [
 ]
 
 data defork_census_resolved: List<ResolvedSharedTypeName> = [
+  ResolvedSharedTypeName {
+    names: ["String"],
+    resolution: ResolvedByDeletingDag { reason: "operator-ruled retirement of `std.string_type` `String` (`= FreeMonoid<Char>`), the duplicate of `v2.std.text` `String`. It had zero importers after gunbc#12512 deleted the 81 that used it as host text (XL-0T ruling B), verified by the #12760 literal-site census. `v2.std.text` `String` stays the one structural declaration, and `v2.std.node` `String` is the distinct host-text concept (gunbc.recurring_failure_mode carrier_by_spelling)" },
+    change: 13089
+  },
   ResolvedSharedTypeName {
     names: ["Nat"],
     resolution: ResolvedByDeletingV2 { reason: "operator ruling A (2026-09-30): the carrier is Peano, declared once in `std.nat` and realized as the kernel integer (`gunbc.structural_realization_bindings` `kernel_grounding_rows`); the `v2.std.nat` declaration is deleted, `std.magnitude` retired, and the semiring moved to inhabitance" },
@@ -340,6 +337,7 @@ fn census_resolution_text(r: ForkResolution) -> String {
   match r {
     ResolvedByRenamingV2 { renamed_to, citation } => concat(concat(concat("v2 side renamed `", renamed_to), "` — "), citation)
     ResolvedByDeletingV2 { reason } => concat("v2 side deleted — ", reason)
+    ResolvedByDeletingDag { reason } => concat("dag side deleted — ", reason)
     ResolvedByRenamingDag { renamed_to, citation } => concat(concat(concat("dag side renamed `", renamed_to), "` — "), citation)
     ResolvedByRehomingBothToExtdeps { authority, citation } => concat(concat(concat("both sides deleted; the concept is homed at `", authority), "` — "), citation)
   }

dag/test/claim/self_host_symbol_identity_binding_witness_test.dag

@@ -62,14 +62,13 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly
 
 // THE SAME-SPELLING SIBLINGS, all REAL declarations (the cited-declaration gate refuses a citation
 // of a declaration that does not exist, so the "another module declaring Symbol" falsifier is
-// asked of the declarations the corpus actually has two of): v2.std.text String and std.string_type
-// String beside the kernel String row, v2.std.logic Bool beside std.types Bool (which HAS an exact
+// asked of the declarations the corpus actually has two of): v2.std.text String beside the kernel
+// String row, v2.std.logic Bool beside std.types Bool (which HAS an exact
 // row), and v2.std.node Hash, declared in Symbol's own module one line below it. None may receive a
 // binding authored for a different declaration -- module-path and decl-name discrimination both.
 fn sibling_declarations_without_bindings() -> List<DeclarationRef> {
   [
     decl_ref(module_path: "v2.std.text", decl_name: "String"),
-    decl_ref(module_path: "std.string_type", decl_name: "String"),
     decl_ref(module_path: "v2.std.logic", decl_name: "Bool"),
     decl_ref(module_path: "v2.std.node", decl_name: "Hash")
   ]

docs/plans/dag-v2-defork-audit.md

@@ -192,12 +192,11 @@ Definition-unification (§3b.2: delete the dag record-of-methods *definition*) a
 
 ## 2D. The shared type-name census (the one list): the population is derived, the dispositions are authored
 
-**Derived:** every name declared as a `type` (record, coproduct or alias) under both `dag/std` and `src/v2/std`, read from the namespace by `gunbc.defork_type_name_census` `shared_type_names` at generation — **23 names** in this projection. **Authored:** each row's disposition, and — until the frontier below lands — the reading of what each side's body RESOLVES to. The two meet in an identity join by name, refused in both directions (a derived name no row disposes of; a row naming a pair that no longer exists), so this section cannot be generated from a stale disposition. Resolution, not body text, is what separates the classes: `Float = Float64` was byte-identical on both sides and bound two different `Float64`s. A **meaning fork** is one name for materially different concepts (DESIGN §3), resolved by renaming or deleting one side at its declaration, delete-first with no alias, the new name taken from the cited framework. **Frontier:** module-scoped type-reference resolution over the live pool, consumable from .dag: for a type declaration, each name its body references resolved to the declaration it binds in that module's scope (its own declarations, else its imports). When it lands, the three reading columns of every row here are derived from it and the authored readings are deleted; nothing else retires this frontier. Candidate home: `v2.compiler.name_resolve::resolve_with_admission`.
+**Derived:** every name declared as a `type` (record, coproduct or alias) under both `dag/std` and `src/v2/std`, read from the namespace by `gunbc.defork_type_name_census` `shared_type_names` at generation — **22 names** in this projection. **Authored:** each row's disposition, and — until the frontier below lands — the reading of what each side's body RESOLVES to. The two meet in an identity join by name, refused in both directions (a derived name no row disposes of; a row naming a pair that no longer exists), so this section cannot be generated from a stale disposition. Resolution, not body text, is what separates the classes: `Float = Float64` was byte-identical on both sides and bound two different `Float64`s. A **meaning fork** is one name for materially different concepts (DESIGN §3), resolved by renaming or deleting one side at its declaration, delete-first with no alias, the new name taken from the cited framework. **Frontier:** module-scoped type-reference resolution over the live pool, consumable from .dag: for a type declaration, each name its body references resolved to the declaration it binds in that module's scope (its own declarations, else its imports). When it lands, the three reading columns of every row here are derived from it and the authored readings are deleted; nothing else retires this frontier. Candidate home: `v2.compiler.name_resolve::resolve_with_admission`.
 
 | name(s) | declared in (derived) | dag/std side (authored reading) | src/v2/std side (authored reading) | class (authored) | disposition |
 | --- | --- | --- | --- | --- | --- |
 | `NonNegativeInt`, `PositiveInt` | `dag/std/integer.dag`, `src/v2/std/refinement.dag` | `std.integer` — `= Nat` / `= Nat where gt_zero` (refinement of `std.nat` `Nat`) | `v2.std.refinement` — record `refined: Refined<Int>` (smart-constructor over `v2.std.integer` `Int`), consumed by the formatter extdeps | MEANING FORK | OPEN — next PR of the de-fork wave (the v2 side has ~40 consumer sites across `v2.extdeps.formatters.*`) |
-| `String` | `dag/std/string_type.dag`, `src/v2/std/node.dag`, `src/v2/std/text.dag` | `= FreeMonoid<Char>` → `std.algebra` `FreeMonoid`, `std.types` `Char` | `v2.std.text` `String`: same referents; `v2.std.node` `String`: opaque kernel host text (gunbc#12760), a different type under the same name, bound only where no other String declaration is visible | the structural pair is one concept, two declarations (duplicate); the v2.std.node host-text String is a distinct concept, not a third copy (gunbc.recurring_failure_mode carrier_by_spelling) | AWAITING OPERATOR RULING — seed kernel name — out of scope for the wave |
 | `List` | `dag/std/types.dag`, `src/v2/std/collection.dag` | `= FreeMonoid<element>` → `std.algebra` `FreeMonoid` | `= std.algebra.FreeMonoid<T>` → same | one concept, two declarations (duplicate) | AWAITING OPERATOR RULING — seed kernel name — out of scope for the wave |
 | `Bool` | `dag/std/types.dag`, `src/v2/std/logic.dag` | `std.types` `= True \| False` | `v2.std.logic` `= True \| False` (arms are two more same-name declarations) | one concept, two declarations (duplicate) | AWAITING OPERATOR RULING — seed kernel name — out of scope for the wave |
 | `Int`, `UInt` | `dag/std/integer.dag`, `src/v2/std/integer.dag` | → `std.nat` `Nat` (via `std.algebra` `GroupCompletion`) | → `v2.std.nat` `Nat` | same concept, divergent referent | NEEDS A DECISION RECORD (integer family) |
@@ -211,6 +210,7 @@ Definition-unification (§3b.2: delete the dag record-of-methods *definition*) a
 
 | name(s) | resolution | change |
 | --- | --- | --- |
+| `String` | dag side deleted — operator-ruled retirement of `std.string_type` `String` (`= FreeMonoid<Char>`), the duplicate of `v2.std.text` `String`. It had zero importers after gunbc#12512 deleted the 81 that used it as host text (XL-0T ruling B), verified by the #12760 literal-site census. `v2.std.text` `String` stays the one structural declaration, and `v2.std.node` `String` is the distinct host-text concept (gunbc.recurring_failure_mode carrier_by_spelling) | #13089 |
 | `Nat` | v2 side deleted — operator ruling A (2026-09-30): the carrier is Peano, declared once in `std.nat` and realized as the kernel integer (`gunbc.structural_realization_bindings` `kernel_grounding_rows`); the `v2.std.nat` declaration is deleted, `std.magnitude` retired, and the semiring moved to inhabitance | #12846 |
 | `Float` | both sides deleted; the concept is homed at `extdeps.standards.ieee_754_2019 binary64` — IEEE 754-2019 §3.6 (operator ruling relayed 2026-09-28): `std.float` (Float = Float64, uncited) and `v2.std.float` (Float = Binary64) both deleted; kernel Float's meaning is the `std.kernel_type_denotation` row, not a std alias | #12547 |
 | `ProjectionKind` | v2 side deleted — `v2.std.projection` (compiler lens kinds) had zero importers; `std.planar_projection` keeps the name for drawing views | #12252 |

src/v1/coercion.dag

@@ -136,7 +136,7 @@ data type_reference_identity_note: String = "A realization decision is made at R
 fn structural_declaration_modules_for(dag_name: String) -> List<String> {
   match dag_name {
     "Hash" => ["src/v2/std/node.dag"]
-    "String" => ["src/v2/std/text.dag", "dag/std/string_type.dag"]
+    "String" => ["src/v2/std/text.dag"]
     "Bool" => ["src/v2/std/logic.dag"]
     _ => []
   }

src/v1/stage0/src/v1_compiler_coercion.rs

@@ -168,10 +168,7 @@ pub fn type_reference_identity_note() -> String {
 pub fn structural_declaration_modules_for(dag_name: String) -> Rc<Vec<String>> {
     match dag_name.clone().as_str() {
         "Hash" => Rc::new(vec!["src/v2/std/node.dag".to_string()]),
-        "String" => Rc::new(vec![
-            "src/v2/std/text.dag".to_string(),
-            "dag/std/string_type.dag".to_string(),
-        ]),
+        "String" => Rc::new(vec!["src/v2/std/text.dag".to_string()]),
         "Bool" => Rc::new(vec!["src/v2/std/logic.dag".to_string()]),
         _ => Rc::new(vec![]),
     }

src/v1/stage0/src/v1_tests_claim_checkpoint_identity_keying_witness_test.rs

@@ -113,18 +113,6 @@ pub fn table_present_string_refuses_under_structural_declaration_text() -> bool
     ) == std::option::Option::None)
 }
 
-pub fn table_present_string_refuses_under_structural_declaration_string_type() -> bool {
-    (crate::v1_compiler_emit_rust::rust_scalar_checkpoint_reference_base(
-        crate::v1_compiler_coercion::type_realization_decision(
-            RenderTarget::Rust,
-            "String".to_string(),
-            Rc::new(TypeDeclarationProvenance::CorpusDeclared {
-                decl_file: "dag/std/string_type.dag".to_string(),
-            }),
-        ),
-    ) == std::option::Option::None)
-}
-
 pub fn table_present_bool_refuses_under_structural_declaration_logic() -> bool {
     (crate::v1_compiler_emit_rust::rust_scalar_checkpoint_reference_base(
         crate::v1_compiler_coercion::type_realization_decision(
@@ -175,18 +163,6 @@ pub fn literal_suffix_refuses_under_structural_declaration_text() -> bool {
     ) == std::option::Option::None)
 }
 
-pub fn literal_suffix_refuses_under_structural_declaration_string_type() -> bool {
-    (crate::v1_compiler_coercion::literal_suffix(
-        crate::v1_compiler_coercion::type_realization_decision(
-            RenderTarget::Rust,
-            "String".to_string(),
-            Rc::new(TypeDeclarationProvenance::CorpusDeclared {
-                decl_file: "dag/std/string_type.dag".to_string(),
-            }),
-        ),
-    ) == std::option::Option::None)
-}
-
 pub fn literal_suffix_production_call_site_never_threads_declaration_identity() -> bool {
     (crate::v1_compiler_coercion::literal_suffix(
         crate::v1_compiler_coercion::type_realization_decision(

src/v1/tests/claim/checkpoint_identity_keying_witness_test.dag

@@ -127,11 +127,6 @@ test fn table_present_string_refuses_under_structural_declaration_text() -> Bool
     == none
 }
 
-test fn table_present_string_refuses_under_structural_declaration_string_type() -> Bool {
-  rust_scalar_checkpoint_reference_base(decision: type_realization_decision(target: Rust, dag_name: "String", provenance: CorpusDeclared { decl_file: "dag/std/string_type.dag" }))
-    == none
-}
-
 test fn table_present_bool_refuses_under_structural_declaration_logic() -> Bool {
   rust_scalar_checkpoint_reference_base(decision: type_realization_decision(target: Rust, dag_name: "Bool", provenance: CorpusDeclared { decl_file: "src/v2/std/logic.dag" }))
     == none
@@ -174,11 +169,6 @@ test fn literal_suffix_refuses_under_structural_declaration_text() -> Bool {
     == none
 }
 
-test fn literal_suffix_refuses_under_structural_declaration_string_type() -> Bool {
-  literal_suffix(decision: type_realization_decision(target: Rust, dag_name: "String", provenance: CorpusDeclared { decl_file: "dag/std/string_type.dag" }))
-    == none
-}
-
 // THE DISCLOSED GAP, EXECUTED RATHER THAN ASSERTED IN PROSE: the real call
 // site in emit_literal passes decl_file: "" for every String literal, and an
 // empty decl_file can never satisfy decl_file_declares_structurally (it