diff --git a/src/v2/compiler/03_normalize.dag b/src/v2/compiler/03_normalize.dag
index d48e5f7ee3c..dbfa94cb347 100644
--- a/src/v2/compiler/03_normalize.dag
+++ b/src/v2/compiler/03_normalize.dag
@@ -50,7 +50,9 @@ import v2.compiler.body_lowering_fold {
   body_lower_fn_decl_to_census_arrow,
   body_lower_service_decl,
   body_lower_is_deferred_lower_at_normalize,
-  body_lower_type_decl_record_name_optional
+  DeclaredTypeKind,
+  body_lower_type_decl_declared_kind_optional,
+  declared_record_names
 }
 import v2.compiler.normalized_tree {
   CensusTree,
@@ -358,13 +360,12 @@ fn import_binding_capture(tree: ParseTree, nodes: List<Node>) -> Outcome<FreeMon
   )
 }
 
-// WHICH OF THIS MODULE'S TYPES ARE RECORDS, read from the parse tree for the reason
-// import_binding_capture reads imports there: after lowering, a record is a bare
-// `Conj { R: payload }` that no reader can tell from a where-alias or a module spine. The question is
-// answered by the rehome's own predicate (v2.compiler.body_lowering_fold
-// body_lower_type_decl_record_name_optional), so what is carried and what was rehomed are one
-// decision, not two.
-fn record_declaration_capture(nodes: List<Node>) -> FreeMonoid<Symbol> {
+// WHICH KIND EACH OF THIS MODULE'S PLAIN-CONJ TYPES IS, read from the parse tree for the reason
+// import_binding_capture reads imports there: after lowering, a record, a where-refinement and a
+// payload-bearing single variant are one `Conj { R: payload }` shape. The question is answered by the
+// lowering's own predicate (v2.compiler.body_lowering_fold body_lower_type_decl_declared_kind_optional),
+// so what is carried and what was lowered are one decision, not two.
+fn type_declaration_kind_capture(nodes: List<Node>) -> FreeMonoid<DeclaredTypeKind> {
   fold_list(
     xs: nodes,
     empty: Empty,
@@ -375,9 +376,9 @@ fn record_declaration_capture(nodes: List<Node>) -> FreeMonoid<Symbol> {
           if id != ^dag_surface_type_decl {
             acc
           } else {
-            match body_lower_type_decl_record_name_optional(shell: n) {
+            match body_lower_type_decl_declared_kind_optional(shell: n) {
               Absent => acc
-              Present { value: name } => list_snoc_item(xs: acc, item: name)
+              Present { value: kind } => list_snoc_item(xs: acc, item: kind)
             }
           }
       }
@@ -385,6 +386,12 @@ fn record_declaration_capture(nodes: List<Node>) -> FreeMonoid<Symbol> {
   )
 }
 
+// The record names alone, for the census and the fixtures that fill a symbol index: a projection of
+// the one capture above, never a second reading of the parse.
+fn record_declaration_capture(nodes: List<Node>) -> FreeMonoid<Symbol> {
+  declared_record_names(kinds: type_declaration_kind_capture(nodes: nodes))
+}
+
 fn bind_retention_free(o: Outcome<BodyLoweredTree>) -> Outcome<Node> {
   match o {
     Rejected { diagnostics: r } => Rejected { diagnostics: r }
@@ -417,7 +424,7 @@ fn normalize(parse_tree: ParseTree) -> Outcome<NormalizedTree> {
                       root: grafted,
                       test_markers: markers,
                       import_bindings: bindings,
-                      record_declarations: record_declaration_capture(nodes: parse_nodes),
+                      type_declaration_kinds: type_declaration_kind_capture(nodes: parse_nodes),
                       diagnostics: d1
                     )
                 }
diff --git a/src/v2/compiler/body_lowering_fold.dag b/src/v2/compiler/body_lowering_fold.dag
index b6c2733bde5..219bff1d875 100644
--- a/src/v2/compiler/body_lowering_fold.dag
+++ b/src/v2/compiler/body_lowering_fold.dag
@@ -8170,7 +8170,8 @@ fn body_lower_find_where_host_conj(root: Node) -> Optional<Node> {
 // SO IT IS CARRIED FROM HERE, not recovered downstream: body_lower_type_decl_record_name_optional
 // (below) is the one predicate that says which type_decl is a record; this dispatch and
 // v2.compiler.normalize record_declaration_capture both ask it, and the capture rides to the symbol
-// index on NormalizedTree record_declarations, where the pattern-binder classifier reads it (Pkg16).
+// index on NormalizedTree type_declaration_kinds (its record projection), where the pattern-binder
+// classifier reads it (Pkg16).
 // The record-versus-where-alias control is v2.test.claim.match_arm_binder_frame
 // mab_where_alias_is_not_a_record.
 fn body_lower_record_type_decl(shell: Node, type_name: Symbol, block_shell: Node, type_params: DeclTypeParams) -> Outcome<Node> {
@@ -8400,6 +8401,53 @@ fn body_lower_type_decl_record_name_optional(shell: Node) -> Optional<Symbol> {
   }
 }
 
+// WHICH KIND OF PLAIN-CONJ DECLARATION A type_decl IS, ASKED ONCE, BY THE ARMS body_lower_type_decl_by_body
+// TAKES. After lowering, a record, a where-refinement and a payload-bearing single variant share the
+// Conj { Name: payload } shape, so the kind is read HERE, on the parse, and carried on
+// v2.compiler.normalized_tree NormalizedTree type_declaration_kinds. One value per declaration: a record
+// and a refinement are authored alternatives, so the carrier has no state naming one declaration as
+// both. A record is what body_lower_type_decl_record_name_optional says; otherwise a where clause --
+// here still its dag_surface_where_refinement_clause production shell, the parse-level form of the arm
+// the by-body dispatch finds as a Named edge -- makes a refinement; anything else carries no kind, and
+// a plain Conj member without one is undecided downstream, never inferred.
+type DeclaredTypeKind
+  = DeclaredRecord { name: Symbol }
+  | DeclaredRefinement { name: Symbol }
+
+fn body_lower_type_decl_declared_kind_optional(shell: Node) -> Optional<DeclaredTypeKind> {
+  match body_lower_type_decl_record_name_optional(shell: shell) {
+    Present { value: name } => Present { value: DeclaredRecord { name: name } }
+    Absent =>
+      match parse_production_captured_child_optional(node: shell) {
+        Absent => Absent
+        Present { value: captured } =>
+          match body_lower_find_production_shell_optional(root: captured, emitted: ^dag_surface_where_refinement_clause) {
+            Absent => Absent
+            Present { value: _ } =>
+              match dag_surface_kw_then_ident_from_captured(captured: captured) {
+                Absent => Absent
+                Present { value: name } => Present { value: DeclaredRefinement { name: name } }
+              }
+          }
+      }
+  }
+}
+
+// The record names among a module's declaration kinds: the projection every record-only consumer (the
+// symbol-index fill, the pattern-binder classifier, the census) reads, so records have one authority.
+fn declared_record_names(kinds: FreeMonoid<DeclaredTypeKind>) -> FreeMonoid<Symbol> {
+  fold_list(
+    xs: kinds,
+    empty: Empty,
+    cons: fn(acc, k) {
+      match k {
+        DeclaredRecord { name: n } => list_snoc_item(xs: acc, item: n)
+        DeclaredRefinement { name: _ } => acc
+      }
+    }
+  )
+}
+
 fn body_lower_type_decl(shell: Node) -> Outcome<Node> {
   match parse_production_captured_child_optional(node: shell) {
     Absent => body_lower_type_decl_unreadable(shell: shell)
diff --git a/src/v2/compiler/emit_produced.dag b/src/v2/compiler/emit_produced.dag
index 060acf01e3d..4d70f03679e 100644
--- a/src/v2/compiler/emit_produced.dag
+++ b/src/v2/compiler/emit_produced.dag
@@ -1,6 +1,6 @@
 module v2.compiler.emit_produced
 
-import v2.compiler.target_serialize { target_serialize_bodied_arrow_from_model }
+import v2.compiler.target_serialize { target_bundle_optional_child, target_serialize_bodied_arrow_from_model }
 import v2.compiler.target_carriers { emit_module_decl_separator, target_source_medium }
 import v2.std.compilers.target_model {
   ProducedDeclUnwired,
@@ -8,11 +8,19 @@ import v2.std.compilers.target_model {
   TargetModel,
   produced_decl_render_from_rows,
   render_target_text,
-  target_model_with_produced_scaffold
+  target_atom_type_spelling,
+  target_model_with_produced_scaffold,
+  TargetTypeExprAtom,
+  TargetTypeExpression,
+  target_type_expr_declaration_reference_emitted,
+  target_type_expression_spelling,
+  type_expression_projection_from_target,
+  BoundToken,
+  FixedToken
 }
 import extdeps.communication.medium { Medium }
-import v2.std.collection { Absent, List, Present, list_at_optional }
-import v2.std.algebra { fold_list, FreeMonoid }
+import v2.std.collection { Absent, List, Present, list_at_optional, map_get }
+import v2.std.algebra { contains, fold_list, FreeMonoid }
 import std.algebra { Cons, Empty, list_append, list_snoc_item }
 import v2.std.diagnostic {
   Accepted,
@@ -27,12 +35,15 @@ import v2.std.diagnostic {
   node_locus,
   outcome_rejected
 }
-import v2.std.node { Arrow, Conj, Disj, Edge, Named, Node, node_synthetic, Positional, Symbol, TypeNode }
+import v2.std.node { Arrow, Atom, Conj, Disj, Edge, Named, Node, node_synthetic, Positional, Symbol, TypeNode }
+import v2.std.qualified_name { declaration_reference_path_optional }
 import v2.std.type_binder { GenericTypeDecl, OpaqueTypeDecl, PlainTypeDecl, TypeAlias, type_decl_view }
-import v2.compiler.emit_semantic_decl { emit_semantic_type_decl }
+import v2.compiler.emit_semantic_decl { emit_semantic_type_decl, produced_type_binding }
+import v2.compiler.translate { serialize_concrete_syntax_tokens_to_source, translate_target_atom_realization_for_carrier }
 import v2.std.logic { Bool }
-import v2.std.node_query { find_arrow_body_child }
-import v2.extdeps.languages.dag { namespace_graft_node_is_module_body }
+import v2.compiler.body_lowering_fold { DeclaredRecord, DeclaredRefinement, DeclaredTypeKind }
+import v2.std.node_query { NamedChildAmbiguous, NamedChildFound, NamedChildMissing, find_arrow_body_child, named_child_lookup }
+import v2.extdeps.languages.dag { namespace_graft_node_is_module_body, parse_production_emitted_identity_optional }
 import v2.std.integer { Int }
 import v2.std.text { String }
 
@@ -143,29 +154,31 @@ fn produced_decl_conjs_in_tree(root: Node) -> FreeMonoid<Node> {
 
 
 // EVERY DIRECT MEMBER OF A MODULE BODY HAS EXACTLY ONE TARGET REALIZATION OR ONE TYPED REFUSAL.
-// The class is decided once, here, from the member's own declaration edge -- never from target
-// syntax, and never by filtering: a member no class renders refuses the whole module, located at that
-// member, so `fn add` beside an unrenderable declaration is never published alone. A bodied Arrow
-// renders through the target's produced-declaration rows (emit_produced_decl); a coproduct -- a plain
-// Disj, which only a coproduct lowers to -- renders through the existing semantic-declaration emitter
-// (v2.compiler.emit_semantic_decl emit_semantic_type_decl). A plain Conj member is NOT classified: after
-// lowering a record and a where-refinement share that shape (v2.compiler.body_lowering_fold
-// body_lower_record_type_decl), and the record/refinement fact rides on NormalizedTree
-// record_declarations, which does not reach this stage; reading it back from shape would be the
-// heuristic that note forbids, so both refuse until that fact is carried here. An alias, a bodyless
-// declaration and a generic declaration refuse under their own reasons: no target realization exists
-// for them yet, and each refusal names that capability rather than a whole-module failure.
+// The class is decided once, here, from the member's own declaration edge and its module's declaration
+// facts -- never from target syntax and never by filtering: a member no class renders refuses the whole
+// module, located at that member, so `fn add` beside an unrenderable declaration is never published
+// alone. A bodied Arrow renders through the target's produced-declaration rows (emit_produced_decl); a
+// coproduct (a plain Disj, which only a coproduct lowers to) and a record (a plain Conj its module's
+// declaration kinds call DeclaredRecord) render through v2.compiler.emit_semantic_decl
+// emit_semantic_type_decl; a where-refinement (DeclaredRefinement) takes its own class. The kinds are
+// v2.compiler.normalized_tree NormalizedTree type_declaration_kinds, one coproduct value per declaration,
+// so a member has one kind or none. A plain Conj with none -- a payload-bearing single variant shares
+// that shape after lowering -- is UNDECIDED and refuses; reading the kind back from the lowered shape or
+// its labels would be the heuristic the captured kind exists to replace. An alias, a bodyless declaration and a generic declaration
+// refuse under their own reasons: no target realization exists for them yet.
 type ModuleMemberClass
   = ModuleMemberBodiedArrow
   | ModuleMemberBodylessArrow
   | ModuleMemberCoproduct { name: Symbol, coproduct: Node }
+  | ModuleMemberRecord { name: Symbol, record: Node }
+  | ModuleMemberRefinement { name: Symbol, refinement: Node }
   | ModuleMemberRecordOrRefinement
   | ModuleMemberAlias
   | ModuleMemberOpaque
   | ModuleMemberGeneric
   | ModuleMemberUnsupported
 
-fn module_member_class(edge: Edge) -> ModuleMemberClass {
+fn module_member_class(edge: Edge, kinds: FreeMonoid<DeclaredTypeKind>) -> ModuleMemberClass {
   match edge.label {
     Positional => ModuleMemberUnsupported
     Named { name: n } =>
@@ -183,7 +196,8 @@ fn module_member_class(edge: Edge) -> ModuleMemberClass {
             PlainTypeDecl { member: m } =>
               match m.kind {
                 TypeNode { connective: Disj } => ModuleMemberCoproduct { name: n, coproduct: m }
-                TypeNode { connective: Conj } => ModuleMemberRecordOrRefinement
+                TypeNode { connective: Conj } =>
+                  module_member_conj_class(name: n, member: m, kinds: kinds)
                 _ => ModuleMemberUnsupported
               }
           }
@@ -191,14 +205,157 @@ fn module_member_class(edge: Edge) -> ModuleMemberClass {
   }
 }
 
+// A plain Conj member is a record or a refinement only when its module's captured kind SAYS so.
+fn module_member_conj_class(name: Symbol, member: Node, kinds: FreeMonoid<DeclaredTypeKind>) -> ModuleMemberClass {
+  fold_list(
+    xs: kinds,
+    empty: ModuleMemberRecordOrRefinement,
+    cons: fn(acc, k) {
+      match acc {
+        ModuleMemberRecordOrRefinement =>
+          match k {
+            DeclaredRecord { name: r } =>
+              if r == name { ModuleMemberRecord { name: name, record: member } } else { acc }
+            DeclaredRefinement { name: r } =>
+              if r == name { ModuleMemberRefinement { name: name, refinement: member } } else { acc }
+          }
+        _ => acc
+      }
+    }
+  )
+}
+
+// A WHERE-REFINEMENT DECLARATION THROUGH THE TARGET'S OWN REALIZATION ROW (target_model_edge_
+// refinement_declaration; Rust's is a transparent alias, v2.extdeps.languages.rust
+// rust_refinement_declaration_realization_node). The fold supplies only what the declaration states --
+// its name and its carrier -- and the row supplies every token class; the carrier is spelled by the one
+// type resolver (produced_type_binding), so no target spelling is written here. A target declaring no
+// row refuses emit_module_member_refinement_not_realized at the member; so does a refinement whose
+// carrier edge is missing or whose carrier the target cannot spell. Rows are read from the base target,
+// as the atom realizations are (the partition's augmented bundle is not their host).
+fn emit_refinement_declaration(
+  name: Symbol,
+  refinement: Node,
+  target: TargetModel,
+  realization_host: TargetModel
+) -> Outcome<Medium<String>> {
+  bind_outcome(
+    o: target_bundle_optional_child(target: realization_host, edge_name: ^target_model_edge_refinement_declaration),
+    f: fn(row_optional) {
+      match row_optional {
+        Absent => emit_module_member_refused(reason: ^emit_module_member_refinement_not_realized, at: refinement)
+        Present { value: row } =>
+          bind_outcome(
+            o: refinement_declaration_row_classes(row: row),
+            f: fn(classes) {
+              bind_outcome(
+                o: named_child_outcome(node: refinement, name: ^dag_surface_type_expr, missing: ^emit_module_member_refinement_carrier_absent),
+                f: fn(carrier) {
+                  if refinement_carrier_is_unlowered(carrier: carrier) {
+                    emit_module_member_refused(reason: ^emit_module_member_refinement_carrier_unlowered, at: carrier)
+                  } else {
+                  let resolve_type = produced_type_binding(target: realization_host)
+                  bind_outcome(
+                    o: resolve_type(carrier),
+                    f: fn(carrier_binding) {
+                      serialize_concrete_syntax_tokens_to_source(
+                        target: target,
+                        tokens: [
+                          FixedToken { token_class: classes.keyword },
+                          BoundToken { token_class: classes.name, binding: name },
+                          FixedToken { token_class: classes.assign },
+                          BoundToken { token_class: classes.name, binding: carrier_binding },
+                          FixedToken { token_class: classes.terminator }
+                        ]
+                      )
+                    }
+                  )
+                  }
+                }
+              )
+            }
+          )
+      }
+    }
+  )
+}
+
+// A REFINEMENT'S CARRIER MUST BE A LOWERED TYPE. The production route lowers it (a module member's
+// where-refinement emits `type Pos = i32;` in v2.test.claim.emit.module_member_emission); a carrier that
+// is still a parse-production shell refuses under its own reason rather than as an unrealized type, so the
+// refusal says what is missing.
+fn refinement_carrier_is_unlowered(carrier: Node) -> Bool {
+  match parse_production_emitted_identity_optional(node: carrier) {
+    Present { value: _ } => true
+    Absent => false
+  }
+}
+
+type RefinementDeclarationClasses {
+  keyword: Symbol
+  name: Symbol
+  assign: Symbol
+  terminator: Symbol
+}
+
+// Each field the row must name, read as one token-class atom; a missing, duplicated or non-atom field
+// refuses emit_module_member_refinement_realization_malformed, located at the row.
+fn refinement_declaration_row_classes(row: Node) -> Outcome<RefinementDeclarationClasses> {
+  bind_outcome(
+    o: refinement_row_class(row: row, field: ^refinement_declaration_field_keyword),
+    f: fn(keyword) {
+      bind_outcome(
+        o: refinement_row_class(row: row, field: ^refinement_declaration_field_name),
+        f: fn(name_class) {
+          bind_outcome(
+            o: refinement_row_class(row: row, field: ^refinement_declaration_field_assign),
+            f: fn(assign) {
+              bind_outcome(
+                o: refinement_row_class(row: row, field: ^refinement_declaration_field_terminator),
+                f: fn(terminator) {
+                  outcome_accepted(value: RefinementDeclarationClasses { keyword: keyword, name: name_class, assign: assign, terminator: terminator })
+                }
+              )
+            }
+          )
+        }
+      )
+    }
+  )
+}
+
+fn refinement_row_class(row: Node, field: Symbol) -> Outcome<Symbol> {
+  bind_outcome(
+    o: named_child_outcome(node: row, name: field, missing: ^emit_module_member_refinement_realization_malformed),
+    f: fn(t) {
+      match t.kind {
+        TypeNode { connective: Atom { identity: id } } => outcome_accepted(value: id)
+        _ => outcome_rejected(d: emit_produced_decl_diagnostic(reason: ^emit_module_member_refinement_realization_malformed, node: row))
+      }
+    }
+  )
+}
+
+// The one child a row or member names (v2.std.node_query named_child_lookup); missing or duplicated
+// refuses with the caller's reason, located at the node.
+fn named_child_outcome(node: Node, name: Symbol, missing: Symbol) -> Outcome<Node> {
+  match named_child_lookup(root: node, name: name) {
+    NamedChildFound { target: t } => outcome_accepted(value: t)
+    NamedChildMissing => outcome_rejected(d: emit_produced_decl_diagnostic(reason: missing, node: node))
+    NamedChildAmbiguous => outcome_rejected(d: emit_produced_decl_diagnostic(reason: missing, node: node))
+  }
+}
+
 fn emit_module_member_refused(reason: Symbol, at: Node) -> Outcome<Medium<String>> {
   outcome_rejected(d: emit_produced_decl_diagnostic(reason: reason, node: at))
 }
 
-fn emit_module_member(edge: Edge, target: TargetModel) -> Outcome<Medium<String>> {
-  match module_member_class(edge: edge) {
-    ModuleMemberBodiedArrow => emit_produced_decl(decl: produced_decl_node_for_edge(edge: edge), target: target)
-    ModuleMemberCoproduct { name: n, coproduct: c } => emit_semantic_type_decl(name: n, params: [], node: c, target: target)
+fn emit_module_member(edge: Edge, target: TargetModel, realization_host: TargetModel, kinds: FreeMonoid<DeclaredTypeKind>) -> Outcome<Medium<String>> {
+  match module_member_class(edge: edge, kinds: kinds) {
+    ModuleMemberBodiedArrow => emit_produced_decl_declaring(decl: produced_decl_node_for_edge(edge: edge), target: target, realization_host: realization_host)
+    ModuleMemberCoproduct { name: n, coproduct: c } => emit_semantic_type_decl(name: n, params: [], node: c, target: target, realization_host: realization_host)
+    ModuleMemberRecord { name: n, record: r } => emit_semantic_type_decl(name: n, params: [], node: r, target: target, realization_host: realization_host)
+    ModuleMemberRefinement { name: n, refinement: m } => emit_refinement_declaration(name: n, refinement: m, target: target, realization_host: realization_host)
     ModuleMemberBodylessArrow => emit_module_member_refused(reason: ^emit_module_member_arrow_has_no_body, at: edge.target)
     ModuleMemberRecordOrRefinement => emit_module_member_refused(reason: ^emit_module_member_record_or_refinement_undecided, at: edge.target)
     ModuleMemberAlias => emit_module_member_refused(reason: ^emit_module_member_alias_not_realized, at: edge.target)
@@ -247,7 +404,7 @@ fn produced_module_bodies_declare_members(root: Node) -> Bool {
 
 // Every module body's members, in order, each through its one realization; the first refusal refuses
 // the module with nothing partial published.
-fn emit_module_body_members(root: Node, target: TargetModel) -> Outcome<Medium<String>> {
+fn emit_module_body_members(root: Node, target: TargetModel, realization_host: TargetModel, kinds: FreeMonoid<DeclaredTypeKind>) -> Outcome<Medium<String>> {
   let members = fold(module_bodies_in_tree(node: root, acc: []), init: [], f: fn(acc, b) {
     concat(acc, module_body_member_edges(body: b))
   })
@@ -260,7 +417,7 @@ fn emit_module_body_members(root: Node, target: TargetModel) -> Outcome<Medium<S
           o: acc,
           f: fn(partial) {
             bind_outcome(
-              o: emit_module_member(edge: edge, target: target),
+              o: emit_module_member(edge: edge, target: target, realization_host: realization_host, kinds: kinds),
               f: fn(medium) {
                 Accepted { value: concat(partial, medium.carried, emit_module_decl_separator), diagnostics: None }
               }
@@ -298,6 +455,10 @@ fn emit_produced_decl_with_target(
 // produced_decl_target_unwired:
 // never a widen, never a fabricated default (DESIGN section 5).
 fn emit_produced_decl(decl: Node, target: TargetModel) -> Outcome<Medium<String>> {
+  emit_produced_decl_declaring(decl: decl, target: target, realization_host: target)
+}
+
+fn emit_produced_decl_declaring(decl: Node, target: TargetModel, realization_host: TargetModel) -> Outcome<Medium<String>> {
   match target.produced_decl_support {
     ProducedDeclUnwired =>
       outcome_rejected(
@@ -309,7 +470,7 @@ fn emit_produced_decl(decl: Node, target: TargetModel) -> Outcome<Medium<String>
       scaffold_base_row: base_row
     } =>
       bind_outcome(
-        o: produced_decl_render_from_rows(rows: rows, decl: decl),
+        o: produced_decl_render_from_rows(rows: rows, decl: decl, type_binding: produced_type_binding(target: realization_host)),
         f: fn(scaffold) {
           emit_produced_decl_with_target(
             decl: decl,
diff --git a/src/v2/compiler/emit_semantic_decl.dag b/src/v2/compiler/emit_semantic_decl.dag
index b0fd0a9f51d..82cfee1f689 100644
--- a/src/v2/compiler/emit_semantic_decl.dag
+++ b/src/v2/compiler/emit_semantic_decl.dag
@@ -1,29 +1,44 @@
 module v2.compiler.emit_semantic_decl
 
-import v2.compiler.translate { serialize_concrete_syntax_tokens_to_source }
+import v2.compiler.translate { serialize_concrete_syntax_tokens_to_source, translate_target_atom_realization_for_carrier }
 import v2.compiler.target_serialize { grammar_relation_row_for_emitted, grammar_relation_row_tokens_root }
 import v2.std.compilers.semantic_decl_emission {
   TargetSemanticDeclSerializeProfile,
   semantic_decl_emission_from_target,
+  semantic_decl_profile_binding_spellings_over,
   semantic_decl_serialize_target,
   target_semantic_enum_surface_from_coproduct,
   target_semantic_struct_surface_from_record
 }
-import v2.std.collection { List }
-import v2.std.compilers.target_model { TargetModel, concrete_syntax_token_list_from_node }
+import v2.std.collection { Absent, List, Map, Present, empty_map, map_get }
+import v2.std.qualified_name { declaration_reference_path_optional }
+import v2.std.compilers.target_model {
+  TargetModel,
+  TargetTypeExprAtom,
+  TargetTypeExpression,
+  concrete_syntax_token_list_from_node,
+  target_atom_type_spelling,
+  target_type_expr_declaration_reference_emitted,
+  target_type_expression_spelling,
+  type_expression_projection_from_target
+}
 import v2.std.diagnostic {
+  Accepted,
+  Rejected,
   Diagnostic,
   ExternalContractUnknown,
   Outcome,
   Unavailable,
   bind_outcome,
   node_locus,
+  outcome_accepted,
   outcome_rejected
 }
-import v2.std.node { Disj, Conj, Node, Symbol, TypeNode }
+import v2.std.node { Atom, Disj, Conj, Node, Symbol, TypeNode }
 import extdeps.communication.medium { Medium }
 import v2.std.text { String }
 import std.algebra { Empty }
+import v2.std.algebra { contains }
 
 fn emit_semantic_decl_unsupported_diagnostic(node: Node) -> Diagnostic {
   Diagnostic {
@@ -36,7 +51,8 @@ fn emit_semantic_decl_unsupported_diagnostic(node: Node) -> Diagnostic {
 fn emit_decl_surface(
   surface: Node,
   rules: Node,
-  profile: TargetSemanticDeclSerializeProfile
+  profile: TargetSemanticDeclSerializeProfile,
+  host_binding_spellings: Map<Symbol, String>
 ) -> Outcome<Medium<String>> {
   bind_outcome(
     o: grammar_relation_row_for_emitted(rules: rules, emitted: surface),
@@ -48,7 +64,7 @@ fn emit_decl_surface(
             o: concrete_syntax_token_list_from_node(list_node: tokens_root),
             f: fn(tokens) {
               bind_outcome(
-                o: semantic_decl_serialize_target(profile: profile, rules: rules),
+                o: semantic_decl_serialize_target(profile: profile, rules: rules, host_binding_spellings: host_binding_spellings),
                 f: fn(serialize_target) {
                   serialize_concrete_syntax_tokens_to_source(
                     target: serialize_target,
@@ -64,45 +80,67 @@ fn emit_decl_surface(
   )
 }
 
+// A TYPE DECLARATION THROUGH THE TARGET'S SEMANTIC ROWS, THE ONE ROUTE. Its field and variant types are
+// spelled by produced_type_binding_over the realization host (the base target whose atom realization
+// rows match) and the map each declaration is serialized with -- its profile's rows over the emitting
+// target's own binding_spellings. There is no route that
+// binds a type as itself: a type the target cannot spell refuses, located, rather than printing its
+// interned name.
 fn emit_semantic_type_decl(
   name: Symbol,
   params: List<Symbol>,
   node: Node,
-  target: TargetModel
+  target: TargetModel,
+  realization_host: TargetModel
 ) -> Outcome<Medium<String>> {
+  let host_binding_spellings = target.binding_spellings
   bind_outcome(
     o: semantic_decl_emission_from_target(target: target),
     f: fn(emission) {
       match node.kind {
         TypeNode { connective: Disj } =>
           bind_outcome(
-            o: target_semantic_enum_surface_from_coproduct(
-              projection: emission.surface,
-              name: name,
-              params: params,
-              coproduct: node
-            ),
-            f: fn(surface) {
-              emit_decl_surface(
-                surface: surface,
-                rules: emission.enum_translation_rules,
-                profile: emission.enum_serialize_profile
+            o: semantic_decl_profile_binding_spellings_over(profile: emission.enum_serialize_profile, base: host_binding_spellings),
+            f: fn(spellings) {
+              bind_outcome(
+                o: target_semantic_enum_surface_from_coproduct(
+                  projection: emission.surface,
+                  name: name,
+                  params: params,
+                  coproduct: node,
+                  type_binding: semantic_decl_type_binding(params: params, resolve: produced_type_binding_over(target: realization_host, spellings: spellings))
+                ),
+                f: fn(surface) {
+                  emit_decl_surface(
+                    surface: surface,
+                    rules: emission.enum_translation_rules,
+                    profile: emission.enum_serialize_profile,
+                    host_binding_spellings: host_binding_spellings
+                  )
+                }
               )
             }
           )
         TypeNode { connective: Conj } =>
           bind_outcome(
-            o: target_semantic_struct_surface_from_record(
-              projection: emission.surface,
-              name: name,
-              params: params,
-              record: node
-            ),
-            f: fn(surface) {
-              emit_decl_surface(
-                surface: surface,
-                rules: emission.struct_translation_rules,
-                profile: emission.struct_serialize_profile
+            o: semantic_decl_profile_binding_spellings_over(profile: emission.struct_serialize_profile, base: host_binding_spellings),
+            f: fn(spellings) {
+              bind_outcome(
+                o: target_semantic_struct_surface_from_record(
+                  projection: emission.surface,
+                  name: name,
+                  params: params,
+                  record: node,
+                  type_binding: semantic_decl_type_binding(params: params, resolve: produced_type_binding_over(target: realization_host, spellings: spellings))
+                ),
+                f: fn(surface) {
+                  emit_decl_surface(
+                    surface: surface,
+                    rules: emission.struct_translation_rules,
+                    profile: emission.struct_serialize_profile,
+                    host_binding_spellings: host_binding_spellings
+                  )
+                }
               )
             }
           )
@@ -111,3 +149,78 @@ fn emit_semantic_type_decl(
     }
   )
 }
+
+// A declaration's own type parameter is bound by the declaration itself (`Pair<K, V> { key: K }`), so it is
+// spelled by its own name; every other type goes through the resolver. A parameter is recognized by
+// identity against the declaration's binder list, never by the shape or case of its name.
+fn semantic_decl_type_binding(params: List<Symbol>, resolve: fn(Node) -> Outcome<Symbol>) -> fn(Node) -> Outcome<Symbol> {
+  fn(type_node) {
+    match type_node.kind {
+      TypeNode { connective: Atom { identity: id } } =>
+        if contains(xs: params, item: id, eq: fn(a, b) { a == b }) { outcome_accepted(value: id) } else { resolve(type_node) }
+      _ => resolve(type_node)
+    }
+  }
+}
+
+fn emit_type_reference_unrealized_diagnostic(node: Node) -> Diagnostic {
+  Diagnostic {
+    reason: ^produced_decl_type_ref_unrealized,
+    at: node_locus(node: node),
+    correction: Unavailable { reason: ExternalContractUnknown }
+  }
+}
+
+// HOW A SIGNATURE TYPE IS SPELLED, IN ONE ORDER, AND NEVER BY FABRICATION. A reference to a declared
+// type (the resolved declaration-reference node) is spelled by the target's own declaration-reference
+// form -- the rule the type-expression translate already applies (v2.std.compilers.target_model
+// target_type_expr_declaration_reference_emitted; Rust: `crate::<module>::<Name>`, the same for this
+// module's types and another's). A kernel carrier atom binds its atom realization row's surface symbol
+// (target_atom_type_spelling), which the target's binding_spellings spell. Failing both, an explicit
+// binding_spellings entry for the atom itself is used as written. Anything else refuses, located.
+// Before this, every type atom was bound as itself and an unmapped one printed its interned name
+// (`bool_node_symbol`), and a declared type's reference refused as an unsupported shape.
+// STANDING, STATED: Int still reaches `i32` through its explicit binding_spellings entry, not through a
+// realization row -- the target has no Int atom realization (there is no integer value-template kind to
+// give one), so that route is not yet unified with Bool's.
+fn produced_type_binding(target: TargetModel) -> fn(Node) -> Outcome<Symbol> {
+  produced_type_binding_over(target: target, spellings: target.binding_spellings)
+}
+
+// The same order, with the explicit-entry step read from the map the caller will SERIALIZE with -- for a
+// type declaration that is the serialize profile's rows over the target's own map
+// (v2.std.compilers.semantic_decl_emission semantic_decl_profile_binding_spellings_over), so an atom is
+// admitted exactly when the serialization that follows spells it, and never reaches the interned-name
+// spelling bound_spelling_from_map gives an unmapped identifier.
+fn produced_type_binding_over(target: TargetModel, spellings: Map<Symbol, String>) -> fn(Node) -> Outcome<Symbol> {
+  fn(type_node) {
+    match declaration_reference_path_optional(node: type_node) {
+      Present { value: path } =>
+        bind_outcome(
+          o: type_expression_projection_from_target(target: target),
+          f: fn(projection) {
+            bind_outcome(
+              o: target_type_expr_declaration_reference_emitted(projection: projection, path: path, reference: type_node),
+              f: fn(emitted) {
+                outcome_accepted(value: target_type_expression_spelling(form: TargetTypeExpression { kind: TargetTypeExprAtom, node: emitted }))
+              }
+            )
+          }
+        )
+      Absent =>
+        match type_node.kind {
+          TypeNode { connective: Atom { identity: id } } =>
+            match translate_target_atom_realization_for_carrier(target: target, source_carrier: type_node) {
+              Accepted { value: row, diagnostics: _ } => outcome_accepted(value: target_atom_type_spelling(row: row))
+              Rejected { diagnostics: _ } =>
+                match map_get(spellings, id) {
+                  Accepted { value: Present { value: _ }, diagnostics: _ } => outcome_accepted(value: id)
+                  _ => outcome_rejected(d: emit_type_reference_unrealized_diagnostic(node: type_node))
+                }
+            }
+          _ => outcome_rejected(d: emit_type_reference_unrealized_diagnostic(node: type_node))
+        }
+    }
+  }
+}
+
diff --git a/src/v2/compiler/normalized_tree.dag b/src/v2/compiler/normalized_tree.dag
index 9e8d0afcaee..63038c77db9 100644
--- a/src/v2/compiler/normalized_tree.dag
+++ b/src/v2/compiler/normalized_tree.dag
@@ -2,6 +2,8 @@ module v2.compiler.normalized_tree
 
 import v2.compiler.body_lowering_fold {
   BodyLoweredTree,
+  DeclaredTypeKind,
+  declared_record_names,
   wrapper_retention_diagnostic
 }
 import v2.std.diagnostic {
@@ -40,14 +42,14 @@ import v2.std.namespace_alias { AliasBindingRow, ModuleBindingSource }
 // shape a where-alias rehome writes and the shape the graft builds for a module spine, so after
 // normalize a record is indistinguishable from either -- and the pattern-binder classifier must
 // tell a record (a constructor) from a module (not one). The fact is read where it is still held,
-// by the same predicate the rehome uses, and carried here as the leaf names this module declares
-// as records; the symbol-index fill qualifies each by this module's own name, so the key the index
+// by the same predicate the rehome uses, and carried here as the kind of each such declaration
+// (records among them); the symbol-index fill qualifies each by this module's own name, so the key the index
 // holds is a declaring path, never a bare spelling.
 type NormalizedTree sole_constructor {
   root: Node,
   test_markers: TestMarkerChannel,
   import_bindings: FreeMonoid<AliasBindingRow>,
-  record_declarations: FreeMonoid<Symbol>,
+  type_declaration_kinds: FreeMonoid<DeclaredTypeKind>,
 }
 
 // THE RETENTION DOOR (MQ-4). A shell the body lowering could not lower is a typed variant of its result
@@ -102,11 +104,22 @@ fn no_record_declarations() -> FreeMonoid<Symbol> {
   Empty
 }
 
+// A hand-built root carries no declaration kinds, for the same reason it carries no record names.
+fn no_type_declaration_kinds() -> FreeMonoid<DeclaredTypeKind> {
+  Empty
+}
+
+// THE KIND OF EACH PLAIN-CONJ TYPE THIS MODULE DECLARES, read at normalize by
+// v2.compiler.body_lowering_fold body_lower_type_decl_declared_kind_optional: after lowering, a record,
+// a where-refinement and a payload-bearing single variant share one shape. One list of one coproduct,
+// so a declaration has one kind or none; the symbol-index fill reads its record projection
+// (normalized_tree_record_declarations) and emission reads the whole (v2.compiler.emit_produced
+// emit_module_member). A caller holding no parse passes no_type_declaration_kinds().
 fn admit_normalized_tree(
   root: Node,
   test_markers: TestMarkerChannel,
   import_bindings: FreeMonoid<AliasBindingRow>,
-  record_declarations: FreeMonoid<Symbol>,
+  type_declaration_kinds: FreeMonoid<DeclaredTypeKind>,
   diagnostics: Diagnostics
 ) -> Outcome<NormalizedTree> {
   Accepted {
@@ -114,12 +127,16 @@ fn admit_normalized_tree(
       root: root,
       test_markers: test_markers,
       import_bindings: import_bindings,
-      record_declarations: record_declarations
+      type_declaration_kinds: type_declaration_kinds
     },
     diagnostics: diagnostics
   }
 }
 
+fn normalized_tree_record_declarations(t: NormalizedTree) -> FreeMonoid<Symbol> {
+  declared_record_names(kinds: t.type_declaration_kinds)
+}
+
 // A MODULE OUTSIDE THE COMPILED CLOSURE, AT CENSUS GRADE (v2.compiler.normalize normalize_census):
 // every declaration, no fn body. It is a separate sealed carrier rather than a NormalizedTree with a
 // flag because what distinguishes it is what may consume it: resolution reads a non-member's
@@ -196,7 +213,7 @@ fn normalized_tree_roots_to_binding_sources(
         item: ModuleBindingSource {
           root: tree.root,
           import_bindings: tree.import_bindings,
-          record_declarations: tree.record_declarations
+          record_declarations: normalized_tree_record_declarations(t: tree)
         }
       )
     }
@@ -238,7 +255,7 @@ fn admit_unmarked_normalized_roots(
             root: root,
             test_markers: test_marker_channel_empty(),
             import_bindings: no_import_bindings(),
-            record_declarations: no_record_declarations()
+            type_declaration_kinds: no_type_declaration_kinds()
           }
         )
       }
diff --git a/src/v2/compiler/program_partition.dag b/src/v2/compiler/program_partition.dag
index 0d861776bd7..e42e9f971da 100644
--- a/src/v2/compiler/program_partition.dag
+++ b/src/v2/compiler/program_partition.dag
@@ -4,9 +4,11 @@ import std.dissolution { DissolutionCondition, dissolution_description, unbound_
 
 import v2.compiler.emit { emit }
 import v2.compiler.emit_produced {
-  produced_module_bodies_declare_members,
-  emit_module_body_members
+  emit_module_body_members,
+  produced_module_bodies_declare_members
 }
+import v2.compiler.body_lowering_fold { DeclaredTypeKind }
+import v2.compiler.normalized_tree { no_type_declaration_kinds }
 import v2.compiler.infer {
   InferredFacts,
   InferredFactsEntry,
@@ -21,7 +23,7 @@ import v2.compiler.target_serialize { translate_project_transform_in_arrow_scope
 import v2.extdeps.languages.dag { dag_value_expression_projection }
 import v2.lens.application { subterm_at }
 import std.algebra { Empty, list_append, list_snoc_item }
-import v2.std.algebra { any, fold_list }
+import v2.std.algebra { any, fold_list, FreeMonoid }
 import v2.std.collection {
   List,
   Map
@@ -607,7 +609,9 @@ fn emit_partition_arrow_body_behavior_source(
 
 fn emit_partition_with_target(
   partition: ProgramPartition,
-  target: TargetModel
+  target: TargetModel,
+  realization_host: TargetModel,
+  kinds: FreeMonoid<DeclaredTypeKind>
 ) -> Outcome<Medium<String>> {
   if partition_segment_is_ambient_arrow_body_behavior(partition: partition) {
     bind_outcome(
@@ -624,7 +628,7 @@ fn emit_partition_with_target(
       o: partition_inferred_tree(partition: partition),
       f: fn(tree) {
         if produced_module_bodies_declare_members(root: tree.root) {
-          emit_module_body_members(root: tree.root, target: target)
+          emit_module_body_members(root: tree.root, target: target, realization_host: realization_host, kinds: kinds)
         } else {
           emit(tree: tree, target: target)
         }
@@ -633,14 +637,21 @@ fn emit_partition_with_target(
   }
 }
 
+// THE AUGMENTED TARGET IS NOT THE ATOM REALIZATIONS' HOST. partition_derive_target_for_emit adds this
+// program's ownership rows and value-semantics carriers to the target's bundle, and every atom
+// realization row is bound to the base bundle it was authored against
+// (v2.std.compilers.target_model target_atom_realization_bundle_matches_host), so a realization looked up
+// against the augmented target matches no row. Emission runs against the augmented target; a signature
+// type's realization is resolved against the base one, passed through as realization_host.
 fn emit_partition(
   partition: ProgramPartition,
-  target: TargetModel
+  target: TargetModel,
+  kinds: FreeMonoid<DeclaredTypeKind>
 ) -> Outcome<Medium<String>> {
   bind_outcome(
     o: partition_derive_target_for_emit(partition: partition, target: target),
     f: fn(derived_target) {
-      emit_partition_with_target(partition: partition, target: derived_target)
+      emit_partition_with_target(partition: partition, target: derived_target, realization_host: target, kinds: kinds)
     }
   )
 }
@@ -650,6 +661,27 @@ fn emit_for_target(
   segment: ProgramSegment,
   target: TargetModel,
   boundary: PartitionBoundaryPolicy
+) -> Outcome<Medium<String>> {
+  emit_for_target_with_declarations(
+    program: program,
+    segment: segment,
+    target: target,
+    boundary: boundary,
+    kinds: no_type_declaration_kinds()
+  )
+}
+
+// THE DECLARATION FACTS A MODULE'S EMISSION NEEDS AND ITS INFERRED TREE DOES NOT CARRY. Which members are
+// records is declaration provenance, not inferred type evidence, so it rides beside the tree rather than
+// in it: the caller that still holds the module's NormalizedTree passes its type_declaration_kinds (the
+// closure door does), and emit_for_target, whose callers hold only the inferred tree, passes none -- so a
+// plain Conj member there refuses as undecided rather than being guessed a record.
+fn emit_for_target_with_declarations(
+  program: InferredTree,
+  segment: ProgramSegment,
+  target: TargetModel,
+  boundary: PartitionBoundaryPolicy,
+  kinds: FreeMonoid<DeclaredTypeKind>
 ) -> Outcome<Medium<String>> {
   bind_outcome(
     o: resolve_program_partition(
@@ -658,7 +690,7 @@ fn emit_for_target(
       boundary: boundary
     ),
     f: fn(partition) {
-      emit_partition(partition: partition, target: target)
+      emit_partition(partition: partition, target: target, kinds: kinds)
     }
   )
 }
diff --git a/src/v2/compiler/self_host/candidate_generation.dag b/src/v2/compiler/self_host/candidate_generation.dag
index a373db81308..7e8de4d6ffa 100644
--- a/src/v2/compiler/self_host/candidate_generation.dag
+++ b/src/v2/compiler/self_host/candidate_generation.dag
@@ -5,6 +5,7 @@ import extdeps.communication.medium { Medium }
 import extdeps.filesystem.filesystem_io { Filesystem }
 import v2.compiler.emit { emit }
 import v2.compiler.emit_produced { emit_module_body_members, produced_module_bodies_declare_members }
+import v2.compiler.normalized_tree { no_type_declaration_kinds }
 import v2.compiler.infer { InferredTree }
 import v2.compiler.name_resolve { Admission }
 import v2.compiler.program_assembly { assemble_program_from_ingest }
@@ -192,7 +193,7 @@ fn generate_rust_module_emission_candidate(
 ) -> Outcome<RustEmissionCandidate> {
   if produced_module_bodies_declare_members(root: inferred.root) {
     bind_outcome(
-      o: emit_module_body_members(root: inferred.root, target: target),
+      o: emit_module_body_members(root: inferred.root, target: target, realization_host: target, kinds: no_type_declaration_kinds()),
       f: fn(source) {
         outcome_accepted(
           value: RustEmissionCandidate {
diff --git a/src/v2/compiler/self_host/closure_emission.dag b/src/v2/compiler/self_host/closure_emission.dag
index 0045f5eb8d2..e3264656019 100644
--- a/src/v2/compiler/self_host/closure_emission.dag
+++ b/src/v2/compiler/self_host/closure_emission.dag
@@ -27,7 +27,7 @@ import v2.compiler.normalized_tree {
 }
 import v2.compiler.parse { PreparedGrammar, parse_module_prepared_seeded, prepare_grammar }
 import v2.compiler.program_assembly { program_assembly_phase_tokenize }
-import v2.compiler.program_partition { emit_for_target }
+import v2.compiler.program_partition { emit_for_target_with_declarations }
 import v2.compiler.reference_closure {
   ReferenceClosureMember,
   ReferenceClosureNeighboursRead,
@@ -437,11 +437,12 @@ fn closure_member_emission(
             bind_outcome(
               o: infer_and_discharge(tree: resolved),
               f: fn(inferred) {
-                emit_for_target(
+                emit_for_target_with_declarations(
                   program: inferred,
                   segment: program_segment_whole_program(),
                   target: target,
-                  boundary: partition_boundary_fail_closed()
+                  boundary: partition_boundary_fail_closed(),
+                  kinds: visit.member.payload.type_declaration_kinds
                 )
               }
             )
diff --git a/src/v2/extdeps/languages/rust.dag b/src/v2/extdeps/languages/rust.dag
index c239dde7e9e..e21222bec62 100644
--- a/src/v2/extdeps/languages/rust.dag
+++ b/src/v2/extdeps/languages/rust.dag
@@ -2084,7 +2084,10 @@ fn rust_binding_spellings() -> Map<Symbol, String> {
   let mx = map_insert(m2, ^dag_binding_param_x, "x")
   let my = map_insert(mx, ^dag_binding_param_y, "y")
   let mi = map_insert(my, ^dag_binding_type_int, "i32")
-  let m3 = map_insert(mi, ^rust_collection_surface_btree_set, "std::collections::BTreeSet")
+  let mb = map_insert(mi, ^rust_surface_spelling_bool, "bool")
+  let mc = map_insert(mb, ^rust_surface_spelling_char, "char")
+  let ms = map_insert(mc, ^rust_target_atom_type_spelling_string, "String")
+  let m3 = map_insert(ms, ^rust_collection_surface_btree_set, "std::collections::BTreeSet")
   let m4 = map_insert(m3, ^rust_collection_surface_hash_set, "std::collections::HashSet")
   let m5 = map_insert(m4, ^rust_collection_surface_vec, "Vec")
   map_insert(m5, ^target_collection_set_carrier, "Set")
@@ -2248,18 +2251,53 @@ data rust_target_function_signature_realization_catalog: List<TargetFunctionSign
   rust_target_function_signature_realization_symbol_return
 ]
 
+// HOW RUST REALIZES A WHERE-REFINEMENT DECLARATION: a TRANSPARENT ALIAS, `type Pos = i32;`. A refinement
+// restricts its carrier and adds no representation -- the predicate is discharged where a value crosses
+// into it (v2.compiler.refinement_discharge), and a crossing back to the carrier is realized as the
+// operand unchanged -- so the target names the carrier's own representation under the refinement's
+// name, and neither adds nor drops behaviour. A newtype would add construction and projection the source
+// never selected; emitting nothing would leave the refinement's uses naming a type that does not exist.
+// The row names the four token classes; the carrier's spelling is not here -- it is the carrier type's
+// own realization (v2.compiler.emit_produced produced_type_binding).
+fn rust_refinement_token_class_node(id: Symbol) -> Node {
+  Node {
+    kind: TypeNode { connective: Atom { identity: id } },
+    children: [],
+    occurrence_id: OccurrenceSynthetic
+  }
+}
+
+fn rust_refinement_declaration_realization_node() -> Node {
+  Node {
+    kind: TypeNode { connective: Conj },
+    children: [
+      rust_named_edge(name: ^refinement_declaration_field_keyword, target: rust_refinement_token_class_node(id: ^rust_token_kw_type)),
+      rust_named_edge(name: ^refinement_declaration_field_name, target: rust_refinement_token_class_node(id: ^rust_token_ident)),
+      rust_named_edge(name: ^refinement_declaration_field_assign, target: rust_refinement_token_class_node(id: ^rust_token_equal)),
+      rust_named_edge(name: ^refinement_declaration_field_terminator, target: rust_refinement_token_class_node(id: ^rust_token_semicolon))
+    ],
+    occurrence_id: OccurrenceSynthetic
+  }
+}
+
 fn rust_target_model_node() -> Node {
 
   Node {
     kind: TypeNode { connective: Conj },
     children: list_snoc_item(
-      xs: rust_target_model_core_edges(),
-      item: rust_named_edge(
-        name: ^target_model_edge_atom_realizations,
-        target: target_atom_realization_catalog_node(
-          rows: rust_target_atom_realization_catalog,
-          host_bundle: rust_target_model_bundle_core()
+      xs: list_snoc_item(
+        xs: rust_target_model_core_edges(),
+        item: rust_named_edge(
+          name: ^target_model_edge_atom_realizations,
+          target: target_atom_realization_catalog_node(
+            rows: rust_target_atom_realization_catalog,
+            host_bundle: rust_target_model_bundle_core()
+          )
         )
+      ),
+      item: rust_named_edge(
+        name: ^target_model_edge_refinement_declaration,
+        target: rust_refinement_declaration_realization_node()
       )
     ),
     occurrence_id: OccurrenceSynthetic
@@ -2338,6 +2376,7 @@ fn rust_value_expression_family_lex_rules() -> List<LexRule> {
     rust_lex_rule(token_class: ^rust_token_closure_pipe, text: "|"),
     rust_lex_rule(token_class: ^rust_token_closure_nop, text: ""),
     rust_lex_rule(token_class: ^rust_token_kw_let, text: "let "),
+    rust_lex_rule(token_class: ^rust_token_kw_type, text: "type "),
     rust_lex_rule(token_class: ^rust_token_equal, text: " = "),
     rust_lex_rule(token_class: ^rust_token_semicolon, text: "; "),
     rust_lex_rule(token_class: ^rust_token_kw_true, text: "true"),
diff --git a/src/v2/extdeps/languages/rust_test_fixtures.dag b/src/v2/extdeps/languages/rust_test_fixtures.dag
index 27820c89c74..f440ecf3ba2 100644
--- a/src/v2/extdeps/languages/rust_test_fixtures.dag
+++ b/src/v2/extdeps/languages/rust_test_fixtures.dag
@@ -980,7 +980,7 @@ fn rust_semantic_decl_target_model_staging() -> TargetModel {
       occurrence_id: OccurrenceSynthetic
     },
     lex: VoidLexRules,
-    binding_spellings: empty_map(),
+    binding_spellings: rust_binding_spellings(),
     token_class_emit_transforms: target_model_emit_transforms_empty,
     authority_source_text: "",
     runtime_row: target_emit_host_runtime_row_unconfigured
diff --git a/src/v2/extdeps/languages/swift.dag b/src/v2/extdeps/languages/swift.dag
index 733b61c8034..53f1700a870 100644
--- a/src/v2/extdeps/languages/swift.dag
+++ b/src/v2/extdeps/languages/swift.dag
@@ -641,7 +641,10 @@ fn swift_target_model_node() -> Node {
 }
 }
 
+// The kernel Int is realized as Swift's Int32, the width v2.extdeps.languages.rust rust_binding_spellings
+// gives it (`i32`); Swift's own `Int` is platform-width and would be a different realization.
 fn swift_binding_spellings() -> Map<Symbol, String> {
+  map_insert(
   map_insert(
     map_insert(
       map_insert(
@@ -658,6 +661,9 @@ fn swift_binding_spellings() -> Map<Symbol, String> {
     ),
     ^swift_binding_op_plus,
     "+"
+  ),
+  ^dag_binding_type_int,
+  "Int32"
   )
 }
 
diff --git a/src/v2/lens/module_graph.dag b/src/v2/lens/module_graph.dag
index 0d60310f81f..e9aee16637f 100644
--- a/src/v2/lens/module_graph.dag
+++ b/src/v2/lens/module_graph.dag
@@ -1,5 +1,6 @@
 module v2.lens.module_graph
 
+import v2.compiler.normalized_tree { normalized_tree_record_declarations }
 import std.dissolution { DissolutionCondition, unbound_dissolution }
 
 import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding }
@@ -300,7 +301,7 @@ fn located_roots_from_source_root_ingest(
               item: LocatedModuleRoot {
                 path: item.path,
                 root: item.tree.root,
-                record_declarations: item.tree.record_declarations
+                record_declarations: normalized_tree_record_declarations(t: item.tree)
               }
             )
           }
@@ -930,8 +931,8 @@ fn path_matches_touched(closure_path: String, touched_path: String) -> Bool {
   let file = strip_leading_dot_slash(closure_path)
   let target = strip_leading_dot_slash(touched_path)
   string_eq(a: file, b: target)
-    || ends_with(s: file, suffix: target)
-    || ends_with(s: target, suffix: file)
+    || file.ends_with(suffix: target)
+    || target.ends_with(suffix: file)
 }
 
 fn touched_path_in_closure(closure: FreeMonoid<String>, path: String) -> Bool {
diff --git a/src/v2/std/compilers/semantic_decl_emission.dag b/src/v2/std/compilers/semantic_decl_emission.dag
index 08d12d231cf..0419843d6dc 100644
--- a/src/v2/std/compilers/semantic_decl_emission.dag
+++ b/src/v2/std/compilers/semantic_decl_emission.dag
@@ -1,5 +1,6 @@
 module v2.std.compilers.semantic_decl_emission
 
+import v2.std.qualified_name { declaration_reference_path_optional }
 import std.occurrence_identity { OccurrenceSynthetic }
 import std.dissolution { DissolutionCondition, unbound_dissolution }
 
@@ -483,10 +484,20 @@ fn semantic_decl_binding_spelling_rows_from_catalog(catalog: Node) -> Outcome<Li
 
 fn semantic_decl_binding_spellings_from_rows(
   rows: List<SemanticDeclBindingSpellingRow>
+) -> Map<Symbol, String> {
+  semantic_decl_binding_spellings_from_rows_over(rows: rows, base: empty_map())
+}
+
+// The profile's rows laid over a base map: the host target's own binding_spellings, so a field type the
+// resolver bound to a target spelling (`i32`, `bool`) is spelled by the one map that owns it, and the
+// profile adds only its derive bindings.
+fn semantic_decl_binding_spellings_from_rows_over(
+  rows: List<SemanticDeclBindingSpellingRow>,
+  base: Map<Symbol, String>
 ) -> Map<Symbol, String> {
   fold_list(
     xs: rows,
-    empty: empty_map(),
+    empty: base,
     cons: fn(acc, row) {
       map_insert(m: acc, key: row.binding, value: row.spelling)
     }
@@ -549,13 +560,24 @@ fn semantic_decl_profile_lex_rules(
 
 fn semantic_decl_profile_binding_spellings(
   profile: TargetSemanticDeclSerializeProfile
+) -> Outcome<Map<Symbol, String>> {
+  semantic_decl_profile_binding_spellings_over(profile: profile, base: empty_map())
+}
+
+// The spellings a declaration is SERIALIZED with: the profile's rows over the host target's own map. The
+// serializer (semantic_decl_serialize_target) and the type resolver that admits a field type
+// (v2.compiler.emit_semantic_decl emit_semantic_type_decl) both read this one map, so a type is admitted
+// exactly when the serialization that follows can spell it.
+fn semantic_decl_profile_binding_spellings_over(
+  profile: TargetSemanticDeclSerializeProfile,
+  base: Map<Symbol, String>
 ) -> Outcome<Map<Symbol, String>> {
   bind_outcome(
     o: semantic_decl_binding_spelling_rows_from_row_nodes(
       rows: profile.binding_spelling_rows
     ),
     f: fn(rows) {
-      outcome_accepted(value: semantic_decl_binding_spellings_from_rows(rows: rows))
+      outcome_accepted(value: semantic_decl_binding_spellings_from_rows_over(rows: rows, base: base))
     }
   )
 }
@@ -629,13 +651,14 @@ fn semantic_decl_tokens_to_source_text(
 
 fn semantic_decl_serialize_target(
   profile: TargetSemanticDeclSerializeProfile,
-  rules: Node
+  rules: Node,
+  host_binding_spellings: Map<Symbol, String>
 ) -> Outcome<TargetModel> {
   bind_outcome(
     o: semantic_decl_profile_lex_rules(profile: profile),
     f: fn(lex) {
       bind_outcome(
-        o: semantic_decl_profile_binding_spellings(profile: profile),
+        o: semantic_decl_profile_binding_spellings_over(profile: profile, base: host_binding_spellings),
         f: fn(binding_spellings) {
           outcome_accepted(
             value: TargetModel {
@@ -1423,9 +1446,35 @@ fn target_semantic_decl_surface_field(
   }
 }
 
+// A FIELD'S TYPE IS SPELLED BY THE CALLER'S type_binding -- the same resolver a function signature's types
+// go through (v2.compiler.emit_produced produced_type_binding): a declared type's reference by the target's
+// declaration-reference form, a kernel carrier by its atom realization, else an explicit target spelling,
+// else refused. It was bound as the raw atom, so `a: Int` emitted `a: dag_binding_type_int`.
+fn target_semantic_decl_field_surface_resolved(
+  name: Symbol,
+  type_node: Node,
+  projection: TargetSemanticDeclSurfaceProjection,
+  type_binding: fn(Node) -> Outcome<Symbol>
+) -> Outcome<Node> {
+  bind_outcome(
+    o: type_binding(type_node),
+    f: fn(t) {
+      outcome_accepted(
+        value: target_semantic_decl_surface_field(
+          name: name,
+          t: t,
+          type_before_name: projection.field_type_before_name,
+          type_expr_field_scope: projection.type_expr_field_scope
+        )
+      )
+    }
+  )
+}
+
 fn target_semantic_decl_field_surface_from_edge(
   edge: Edge,
-  projection: TargetSemanticDeclSurfaceProjection
+  projection: TargetSemanticDeclSurfaceProjection,
+  type_binding: fn(Node) -> Outcome<Symbol>
 ) -> Outcome<Node> {
   match edge.label {
     Named { name: fname } =>
@@ -1438,21 +1487,19 @@ fn target_semantic_decl_field_surface_from_edge(
                   correction: Unavailable { reason: ExternalContractUnknown }
                 })
           } else {
-            outcome_accepted(
-              value: target_semantic_decl_surface_field(
-                name: fname,
-                t: tid,
-                type_before_name: projection.field_type_before_name,
-                type_expr_field_scope: projection.type_expr_field_scope
-              )
-            )
+            target_semantic_decl_field_surface_resolved(name: fname, type_node: edge.target, projection: projection, type_binding: type_binding)
           }
         _ =>
-          outcome_rejected(d: Diagnostic {
+          match declaration_reference_path_optional(node: edge.target) {
+            Present { value: _ } =>
+              target_semantic_decl_field_surface_resolved(name: fname, type_node: edge.target, projection: projection, type_binding: type_binding)
+            Absent =>
+              outcome_rejected(d: Diagnostic {
                 reason: ^target_semantic_decl_field_type_not_atom,
                 at: node_locus(node: edge.target),
                 correction: Unavailable { reason: ExternalContractUnknown }
               })
+          }
       }
     Positional =>
       outcome_rejected(d: Diagnostic {
@@ -1896,7 +1943,8 @@ fn target_semantic_decl_coproduct_decoration_lines(
 }
 fn target_semantic_decl_field_surfaces(
   edges: List<Edge>,
-  projection: TargetSemanticDeclSurfaceProjection
+  projection: TargetSemanticDeclSurfaceProjection,
+  type_binding: fn(Node) -> Outcome<Symbol>
 ) -> Outcome<List<Node>> {
   fold_list(
     xs: edges,
@@ -1908,7 +1956,8 @@ fn target_semantic_decl_field_surfaces(
           bind_outcome(
             o: target_semantic_decl_field_surface_from_edge(
               edge: edge,
-              projection: projection
+              projection: projection,
+              type_binding: type_binding
             ),
             f: fn(fnode) {
               outcome_accepted(value: list_snoc_item(xs: acc, item: fnode))
@@ -1922,7 +1971,8 @@ fn target_semantic_decl_field_surfaces(
 
 fn target_semantic_decl_tagged_union_variant_surface_from_edge(
   edge: Edge,
-  projection: TargetSemanticDeclSurfaceProjection
+  projection: TargetSemanticDeclSurfaceProjection,
+  type_binding: fn(Node) -> Outcome<Symbol>
 ) -> Outcome<Node> {
   match edge.label {
     Named { name: vname } =>
@@ -1930,7 +1980,8 @@ fn target_semantic_decl_tagged_union_variant_surface_from_edge(
         bind_outcome(
           o: target_semantic_decl_field_surfaces(
             edges: edge.target.children,
-            projection: projection
+            projection: projection,
+            type_binding: type_binding
           ),
           f: fn(fields) {
             outcome_accepted(
@@ -1955,7 +2006,8 @@ fn target_semantic_decl_tagged_union_variant_surface_from_edge(
 
 fn target_semantic_decl_tagged_union_variant_surfaces(
   edges: List<Edge>,
-  projection: TargetSemanticDeclSurfaceProjection
+  projection: TargetSemanticDeclSurfaceProjection,
+  type_binding: fn(Node) -> Outcome<Symbol>
 ) -> Outcome<List<Node>> {
   fold_list(
     xs: edges,
@@ -1967,7 +2019,8 @@ fn target_semantic_decl_tagged_union_variant_surfaces(
           bind_outcome(
             o: target_semantic_decl_tagged_union_variant_surface_from_edge(
               edge: edge,
-              projection: projection
+              projection: projection,
+              type_binding: type_binding
             ),
             f: fn(vnode) {
               outcome_accepted(value: list_snoc_item(xs: acc, item: vnode))
@@ -1981,7 +2034,8 @@ fn target_semantic_decl_tagged_union_variant_surfaces(
 
 fn target_semantic_decl_variant_surface_from_edge(
   edge: Edge,
-  projection: TargetSemanticDeclSurfaceProjection
+  projection: TargetSemanticDeclSurfaceProjection,
+  type_binding: fn(Node) -> Outcome<Symbol>
 ) -> Outcome<Node> {
   match edge.label {
     Named { name: vname } =>
@@ -1989,7 +2043,8 @@ fn target_semantic_decl_variant_surface_from_edge(
         bind_outcome(
           o: target_semantic_decl_field_surfaces(
             edges: edge.target.children,
-            projection: projection
+            projection: projection,
+            type_binding: type_binding
           ),
           f: fn(fields) {
             outcome_accepted(
@@ -2011,7 +2066,8 @@ fn target_semantic_decl_variant_surface_from_edge(
 
 fn target_semantic_decl_variant_surfaces(
   edges: List<Edge>,
-  projection: TargetSemanticDeclSurfaceProjection
+  projection: TargetSemanticDeclSurfaceProjection,
+  type_binding: fn(Node) -> Outcome<Symbol>
 ) -> Outcome<List<Node>> {
   fold_list(
     xs: edges,
@@ -2023,7 +2079,8 @@ fn target_semantic_decl_variant_surfaces(
           bind_outcome(
             o: target_semantic_decl_variant_surface_from_edge(
               edge: edge,
-              projection: projection
+              projection: projection,
+              type_binding: type_binding
             ),
             f: fn(vnode) {
               outcome_accepted(value: list_snoc_item(xs: acc, item: vnode))
@@ -2046,19 +2103,22 @@ fn target_semantic_decl_coproduct_uses_tagged_union_layout(
 
 fn target_semantic_decl_variant_surfaces_for_coproduct(
   projection: TargetSemanticDeclSurfaceProjection,
-  coproduct: Node
+  coproduct: Node,
+  type_binding: fn(Node) -> Outcome<Symbol>
 ) -> Outcome<List<Node>> {
   if target_semantic_decl_coproduct_uses_tagged_union_layout(layout: projection.coproduct_layout)
     && !coproduct_all_variants_nullary(edges: coproduct.children)
   {
     target_semantic_decl_tagged_union_variant_surfaces(
       edges: coproduct.children,
-      projection: projection
+      projection: projection,
+      type_binding: type_binding
     )
   } else {
     target_semantic_decl_variant_surfaces(
       edges: coproduct.children,
-      projection: projection
+      projection: projection,
+      type_binding: type_binding
     )
   }
 }
@@ -2092,7 +2152,8 @@ fn target_semantic_enum_surface_from_coproduct(
   projection: TargetSemanticDeclSurfaceProjection,
   name: Symbol,
   params: List<Symbol>,
-  coproduct: Node
+  coproduct: Node,
+  type_binding: fn(Node) -> Outcome<Symbol>
 ) -> Outcome<Node> {
   match type_decl_view(target: coproduct) {
     GenericTypeDecl { binders: _, member: _ } =>
@@ -2102,7 +2163,7 @@ fn target_semantic_enum_surface_from_coproduct(
     OpaqueTypeDecl { binders: _ } =>
       outcome_rejected(d: semantic_decl_not_a_member_diagnostic(decl: coproduct))
     PlainTypeDecl { member: m } =>
-      target_semantic_enum_surface_from_coproduct_admitted(projection: projection, name: name, params: params, coproduct: m)
+      target_semantic_enum_surface_from_coproduct_admitted(projection: projection, name: name, params: params, coproduct: m, type_binding: type_binding)
   }
 }
 
@@ -2110,7 +2171,8 @@ fn target_semantic_enum_surface_from_coproduct_admitted(
   projection: TargetSemanticDeclSurfaceProjection,
   name: Symbol,
   params: List<Symbol>,
-  coproduct: Node
+  coproduct: Node,
+  type_binding: fn(Node) -> Outcome<Symbol>
 ) -> Outcome<Node> {
   match coproduct.kind {
     TypeNode { connective: Disj } =>
@@ -2123,7 +2185,8 @@ fn target_semantic_enum_surface_from_coproduct_admitted(
           bind_outcome(
             o: target_semantic_decl_variant_surfaces_for_coproduct(
               projection: projection,
-              coproduct: coproduct
+              coproduct: coproduct,
+              type_binding: type_binding
             ),
             f: fn(variants) {
               if target_semantic_decl_coproduct_uses_tagged_union_layout(
@@ -2184,7 +2247,8 @@ fn target_semantic_struct_surface_from_record(
   projection: TargetSemanticDeclSurfaceProjection,
   name: Symbol,
   params: List<Symbol>,
-  record: Node
+  record: Node,
+  type_binding: fn(Node) -> Outcome<Symbol>
 ) -> Outcome<Node> {
   match type_decl_view(target: record) {
     GenericTypeDecl { binders: _, member: _ } =>
@@ -2194,7 +2258,7 @@ fn target_semantic_struct_surface_from_record(
     OpaqueTypeDecl { binders: _ } =>
       outcome_rejected(d: semantic_decl_not_a_member_diagnostic(decl: record))
     PlainTypeDecl { member: m } =>
-      target_semantic_struct_surface_from_record_admitted(projection: projection, name: name, params: params, record: m)
+      target_semantic_struct_surface_from_record_admitted(projection: projection, name: name, params: params, record: m, type_binding: type_binding)
   }
 }
 
@@ -2202,14 +2266,16 @@ fn target_semantic_struct_surface_from_record_admitted(
   projection: TargetSemanticDeclSurfaceProjection,
   name: Symbol,
   params: List<Symbol>,
-  record: Node
+  record: Node,
+  type_binding: fn(Node) -> Outcome<Symbol>
 ) -> Outcome<Node> {
   match record.kind {
     TypeNode { connective: Conj } =>
       bind_outcome(
         o: target_semantic_decl_field_surfaces(
           edges: record.children,
-          projection: projection
+          projection: projection,
+          type_binding: type_binding
         ),
         f: fn(fields) {
           if is_empty(xs: params) {
diff --git a/src/v2/std/compilers/target_model.dag b/src/v2/std/compilers/target_model.dag
index eb27706513a..aee44673328 100644
--- a/src/v2/std/compilers/target_model.dag
+++ b/src/v2/std/compilers/target_model.dag
@@ -370,29 +370,29 @@ fn produced_decl_render_diagnostic(reason: Symbol, node: Node) -> Diagnostic {
   }
 }
 
-// A type reference renders as one bound token in the target's identifier class. Any
-// other type shape REFUSES, typed and located -- never a fabricated spelling.
+// A type reference renders as one bound token in the target's identifier class, bound to what the
+// caller's type_binding resolves the type to: a declared type's reference spelled by the target's
+// declaration-reference form, a kernel carrier's atom realization, or an explicit target spelling
+// (v2.compiler.emit_produced
+// produced_type_binding). EVERY type shape is handed to the resolver, which is the one place that
+// decides a spelling or refuses, typed and located; the token is never bound to a type nothing resolved,
+// so the serializer's interned-name fallback cannot fabricate a type spelling.
 fn produced_decl_type_ref_tokens(
   token_class: Symbol,
-  type_node: Node
+  type_node: Node,
+  type_binding: fn(Node) -> Outcome<Symbol>
 ) -> Outcome<List<ConcreteSyntaxToken>> {
-  match type_node.kind {
-    TypeNode { connective: Atom { identity: id } } =>
-      outcome_accepted(value: [BoundToken { token_class: token_class, binding: id }])
-    _ =>
-      outcome_rejected(
-        d: produced_decl_render_diagnostic(
-          reason: ^produced_decl_render_type_shape_unsupported,
-          node: type_node
-        )
-      )
-  }
+  bind_outcome(
+    o: type_binding(type_node),
+    f: fn(binding) { outcome_accepted(value: [BoundToken { token_class: token_class, binding: binding }]) }
+  )
 }
 
 fn produced_decl_param_segment_tokens(
   rows: ProducedDeclRenderRows,
   edge: Edge,
-  segment: ProducedDeclParamSegment
+  segment: ProducedDeclParamSegment,
+  type_binding: fn(Node) -> Outcome<Symbol>
 ) -> Outcome<List<ConcreteSyntaxToken>> {
   match segment {
     ProducedParamFixed { token_class: tc } =>
@@ -412,7 +412,8 @@ fn produced_decl_param_segment_tokens(
     ProducedParamType =>
       produced_decl_type_ref_tokens(
         token_class: rows.type_ref_token_class,
-        type_node: edge.target
+        type_node: edge.target,
+        type_binding: type_binding
       )
   }
 }
@@ -420,7 +421,8 @@ fn produced_decl_param_segment_tokens(
 fn produced_decl_param_layout_tokens(
   rows: ProducedDeclRenderRows,
   edge: Edge,
-  layout: List<ProducedDeclParamSegment>
+  layout: List<ProducedDeclParamSegment>,
+  type_binding: fn(Node) -> Outcome<Symbol>
 ) -> Outcome<List<ConcreteSyntaxToken>> {
   fold_list(
     xs: layout,
@@ -430,7 +432,7 @@ fn produced_decl_param_layout_tokens(
         o: acc,
         f: fn(so_far) {
           bind_outcome(
-            o: produced_decl_param_segment_tokens(rows: rows, edge: edge, segment: segment),
+            o: produced_decl_param_segment_tokens(rows: rows, edge: edge, segment: segment, type_binding: type_binding),
             f: fn(toks) {
               outcome_accepted(value: list_append(left: so_far, right: toks))
             }
@@ -463,7 +465,8 @@ type ProducedDeclParamsFold {
 
 fn produced_decl_params_tokens(
   rows: ProducedDeclRenderRows,
-  params: List<Edge>
+  params: List<Edge>,
+  type_binding: fn(Node) -> Outcome<Symbol>
 ) -> Outcome<List<ConcreteSyntaxToken>> {
   bind_outcome(
     o: fold_list(
@@ -479,7 +482,8 @@ fn produced_decl_params_tokens(
               o: produced_decl_param_layout_tokens(
                 rows: rows,
                 edge: edge,
-                layout: rows.param_layout
+                layout: rows.param_layout,
+                type_binding: type_binding
               ),
               f: fn(toks) {
                 outcome_accepted(
@@ -513,7 +517,8 @@ fn produced_decl_params_tokens(
 fn produced_decl_signature_segment_tokens(
   rows: ProducedDeclRenderRows,
   subject: ProducedDeclSignatureSubject,
-  segment: ProducedDeclSignatureSegment
+  segment: ProducedDeclSignatureSegment,
+  type_binding: fn(Node) -> Outcome<Symbol>
 ) -> Outcome<List<ConcreteSyntaxToken>> {
   match segment {
     ProducedSignatureFixed { token_class: tc } =>
@@ -521,12 +526,13 @@ fn produced_decl_signature_segment_tokens(
     ProducedSignatureDeclName { token_class: tc } =>
       outcome_accepted(value: [BoundToken { token_class: tc, binding: subject.fn_name }])
     ProducedSignatureParams =>
-      produced_decl_params_tokens(rows: rows, params: subject.params)
+      produced_decl_params_tokens(rows: rows, params: subject.params, type_binding: type_binding)
     ProducedSignatureReturnType =>
       produced_decl_type_tokens_at(
         rows: rows,
         position: FunctionTypeAtItemReturn,
-        type_node: subject.codomain
+        type_node: subject.codomain,
+        type_binding: type_binding
       )
   }
 }
@@ -538,7 +544,8 @@ fn produced_decl_signature_segment_tokens(
 fn produced_decl_type_tokens_at(
   rows: ProducedDeclRenderRows,
   position: FunctionTypePosition,
-  type_node: Node
+  type_node: Node,
+  type_binding: fn(Node) -> Outcome<Symbol>
 ) -> Outcome<List<ConcreteSyntaxToken>> {
   match type_node.kind {
     TypeNode { connective: Arrow } =>
@@ -558,14 +565,16 @@ fn produced_decl_type_tokens_at(
                 o: produced_decl_function_type_params_tokens(
                   rows: rows,
                   sugar: row.sugar,
-                  params: shape.params
+                  params: shape.params,
+                  type_binding: type_binding
                 ),
                 f: fn(param_tokens) {
                   bind_outcome(
                     o: produced_decl_type_tokens_at(
                       rows: rows,
                       position: FunctionTypeAtFnBoundReturn,
-                      type_node: shape.codomain
+                      type_node: shape.codomain,
+                      type_binding: type_binding
                     ),
                     f: fn(return_tokens) {
                       outcome_accepted(
@@ -584,21 +593,23 @@ fn produced_decl_type_tokens_at(
             }
           )
       }
-    _ => produced_decl_type_ref_tokens(token_class: rows.type_ref_token_class, type_node: type_node)
+    _ => produced_decl_type_ref_tokens(token_class: rows.type_ref_token_class, type_node: type_node, type_binding: type_binding)
   }
 }
 
 fn produced_decl_function_type_param_tokens(
   rows: ProducedDeclRenderRows,
-  edge: Edge
+  edge: Edge,
+  type_binding: fn(Node) -> Outcome<Symbol>
 ) -> Outcome<List<ConcreteSyntaxToken>> {
-  produced_decl_type_ref_tokens(token_class: rows.type_ref_token_class, type_node: edge.target)
+  produced_decl_type_ref_tokens(token_class: rows.type_ref_token_class, type_node: edge.target, type_binding: type_binding)
 }
 
 fn produced_decl_function_type_params_tokens(
   rows: ProducedDeclRenderRows,
   sugar: FunctionTypeSugarRows,
-  params: List<Edge>
+  params: List<Edge>,
+  type_binding: fn(Node) -> Outcome<Symbol>
 ) -> Outcome<List<ConcreteSyntaxToken>> {
   bind_outcome(
     o: fold_list(
@@ -609,7 +620,7 @@ fn produced_decl_function_type_params_tokens(
           o: acc,
           f: fn(so_far) {
             bind_outcome(
-              o: produced_decl_function_type_param_tokens(rows: rows, edge: edge),
+              o: produced_decl_function_type_param_tokens(rows: rows, edge: edge, type_binding: type_binding),
               f: fn(toks) {
                 outcome_accepted(
                   value: ProducedDeclParamsFold {
@@ -643,7 +654,8 @@ fn produced_decl_function_type_params_tokens(
 fn produced_decl_signature_segments_tokens(
   rows: ProducedDeclRenderRows,
   subject: ProducedDeclSignatureSubject,
-  segments: List<ProducedDeclSignatureSegment>
+  segments: List<ProducedDeclSignatureSegment>,
+  type_binding: fn(Node) -> Outcome<Symbol>
 ) -> Outcome<List<ConcreteSyntaxToken>> {
   fold_list(
     xs: segments,
@@ -656,7 +668,8 @@ fn produced_decl_signature_segments_tokens(
             o: produced_decl_signature_segment_tokens(
               rows: rows,
               subject: subject,
-              segment: segment
+              segment: segment,
+              type_binding: type_binding
             ),
             f: fn(toks) {
               outcome_accepted(value: list_append(left: so_far, right: toks))
@@ -807,7 +820,8 @@ fn produced_decl_subject_from_decl(decl: Node) -> Outcome<ProducedDeclSignatureS
 
 fn produced_decl_signature_with_open_from_rows(
   rows: ProducedDeclRenderRows,
-  decl: Node
+  decl: Node,
+  type_binding: fn(Node) -> Outcome<Symbol>
 ) -> Outcome<List<ConcreteSyntaxToken>> {
   bind_outcome(
     o: produced_decl_subject_from_decl(decl: decl),
@@ -815,7 +829,8 @@ fn produced_decl_signature_with_open_from_rows(
       produced_decl_signature_segments_tokens(
         rows: rows,
         subject: subject,
-        segments: rows.signature
+        segments: rows.signature,
+        type_binding: type_binding
       )
     }
   )
@@ -825,10 +840,11 @@ fn produced_decl_signature_with_open_from_rows(
 // is the structural inverse of the target's rows and holds no per-target knowledge.
 fn produced_decl_render_from_rows(
   rows: ProducedDeclRenderRows,
-  decl: Node
+  decl: Node,
+  type_binding: fn(Node) -> Outcome<Symbol>
 ) -> Outcome<TargetBodiedArrowStatementScaffold> {
   bind_outcome(
-    o: produced_decl_signature_with_open_from_rows(rows: rows, decl: decl),
+    o: produced_decl_signature_with_open_from_rows(rows: rows, decl: decl, type_binding: type_binding),
     f: fn(signature_with_open) {
       outcome_accepted(
         derive_bodied_arrow_scaffold(
@@ -9289,7 +9305,8 @@ fn target_model_bundle_core_keep_edge(acc: List<Edge>, edge: Edge) -> List<Edge>
     Named { name: n } =>
 
       match n == ^target_model_edge_atom_realizations
-        || n == ^target_model_edge_signature_realizations {
+        || n == ^target_model_edge_signature_realizations
+        || n == ^target_model_edge_refinement_declaration {
         true => acc
         false => list_snoc_item(xs: acc, item: edge)
       }
@@ -15592,6 +15609,12 @@ fn target_project_arrow_body_to_value_expression(
 
 // The per-kind projection of a body classify_arrow_body_form did not classify as a function
 // value; a function-value body is dispatched above by its ArrowBodyForm, never by a raw kind here.
+// A TAIL ATOM IS THE SAME VALUE FORM AS A NESTED ONE. A body that is a bare parameter (`{ x }`) or a
+// bare literal (`{ true }`) is an Atom, and it projects through the one atom projection nested operands
+// already use (target_value_expr_project_atom_in_arrow_scope): a parameter binding first, then the
+// target's literal realizations, and an unresolved name refuses body_scope_binding_invalid. The Atom arm
+// used to accept only an integer literal and refuse every other atom as transform_shape_invalid, so a
+// bare-parameter or boolean body could not be emitted although the same atom emitted as an operand.
 fn target_project_arrow_body_by_kind(
   arrow: Node,
   body: Node,
@@ -15663,16 +15686,12 @@ fn target_project_arrow_body_by_kind(
           )
         }
       TypeNode { connective: Atom { identity: _ } } =>
-        if target_value_expr_is_int_literal_atom(node: body) {
-          target_value_expr_project_int_literal_atom(node: body)
-        } else {
-          outcome_rejected(
-            target_value_expr_diagnostic(
-              reason: ^target_value_expr_reason_transform_shape_invalid,
-              node: body
-            )
-          )
-        }
+        target_value_expr_project_atom_in_arrow_scope(
+          arrow: arrow,
+          node: body,
+          target: target,
+          source_bool_form: source_bool_form
+        )
       _ =>
         outcome_rejected(
           target_value_expr_diagnostic(
diff --git a/src/v2/test/claim/body_let_annotation_test.dag b/src/v2/test/claim/body_let_annotation_test.dag
index 339ab775c4d..1b13d518aea 100644
--- a/src/v2/test/claim/body_let_annotation_test.dag
+++ b/src/v2/test/claim/body_let_annotation_test.dag
@@ -406,7 +406,7 @@ fn bla_single_tree_resolved(text: String) -> Outcome<ResolvedTree> {
   match conservation_subject_of_text(path: "body_let_annotation_subject", text: text).normalized {
     Rejected { diagnostics: d } => Rejected { diagnostics: d }
     Accepted { value: t, diagnostics: _ } =>
-      match admit_normalized_tree(root: t.root, test_markers: t.test_markers, import_bindings: t.import_bindings, record_declarations: t.record_declarations, diagnostics: None) {
+      match admit_normalized_tree(root: t.root, test_markers: t.test_markers, import_bindings: t.import_bindings, type_declaration_kinds: t.type_declaration_kinds, diagnostics: None) {
         Rejected { diagnostics: d } => Rejected { diagnostics: d }
         Accepted { value: tree, diagnostics: _ } => resolve(tree: tree, lm: dag_language_model())
       }
@@ -614,7 +614,7 @@ fn bla_reordered_resolve(text: String) -> BlaReorderedResolve {
     Rejected { diagnostics: d } => BlaReorderedResolve { reordered: false, fatal: optional_present(value: diagnostics_fatal_reason(d: d)) }
     Accepted { value: t, diagnostics: _ } =>
       let root = bla_annotation_second(n: t.root)
-      match admit_normalized_tree(root: root, test_markers: t.test_markers, import_bindings: t.import_bindings, record_declarations: t.record_declarations, diagnostics: None) {
+      match admit_normalized_tree(root: root, test_markers: t.test_markers, import_bindings: t.import_bindings, type_declaration_kinds: t.type_declaration_kinds, diagnostics: None) {
         Rejected { diagnostics: d } => BlaReorderedResolve { reordered: false, fatal: optional_present(value: diagnostics_fatal_reason(d: d)) }
         Accepted { value: tree, diagnostics: _ } =>
           BlaReorderedResolve {
diff --git a/src/v2/test/claim/body_lowering/arrow_body_form_witness_test.dag b/src/v2/test/claim/body_lowering/arrow_body_form_witness_test.dag
index b1afde150df..47d069a4d2f 100644
--- a/src/v2/test/claim/body_lowering/arrow_body_form_witness_test.dag
+++ b/src/v2/test/claim/body_lowering/arrow_body_form_witness_test.dag
@@ -3,7 +3,7 @@ module v2.test.claim.body_lowering.arrow_body_form_witness
 import std.occurrence_identity { OccurrenceSynthetic }
 import v2.std.arrow_signature { declared_signature }
 import v2.std.declaration_marker { test_marker_channel_empty }
-import v2.compiler.normalized_tree { NormalizedTree, admit_normalized_tree, no_import_bindings, no_record_declarations}
+import v2.compiler.normalized_tree { NormalizedTree, admit_normalized_tree, no_import_bindings, no_type_declaration_kinds }
 import v2.compiler.resolve { resolve }
 import v2.extdeps.languages.dag {
   dag_add_arrow_with_body_node,
@@ -134,7 +134,7 @@ fn arrow_body_form_zero_arrow_fixture() -> Optional<Node> {
 // arm FAILS the witness rather than skipping it — an unadmittable fixture is a defect in
 // the fixture, not a reason to report green.
 fn abf_admitted_add_arrow_tree() -> Outcome<NormalizedTree> {
-  admit_normalized_tree(import_bindings: no_import_bindings(), record_declarations: no_record_declarations(), test_markers: test_marker_channel_empty(), root: dag_add_arrow_with_body_node(), diagnostics: None)
+  admit_normalized_tree(import_bindings: no_import_bindings(), type_declaration_kinds: no_type_declaration_kinds(), test_markers: test_marker_channel_empty(), root: dag_add_arrow_with_body_node(), diagnostics: None)
 }
 
 test fn arrow_body_form_eval_value_vertical_holds() -> Bool {
@@ -464,7 +464,7 @@ test fn arrow_body_form_reference_shape_without_marker_refused_holds() -> Bool {
 // ...and it reaches a gate that is not eval: resolve admits a normalized tree only if it is well
 // formed, so the unmarked shape is refused there before any evaluator runs.
 fn abf_admitted_unmarked_reference_tree() -> Outcome<NormalizedTree> {
-  admit_normalized_tree(import_bindings: no_import_bindings(), record_declarations: no_record_declarations(), test_markers: test_marker_channel_empty(), root: arrow_body_form_fixture_arrow_with_body(body: abf_reference_shaped_record()), diagnostics: None)
+  admit_normalized_tree(import_bindings: no_import_bindings(), type_declaration_kinds: no_type_declaration_kinds(), test_markers: test_marker_channel_empty(), root: arrow_body_form_fixture_arrow_with_body(body: abf_reference_shaped_record()), diagnostics: None)
 }
 
 test fn arrow_body_form_reference_shape_without_marker_refused_at_resolve_holds() -> Bool {
diff --git a/src/v2/test/claim/body_lowering/infer_transform_binary_infix_witness_helpers.dag b/src/v2/test/claim/body_lowering/infer_transform_binary_infix_witness_helpers.dag
index 4531bce8f14..083e4395a14 100644
--- a/src/v2/test/claim/body_lowering/infer_transform_binary_infix_witness_helpers.dag
+++ b/src/v2/test/claim/body_lowering/infer_transform_binary_infix_witness_helpers.dag
@@ -5,7 +5,7 @@ import v2.compiler.refinement_discharge { infer_and_discharge }
 import v2.compiler.infer { inferred_facts_grounding_derived, inferred_facts_witness_for_node }
 import v2.compiler.resolve { resolve }
 import v2.std.declaration_marker { test_marker_channel_empty }
-import v2.compiler.normalized_tree { admit_normalized_tree, no_import_bindings, no_record_declarations}
+import v2.compiler.normalized_tree { admit_normalized_tree, no_import_bindings, no_type_declaration_kinds }
 import v2.extdeps.languages.dag {
   dag_int_literal_fixture_one,
   dag_int_literal_fixture_two,
@@ -51,7 +51,7 @@ fn infer_transform_witness_resolved_add_arrow() -> Optional<Node> {
   match wave1_gate1_normalized_add_module() {
     Absent => Absent
     Present { value: tree } =>
-      match admit_normalized_tree(import_bindings: no_import_bindings(), record_declarations: no_record_declarations(), test_markers: test_marker_channel_empty(), root: tree, diagnostics: None) {
+      match admit_normalized_tree(import_bindings: no_import_bindings(), type_declaration_kinds: no_type_declaration_kinds(), test_markers: test_marker_channel_empty(), root: tree, diagnostics: None) {
         Rejected { diagnostics: _ } => Absent
         Accepted { value: normalized, diagnostics: _ } =>
           match resolve(tree: normalized, lm: dag_language_model()) {
diff --git a/src/v2/test/claim/body_lowering/wave1_gate1_normalize_add_helpers.dag b/src/v2/test/claim/body_lowering/wave1_gate1_normalize_add_helpers.dag
index 704fb14f3e8..ff72b56e2f4 100644
--- a/src/v2/test/claim/body_lowering/wave1_gate1_normalize_add_helpers.dag
+++ b/src/v2/test/claim/body_lowering/wave1_gate1_normalize_add_helpers.dag
@@ -3,7 +3,7 @@ module v2.test.claim.body_lowering.wave1_gate1_normalize_add_helpers
 import v2.compiler.reference_conservation_admission { conserved_normalize_of_text, no_explained_drops }
 import v2.compiler.normalize { normalize }
 import v2.std.declaration_marker { test_marker_channel_empty }
-import v2.compiler.normalized_tree { admit_normalized_tree, no_import_bindings, no_record_declarations}
+import v2.compiler.normalized_tree { admit_normalized_tree, no_import_bindings, no_type_declaration_kinds }
 import v2.compiler.parse { parse_module }
 import v2.compiler.resolve { resolve }
 import v2.compiler.tokenize { tokenize }
@@ -58,7 +58,7 @@ fn wave1_gate1_normalized_add_resolves_holds() -> Bool {
   match wave1_gate1_normalized_add_module() {
     Absent => false
     Present { value: tree } =>
-      match admit_normalized_tree(import_bindings: no_import_bindings(), record_declarations: no_record_declarations(), test_markers: test_marker_channel_empty(), root: tree, diagnostics: None) {
+      match admit_normalized_tree(import_bindings: no_import_bindings(), type_declaration_kinds: no_type_declaration_kinds(), test_markers: test_marker_channel_empty(), root: tree, diagnostics: None) {
         Rejected { diagnostics: _ } => false
         Accepted { value: normalized, diagnostics: _ } =>
           match resolve(tree: normalized, lm: dag_language_model()) {
@@ -93,7 +93,7 @@ fn wave1_gate1_resolved_add_arrow_transform_holds() -> Bool {
   match wave1_gate1_normalized_add_module() {
     Absent => false
     Present { value: tree } =>
-      match admit_normalized_tree(import_bindings: no_import_bindings(), record_declarations: no_record_declarations(), test_markers: test_marker_channel_empty(), root: tree, diagnostics: None) {
+      match admit_normalized_tree(import_bindings: no_import_bindings(), type_declaration_kinds: no_type_declaration_kinds(), test_markers: test_marker_channel_empty(), root: tree, diagnostics: None) {
         Rejected { diagnostics: _ } => false
         Accepted { value: normalized, diagnostics: _ } =>
           match resolve(tree: normalized, lm: dag_language_model()) {
diff --git a/src/v2/test/claim/claim_pipeline/resolve_test.dag b/src/v2/test/claim/claim_pipeline/resolve_test.dag
index 82603d4718f..2be96fbb260 100644
--- a/src/v2/test/claim/claim_pipeline/resolve_test.dag
+++ b/src/v2/test/claim/claim_pipeline/resolve_test.dag
@@ -3,7 +3,7 @@ module v2.test.claim_pipeline.resolve
 import std.occurrence_identity { OccurrenceSynthetic }
 import v2.compiler.normalize { normalize }
 import v2.std.declaration_marker { test_marker_channel_empty }
-import v2.compiler.normalized_tree { admit_normalized_tree, no_import_bindings, no_record_declarations}
+import v2.compiler.normalized_tree { admit_normalized_tree, no_import_bindings, no_type_declaration_kinds }
 import v2.compiler.resolve { resolve }
 import v2.extdeps.languages.dag {
   dag_language_model_surface_empty_prelude,
@@ -69,7 +69,7 @@ data spine_resolve_reject_module_subject: Node = Node {
 // self-bound every Atom node anywhere in the tree -- including this
 // reference -- so it resolved without ever consulting canonical_symbols.
 test fn spine_resolve_rejects_noncanonical_root_atom() -> Bool {
-  match admit_normalized_tree(import_bindings: no_import_bindings(), record_declarations: no_record_declarations(), test_markers: test_marker_channel_empty(), root: spine_resolve_reject_module_subject, diagnostics: None) {
+  match admit_normalized_tree(import_bindings: no_import_bindings(), type_declaration_kinds: no_type_declaration_kinds(), test_markers: test_marker_channel_empty(), root: spine_resolve_reject_module_subject, diagnostics: None) {
     Accepted { value: normalized, diagnostics: _ } =>
       match resolve(tree: normalized, lm: dag_language_model_surface_empty_prelude()) {
         Accepted { value: _, diagnostics: _ } => false
diff --git a/src/v2/test/claim/emit/c_semantic_decl_routing_test.dag b/src/v2/test/claim/emit/c_semantic_decl_routing_test.dag
index 79cc13edb9e..7ca2a89fa22 100644
--- a/src/v2/test/claim/emit/c_semantic_decl_routing_test.dag
+++ b/src/v2/test/claim/emit/c_semantic_decl_routing_test.dag
@@ -55,7 +55,7 @@ fn cdr_variant_edge_payload(name: Symbol, fields: List<Edge>) -> Edge {
 }
 
 fn cdr_emit_text(name: Symbol, node: Node) -> Outcome<String> {
-  match emit_semantic_type_decl(name: name, params: Empty, node: node, target: c_target_model()) {
+  match emit_semantic_type_decl(name: name, params: Empty, node: node, target: c_target_model(), realization_host: c_target_model()) {
     Accepted { value: medium, diagnostics: _ } => Accepted { value: medium.carried, diagnostics: None }
     Rejected { diagnostics: r } => Rejected { diagnostics: r }
   }
@@ -125,7 +125,8 @@ test fn c_semantic_non_int_field_refuses() -> Bool {
     name: ^Bad,
     params: [],
     node: cdr_bool_field_record(),
-    target: c_target_model()
+    target: c_target_model(),
+    realization_host: c_target_model()
   ) {
     Accepted { value: _, diagnostics: _ } => false
     Rejected { diagnostics: _ } => true
@@ -145,7 +146,8 @@ test fn c_semantic_generic_struct_refuses() -> Bool {
     name: ^Pair,
     params: [^K, ^V],
     node: cdr_point_record(),
-    target: c_target_model()
+    target: c_target_model(),
+    realization_host: c_target_model()
   ) {
     Accepted { value: _, diagnostics: _ } => false
     Rejected { diagnostics: _ } => true
@@ -157,7 +159,8 @@ test fn c_semantic_generic_tagged_union_refuses() -> Bool {
     name: ^Answer,
     params: [^T],
     node: cdr_answer_coproduct(),
-    target: c_target_model()
+    target: c_target_model(),
+    realization_host: c_target_model()
   ) {
     Accepted { value: _, diagnostics: _ } => false
     Rejected { diagnostics: _ } => true
diff --git a/src/v2/test/claim/emit/module_member_emission_test.dag b/src/v2/test/claim/emit/module_member_emission_test.dag
index 9e8cdaf50e8..8fbd86bda26 100644
--- a/src/v2/test/claim/emit/module_member_emission_test.dag
+++ b/src/v2/test/claim/emit/module_member_emission_test.dag
@@ -1,6 +1,8 @@
 module v2.test.claim.emit.module_member_emission
 
 import extdeps.communication.medium { Lossless, Medium }
+import v2.compiler.emit_produced { emit_module_member }
+import v2.compiler.body_lowering_fold { DeclaredRefinement }
 import v2.compiler.self_host.closure_emission {
   ClosureEmissionLocated, ClosureMemberEmitted, ClosureMemberRefused, emit_closure_from_ingest_located,
 }
@@ -11,7 +13,7 @@ import v2.std.cross_tree.import_model { DagTree }
 import v2.std.diagnostic { Accepted, Rejected, diagnostics_fatal_reason }
 import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
 import v2.std.logic { Bool }
-import v2.std.node { Node, Symbol, node_synthetic }
+import v2.std.node { Atom, Conj, Edge, Named, Node, Symbol, TypeNode, node_synthetic, symbol_lexeme }
 import v2.std.optional { Absent, Present }
 import v2.std.qualified_name { qualified_name_from_dotted_string }
 import v2.std.text { String }
@@ -94,6 +96,30 @@ fn member_emission_generic_verdict() -> MemberEmissionVerdict {
   member_emission_verdict_of(source: "module v2.test.member_emission\n\ntype Tag<T> = A | B\n\nfn f(x: Int) -> Int { x as Int }\n")
 }
 
+fn member_emission_payload_variant_verdict() -> MemberEmissionVerdict {
+  member_emission_verdict_of(source: "module v2.test.member_emission\n\ntype Wrapped = Only { a: Int }\n\nfn f(x: Int) -> Int { x as Int }\n")
+}
+
+fn member_emission_label_spelled_record_verdict() -> MemberEmissionVerdict {
+  member_emission_verdict_of(source: "module v2.test.member_emission\n\ntype Weird { dag_surface_where_refinement_clause: Int }\n\nfn f(x: Int) -> Int { x as Int }\n")
+}
+
+fn member_emission_bool_signature_verdict() -> MemberEmissionVerdict {
+  member_emission_verdict_of(source: "module v2.test.member_emission\n\nfn f(p: Bool) -> Bool { p }\n")
+}
+
+fn member_emission_declared_type_signature_verdict() -> MemberEmissionVerdict {
+  member_emission_verdict_of(source: "module v2.test.member_emission\n\ntype Decision = Allowed | Blocked\n\nfn f(d: Decision) -> Decision { d }\n")
+}
+
+fn member_emission_bare_parameter_body_verdict() -> MemberEmissionVerdict {
+  member_emission_verdict_of(source: "module v2.test.member_emission\n\nfn f(x: Int) -> Int { x }\n")
+}
+
+fn member_emission_bare_literal_body_verdict() -> MemberEmissionVerdict {
+  member_emission_verdict_of(source: "module v2.test.member_emission\n\nfn t() -> Bool { true }\n")
+}
+
 // A coproduct beside a function: BOTH are emitted, the enum first because it is declared first -- the
 // module's direct members in source order, the coproduct through the semantic-declaration emitter and
 // the function through the produced-declaration rows.
@@ -113,24 +139,126 @@ test fn a_coproduct_beside_a_function_emits_both_in_source_order_holds() -> Bool
   }
 }
 
-// A where-refinement shares a record's lowered shape, so it refuses as UNDECIDED at the member and is
-// never rendered as a struct; the function beside it is not published alone. The refinement is declared
-// FIRST so the fold, which refuses at the first member it cannot realize, reaches it before its
-// predicate: a literal-bodied function is a separate emission frontier (target_value_expr_reason_
-// transform_shape_invalid) that would otherwise answer this row for the wrong member.
-test fn a_where_refinement_is_not_emitted_as_a_record_holds() -> Bool {
+// A WHERE-REFINEMENT IS CLASSIFIED FROM ITS DECLARATION AND NEVER RENDERED AS A RECORD, although it shares a
+// record's lowered shape: on the production route (parse, normalize, lowered carrier) it emits the target's
+// transparent alias, not a struct. This is the route's inhabitance claim for the supplied row below.
+test fn a_where_refinement_emits_its_transparent_alias_on_the_production_route_holds() -> Bool {
   match member_emission_refinement_verdict() {
-    MemberEmitted { text: _ } => false
-    MemberRefused { reason: r } => r == ^emit_module_member_record_or_refinement_undecided
+    MemberEmitted { text: t } => string_contains(s: t, pattern: "type Pos = i32;") && !string_contains(s: t, pattern: "struct")
+    MemberRefused { reason: _ } => false
     MemberClosureRefused { reason: _ } => false
   }
 }
 
-// A genuine record refuses under the same undecided reason until the record fact reaches emission.
-test fn a_record_refuses_until_its_kind_reaches_emission_holds() -> Bool {
+// THE REFINEMENT REALIZATION ITSELF, over a SUPPLIED member whose carrier is already lowered (the form the
+// lowering above will produce): named in the module's refinement facts, it emits the target's transparent
+// alias, the carrier spelled by the one type resolver -- `type Pos = i32;`, never a struct. The inhabitance
+// partner is the route row above, which reaches the same arm for real.
+fn member_emission_supplied_refinement() -> String {
+  let member = Edge {
+    label: Named { name: ^Pos },
+    target: node_synthetic(
+      kind: TypeNode { connective: Conj },
+      children: [
+        Edge { label: Named { name: ^dag_surface_type_expr }, target: node_synthetic(kind: TypeNode { connective: Atom { identity: ^dag_binding_type_int } }, children: []) },
+        Edge { label: Named { name: ^dag_surface_where_refinement_clause }, target: node_synthetic(kind: TypeNode { connective: Atom { identity: ^positive } }, children: []) }
+      ]
+    )
+  }
+  match emit_module_member(
+    edge: member,
+    target: rust_target_model(),
+    realization_host: rust_target_model(),
+    kinds: [DeclaredRefinement { name: ^Pos }]
+  ) {
+    Accepted { value: m, diagnostics: _ } => m.carried
+    Rejected { diagnostics: d } => concat("REFUSED ", symbol_lexeme(sym: diagnostics_fatal_reason(d: d)))
+  }
+}
+
+test fn a_refinement_with_a_lowered_carrier_emits_a_transparent_alias_holds() -> Bool {
+  let text = member_emission_supplied_refinement()
+  string_contains(s: text, pattern: "type Pos = i32;") && !string_contains(s: text, pattern: "struct")
+}
+
+// A record -- a Conj its module's declaration kinds call DeclaredRecord -- emits as a struct beside the function, the
+// record through the semantic-declaration emitter and its field's Int through the target's spelling.
+test fn a_record_beside_a_function_emits_as_a_struct_holds() -> Bool {
   match member_emission_record_verdict() {
-    MemberEmitted { text: _ } => false
-    MemberRefused { reason: r } => r == ^emit_module_member_record_or_refinement_undecided
+    MemberEmitted { text: t } =>
+      string_contains(s: t, pattern: "struct Point")
+        && string_contains(s: t, pattern: "a: i32")
+        && !string_contains(s: t, pattern: "dag_binding_type_int")
+        && string_contains(s: t, pattern: "fn f(x: i32) -> i32")
+    MemberRefused { reason: _ } => false
+    MemberClosureRefused { reason: _ } => false
+  }
+}
+
+// A PAYLOAD-BEARING SINGLE VARIANT IS A ONE-ARM COPRODUCT, not a record and not an undecided Conj:
+// `type Wrapped = Only { a: Int }` lowers to a Disj, so it emits as an enum whose one variant carries its
+// field, spelled by the target.
+test fn a_payload_single_variant_emits_as_a_one_arm_enum_holds() -> Bool {
+  match member_emission_payload_variant_verdict() {
+    MemberEmitted { text: t } =>
+      string_contains(s: t, pattern: "enum Wrapped")
+        && string_contains(s: t, pattern: "Only")
+        && string_contains(s: t, pattern: "a: i32")
+        && !string_contains(s: t, pattern: "dag_binding_type_int")
+    MemberRefused { reason: _ } => false
+    MemberClosureRefused { reason: _ } => false
+  }
+}
+
+// THE KIND IS THE DECLARATION'S, NEVER ITS SPELLING: a record whose field is literally named like the
+// where-clause label is still a record, because the record fact says so.
+test fn a_record_with_a_where_labelled_field_is_still_a_record_holds() -> Bool {
+  match member_emission_label_spelled_record_verdict() {
+    MemberEmitted { text: t } => string_contains(s: t, pattern: "struct Weird")
+    MemberRefused { reason: _ } => false
+    MemberClosureRefused { reason: _ } => false
+  }
+}
+
+// A SIGNATURE TYPE IS SPELLED BY THE TARGET: Bool reaches Rust `bool` through its atom realization and
+// the target's spelling of that surface symbol -- never its carrier name `bool_node_symbol`.
+test fn a_bool_signature_is_spelled_by_its_realization_holds() -> Bool {
+  match member_emission_bool_signature_verdict() {
+    MemberEmitted { text: t } =>
+      string_contains(s: t, pattern: "fn f(p: bool) -> bool") && !string_contains(s: t, pattern: "bool_node_symbol")
+    MemberRefused { reason: _ } => false
+    MemberClosureRefused { reason: _ } => false
+  }
+}
+
+// A REFERENCE TO A DECLARED TYPE IS SPELLED BY THE TARGET'S DECLARATION-REFERENCE FORM -- the rule the
+// type-expression translate applies (v2.std.compilers.target_model
+// target_type_expr_declaration_reference_emitted): Rust's is crate-rooted, `crate::<module>::<Name>`,
+// the same for this module's types and another's, and never a bare leaf name. The enum it declares is
+// emitted beside the function that uses it.
+test fn a_declared_type_in_a_signature_keeps_its_name_holds() -> Bool {
+  match member_emission_declared_type_signature_verdict() {
+    MemberEmitted { text: t } =>
+      string_contains(s: t, pattern: "enum Decision")
+        && string_contains(s: t, pattern: "fn f(d: crate::v2_test_member_emission::Decision) -> crate::v2_test_member_emission::Decision")
+    MemberRefused { reason: _ } => false
+    MemberClosureRefused { reason: _ } => false
+  }
+}
+
+// A BARE PARAMETER OR LITERAL BODY is the same atom form as a nested operand and emits.
+test fn a_bare_parameter_body_emits_holds() -> Bool {
+  match member_emission_bare_parameter_body_verdict() {
+    MemberEmitted { text: t } => string_contains(s: t, pattern: "fn f(x: i32) -> i32 { x }")
+    MemberRefused { reason: _ } => false
+    MemberClosureRefused { reason: _ } => false
+  }
+}
+
+test fn a_bare_literal_body_emits_holds() -> Bool {
+  match member_emission_bare_literal_body_verdict() {
+    MemberEmitted { text: t } => string_contains(s: t, pattern: "fn t() -> bool { true }")
+    MemberRefused { reason: _ } => false
     MemberClosureRefused { reason: _ } => false
   }
 }
diff --git a/src/v2/test/claim/emit/produced_decl_support_preserved_test.dag b/src/v2/test/claim/emit/produced_decl_support_preserved_test.dag
index b65e92ad694..dc43099f6b2 100644
--- a/src/v2/test/claim/emit/produced_decl_support_preserved_test.dag
+++ b/src/v2/test/claim/emit/produced_decl_support_preserved_test.dag
@@ -22,9 +22,9 @@ import v2.std.compilers.target_model {
   target_model_type_atom_node
 }
 import v2.std.collection { List, list_at_optional, Absent, Present }
-import v2.std.diagnostic { Accepted, Outcome, Rejected, bind_outcome }
+import v2.std.diagnostic { Accepted, None, Outcome, Rejected, bind_outcome }
 import v2.std.logic { Bool }
-import v2.std.node { Node, Symbol }
+import v2.std.node { Atom, Node, Symbol, TypeNode }
 import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
 import v2.std.text { String }
 
@@ -82,7 +82,7 @@ fn pdp_target_with(support: ProducedDeclSupport) -> TargetModel {
 fn pdp_rendered_scaffold(rows: ProducedDeclRenderRows) -> Outcome<TargetBodiedArrowStatementScaffold> {
   bind_outcome(
     o: table_fixture_add_decl_node(fn_name: ^rust_binding_fn_add),
-    f: fn(decl) { produced_decl_render_from_rows(rows: rows, decl: decl) }
+    f: fn(decl) { produced_decl_render_from_rows(rows: rows, decl: decl, type_binding: fn(t) { produced_decl_support_type_as_itself(type_node: t) }) }
   )
 }
 
@@ -151,3 +151,13 @@ test fn produced_decl_support_survives_augmentation() -> Bool {
     && !pdp_after_value_semantics(support: ProducedDeclUnwired)
     && !pdp_after_use_site_ownership(support: ProducedDeclUnwired)
 }
+
+// This claim's subject is that produced-declaration support survives, not how a type is spelled, so its
+// type_binding binds an atom as itself -- the renderer's behaviour before type spelling was resolved by
+// the caller (v2.compiler.emit_produced produced_type_binding owns that).
+fn produced_decl_support_type_as_itself(type_node: Node) -> Outcome<Symbol> {
+  match type_node.kind {
+    TypeNode { connective: Atom { identity: id } } => Accepted { value: id, diagnostics: None }
+    _ => Accepted { value: ^produced_decl_support_non_atom_type, diagnostics: None }
+  }
+}
diff --git a/src/v2/test/claim/emit/rust_signature_general_emit_test.dag b/src/v2/test/claim/emit/rust_signature_general_emit_test.dag
index 155c3bbb8b2..5cfe6b85c66 100644
--- a/src/v2/test/claim/emit/rust_signature_general_emit_test.dag
+++ b/src/v2/test/claim/emit/rust_signature_general_emit_test.dag
@@ -1,6 +1,7 @@
 module v2.test.emit.rust_signature_general_emit
 
 import v2.test.complexity_gate.table_fixture_add_subject_producer { table_fixture_add_decl_node }
+import v2.compiler.emit_semantic_decl { produced_type_binding }
 import v2.compiler.translate { serialize_concrete_syntax_tokens_to_source }
 import v2.extdeps.languages.rust {
   rust_target_model_staging,
@@ -33,7 +34,8 @@ fn rust_signature_add_text() -> Outcome<String> {
       bind_outcome(
         o: produced_decl_signature_with_open_from_rows(
           rows: rust_produced_decl_render_rows,
-          decl: decl
+          decl: decl,
+          type_binding: produced_type_binding(target: rust_target_model_staging())
         ),
         f: fn(toks) {
           bind_outcome(
diff --git a/src/v2/test/claim/emit/semantic_decl_emit_substrings_test.dag b/src/v2/test/claim/emit/semantic_decl_emit_substrings_test.dag
index 26962fc138f..28b0c077d13 100644
--- a/src/v2/test/claim/emit/semantic_decl_emit_substrings_test.dag
+++ b/src/v2/test/claim/emit/semantic_decl_emit_substrings_test.dag
@@ -33,7 +33,8 @@ test fn emit_eq_golden() -> Bool {
     name: ^Bool,
     params: Empty,
     node: semantic_bool_coproduct(),
-    target: rust_semantic_decl_target_model_staging()
+    target: rust_semantic_decl_target_model_staging(),
+    realization_host: rust_semantic_decl_target_model_staging()
   ) {
     Accepted { value: m, diagnostics: _ } => m.carried == golden
     Rejected { diagnostics: _ } => false
diff --git a/src/v2/test/claim/emit/semantic_decl_routing_generic_test.dag b/src/v2/test/claim/emit/semantic_decl_routing_generic_test.dag
index d897e9029a4..a6224fdcd83 100644
--- a/src/v2/test/claim/emit/semantic_decl_routing_generic_test.dag
+++ b/src/v2/test/claim/emit/semantic_decl_routing_generic_test.dag
@@ -15,9 +15,9 @@ import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
 
 data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly
 
-data semantic_witness_golden: String = concat(rust_enum_derives, "\nenum Witness<C> { Holds { value: C }, Violates { diagnostic: Diagnostic } }")
+data semantic_witness_golden: String = concat(rust_enum_derives, "\nenum Witness<C> { Holds { value: C }, Violates { diagnostic: i32 } }")
 
-data semantic_witness_wrong_golden: String = concat(rust_enum_derives, "\nenum Witness<C> { Violates { diagnostic: Diagnostic }, Holds { value: C } }")
+data semantic_witness_wrong_golden: String = concat(rust_enum_derives, "\nenum Witness<C> { Violates { diagnostic: i32 }, Holds { value: C } }")
 
 data semantic_pair_golden: String = concat(rust_struct_derives, "\nstruct Pair<K, V> { key: K, value: V }")
 
@@ -44,7 +44,7 @@ fn semantic_witness_coproduct() -> Node {
     kind: TypeNode { connective: Disj },
     children: [
       sdrg_variant_edge(name: ^Holds, payload: sdrg_record(edges: [ sdrg_field_edge(name: ^value, type_name: ^C) ])),
-      sdrg_variant_edge(name: ^Violates, payload: sdrg_record(edges: [ sdrg_field_edge(name: ^diagnostic, type_name: ^Diagnostic) ]))
+      sdrg_variant_edge(name: ^Violates, payload: sdrg_record(edges: [ sdrg_field_edge(name: ^diagnostic, type_name: ^dag_binding_type_int) ]))
     ],
     occurrence_id: OccurrenceSynthetic
   }
@@ -55,7 +55,7 @@ fn semantic_pair_record() -> Node {
 }
 
 fn semantic_generic_emit_text(name: Symbol, params: List<Symbol>, node: Node) -> Outcome<String> {
-  match emit_semantic_type_decl(name: name, params: params, node: node, target: rust_semantic_decl_target_model_staging()) {
+  match emit_semantic_type_decl(name: name, params: params, node: node, target: rust_semantic_decl_target_model_staging(), realization_host: rust_semantic_decl_target_model_staging()) {
     Accepted { value: medium, diagnostics: _ } => Accepted { value: medium.carried, diagnostics: None }
     Rejected { diagnostics: r } => Rejected { diagnostics: r }
   }
diff --git a/src/v2/test/claim/emit/semantic_decl_routing_test.dag b/src/v2/test/claim/emit/semantic_decl_routing_test.dag
index c0046492e40..ab4c2a72e43 100644
--- a/src/v2/test/claim/emit/semantic_decl_routing_test.dag
+++ b/src/v2/test/claim/emit/semantic_decl_routing_test.dag
@@ -5,7 +5,7 @@ import v2.compiler.emit_semantic_decl { emit_semantic_type_decl }
 import v2.extdeps.languages.rust_test { rust_semantic_decl_target_model_staging }
 import extdeps.languages.rust.emit { rust_enum_derives_copy, rust_struct_derives }
 import std.algebra { Empty }
-import v2.std.diagnostic { Accepted, None, Outcome, Rejected }
+import v2.std.diagnostic { Accepted, None, Outcome, Rejected, diagnostics_fatal_reason }
 import v2.std.logic { Bool }
 import v2.std.arrow_signature { anonymous_signature_arrow }
 import v2.std.node { Atom, Conj, Disj, Edge, Named, Node, Positional, Symbol, TypeNode }
@@ -19,7 +19,7 @@ data semantic_bool_golden: String = concat(rust_enum_derives_copy, "\nenum Bool
 
 data semantic_bool_wrong_golden: String = concat(rust_enum_derives_copy, "\nenum Bool { False, True }")
 
-data semantic_record_golden: String = concat(rust_struct_derives, "\nstruct OccurrenceIdAllocator { next_id: Int }")
+data semantic_record_golden: String = concat(rust_struct_derives, "\nstruct OccurrenceIdAllocator { next_id: i32 }")
 
 data semantic_record_wrong_golden: String = concat(rust_struct_derives, "\nstruct OccurrenceIdAllocator { next_id: Bool }")
 
@@ -44,7 +44,8 @@ fn semantic_bool_emit_text() -> Outcome<String> {
     name: ^Bool,
     params: Empty,
     node: semantic_bool_coproduct(),
-    target: rust_semantic_decl_target_model_staging()
+    target: rust_semantic_decl_target_model_staging(),
+    realization_host: rust_semantic_decl_target_model_staging()
   ) {
     Accepted { value: medium, diagnostics: _ } => Accepted { value: medium.carried, diagnostics: None }
     Rejected { diagnostics: r } => Rejected { diagnostics: r }
@@ -69,7 +70,7 @@ fn sdr_field_edge(name: Symbol, type_name: Symbol) -> Edge {
 fn semantic_record_type() -> Node {
   Node {
     kind: TypeNode { connective: Conj },
-    children: [ sdr_field_edge(name: ^next_id, type_name: ^Int) ],
+    children: [ sdr_field_edge(name: ^next_id, type_name: ^dag_binding_type_int) ],
     occurrence_id: OccurrenceSynthetic
   }
 }
@@ -79,7 +80,8 @@ fn semantic_record_emit_text() -> Outcome<String> {
     name: ^OccurrenceIdAllocator,
     params: Empty,
     node: semantic_record_type(),
-    target: rust_semantic_decl_target_model_staging()
+    target: rust_semantic_decl_target_model_staging(),
+    realization_host: rust_semantic_decl_target_model_staging()
   ) {
     Accepted { value: medium, diagnostics: _ } => Accepted { value: medium.carried, diagnostics: None }
     Rejected { diagnostics: r } => Rejected { diagnostics: r }
@@ -93,6 +95,30 @@ fn semantic_record_matches(golden: String) -> Bool {
   }
 }
 
+// THE DISCRIMINATING RED FOR A FABRICATED SPELLING. A field whose type atom the target spells nowhere --
+// `^Int` is not the kernel carrier production lowers to, and Rust has no `Int` -- refuses at the type,
+// by name, where the route this replaced printed the interned `Int` into Rust source.
+fn semantic_unspelled_field_record() -> Node {
+  Node {
+    kind: TypeNode { connective: Conj },
+    children: [ sdr_field_edge(name: ^next_id, type_name: ^Int) ],
+    occurrence_id: OccurrenceSynthetic
+  }
+}
+
+test fn semantic_record_with_an_unspelled_field_type_refuses_by_name() -> Bool {
+  match emit_semantic_type_decl(
+    name: ^OccurrenceIdAllocator,
+    params: Empty,
+    node: semantic_unspelled_field_record(),
+    target: rust_semantic_decl_target_model_staging(),
+    realization_host: rust_semantic_decl_target_model_staging()
+  ) {
+    Accepted { value: _, diagnostics: _ } => false
+    Rejected { diagnostics: d } => diagnostics_fatal_reason(d: d) == ^produced_decl_type_ref_unrealized
+  }
+}
+
 test fn semantic_bool_coproduct_routes_to_enum_emit() -> Bool {
   semantic_bool_matches(golden: semantic_bool_golden)
     && !semantic_bool_matches(golden: semantic_bool_wrong_golden)
@@ -112,7 +138,8 @@ fn semantic_arrow_refuses() -> Bool {
     name: ^Bogus,
     params: Empty,
     node: semantic_arrow_type(),
-    target: rust_semantic_decl_target_model_staging()
+    target: rust_semantic_decl_target_model_staging(),
+    realization_host: rust_semantic_decl_target_model_staging()
   ) {
     Accepted { value: _, diagnostics: _ } => false
     Rejected { diagnostics: _ } => true
diff --git a/src/v2/test/claim/emit/semantic_decl_rules_parity_test.dag b/src/v2/test/claim/emit/semantic_decl_rules_parity_test.dag
index d560b5eef7f..52f3ca2b73c 100644
--- a/src/v2/test/claim/emit/semantic_decl_rules_parity_test.dag
+++ b/src/v2/test/claim/emit/semantic_decl_rules_parity_test.dag
@@ -1,5 +1,6 @@
 module v2.test.emit.semantic_decl_rules_parity_test
 
+import v2.compiler.emit_semantic_decl { produced_type_binding }
 import std.occurrence_identity { OccurrenceSynthetic }
 import v2.compiler.target_serialize { grammar_relation_row_for_emitted, grammar_relation_row_tokens_root }
 import v2.extdeps.languages.rust {
@@ -49,7 +50,8 @@ test fn emission_rules_match_rust_rules_for_generic_surface() -> Bool {
         projection: emission.surface,
         name: ^Bool,
         params: Empty,
-        coproduct: bool_coproduct()
+        coproduct: bool_coproduct(),
+        type_binding: produced_type_binding(target: rust_semantic_decl_target_model_staging())
       ) {
         Accepted { value: surface, diagnostics: _ } =>
           tokens_for_rules(surface: surface, rules: emission.enum_translation_rules)
diff --git a/src/v2/test/claim/emit/semantic_decl_serialize_parity_test.dag b/src/v2/test/claim/emit/semantic_decl_serialize_parity_test.dag
index 46752d3db82..49f96360abc 100644
--- a/src/v2/test/claim/emit/semantic_decl_serialize_parity_test.dag
+++ b/src/v2/test/claim/emit/semantic_decl_serialize_parity_test.dag
@@ -1,5 +1,7 @@
 module v2.test.emit.semantic_decl_serialize_parity
 
+import v2.std.collection { empty_map }
+import v2.compiler.emit_semantic_decl { produced_type_binding }
 import std.occurrence_identity { OccurrenceSynthetic }
 import v2.compiler.translate { serialize_concrete_syntax_tokens_to_source }
 import v2.compiler.target_serialize { grammar_relation_row_for_emitted, grammar_relation_row_tokens_root }
@@ -98,7 +100,8 @@ fn bool_text_with_target(target: TargetModel) -> Outcome<String> {
           projection: emission.surface,
           name: ^Bool,
           params: Empty,
-          coproduct: bool_coproduct()
+          coproduct: bool_coproduct(),
+          type_binding: produced_type_binding(target: rust_semantic_decl_target_model_staging())
         ),
         f: fn(surface) {
           serialize_surface_with_target(
@@ -121,7 +124,8 @@ test fn same_tokens_decoded_bindings_match_live_bindings() -> Bool {
             projection: emission.surface,
             name: ^Bool,
             params: Empty,
-            coproduct: bool_coproduct()
+            coproduct: bool_coproduct(),
+            type_binding: produced_type_binding(target: rust_semantic_decl_target_model_staging())
           ) {
             Accepted { value: surface, diagnostics: _ } =>
               match grammar_relation_row_for_emitted(
@@ -177,7 +181,8 @@ test fn same_tokens_decoded_lex_matches_live_lex() -> Bool {
             projection: emission.surface,
             name: ^Bool,
             params: Empty,
-            coproduct: bool_coproduct()
+            coproduct: bool_coproduct(),
+            type_binding: produced_type_binding(target: rust_semantic_decl_target_model_staging())
           ) {
             Accepted { value: surface, diagnostics: _ } =>
               match grammar_relation_row_for_emitted(
@@ -301,12 +306,14 @@ test fn generic_row_profile_matches_golden() -> Bool {
         projection: emission.surface,
         name: ^Bool,
         params: Empty,
-        coproduct: bool_coproduct()
+        coproduct: bool_coproduct(),
+        type_binding: produced_type_binding(target: rust_semantic_decl_target_model_staging())
       ) {
         Accepted { value: surface, diagnostics: _ } =>
           match semantic_decl_serialize_target(
             profile: emission.enum_serialize_profile,
-            rules: rust_enum_general_decl_productions_only_translation_rules()
+            rules: rust_enum_general_decl_productions_only_translation_rules(),
+            host_binding_spellings: empty_map()
           ) {
             Accepted { value: target, diagnostics: _ } =>
               match serialize_surface_with_target(
diff --git a/src/v2/test/claim/emit/semantic_decl_target_refusal_test.dag b/src/v2/test/claim/emit/semantic_decl_target_refusal_test.dag
index 37ebc92e464..67a76b15d10 100644
--- a/src/v2/test/claim/emit/semantic_decl_target_refusal_test.dag
+++ b/src/v2/test/claim/emit/semantic_decl_target_refusal_test.dag
@@ -36,7 +36,8 @@ fn sdtr_unwired_target_refuses() -> Bool {
     name: ^Bool,
     params: Empty,
     node: sdtr_bool_coproduct(),
-    target: cpp_target_model()
+    target: cpp_target_model(),
+    realization_host: cpp_target_model()
   ) {
     Accepted { value: _, diagnostics: _ } => false
     Rejected { diagnostics: _ } => true
diff --git a/src/v2/test/claim/emit/swift_semantic_decl_routing_test.dag b/src/v2/test/claim/emit/swift_semantic_decl_routing_test.dag
index 9ee0e5ef26b..eab28d49e98 100644
--- a/src/v2/test/claim/emit/swift_semantic_decl_routing_test.dag
+++ b/src/v2/test/claim/emit/swift_semantic_decl_routing_test.dag
@@ -18,21 +18,21 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly
 // exact text; each wrong golden differs in one fact the rows decide (member order, punctuation), so
 // a row that emitted plausible-but-wrong Swift reds here rather than passing a substring check.
 
-data swift_point_golden: String = "struct Point: Equatable, Sendable { let x: Int; let y: Int }"
+data swift_point_golden: String = "struct Point: Equatable, Sendable { let x: Int32; let y: Int32 }"
 
-data swift_point_wrong_golden: String = "struct Point: Equatable, Sendable { let y: Int; let x: Int }"
+data swift_point_wrong_golden: String = "struct Point: Equatable, Sendable { let y: Int32; let x: Int32 }"
 
 data swift_bool_golden: String = "enum Bool: Equatable, Sendable { case True, False }"
 
 data swift_bool_wrong_golden: String = "enum Bool: Equatable, Sendable { case False, True }"
 
-data swift_answer_golden: String = "enum Answer: Equatable, Sendable { case Yes(n: Int), No(code: Int) }"
+data swift_answer_golden: String = "enum Answer: Equatable, Sendable { case Yes(n: Int32), No(code: Int32) }"
 
-data swift_answer_rust_shaped_golden: String = "enum Answer: Equatable, Sendable { case Yes { n: Int }, No { code: Int } }"
+data swift_answer_rust_shaped_golden: String = "enum Answer: Equatable, Sendable { case Yes { n: Int32 }, No { code: Int32 } }"
 
 data swift_pair_golden: String = "struct Pair<K: Equatable & Sendable, V: Equatable & Sendable>: Equatable, Sendable { let key: K; let value: V }"
 
-data swift_wire_decode_golden: String = "enum WireDecode<T: Equatable & Sendable>: Equatable, Sendable { case WireDecoded(value: T), WireRefused(at: NonEmptyStr, cause: NonEmptyStr) }"
+data swift_wire_decode_golden: String = "enum WireDecode<T: Equatable & Sendable>: Equatable, Sendable { case WireDecoded(value: T), WireRefused(at: Int32, cause: Int32) }"
 
 fn sdr_empty_conj() -> Node {
   Node { kind: TypeNode { connective: Conj }, children: [], occurrence_id: OccurrenceSynthetic }
@@ -58,7 +58,7 @@ fn sdr_variant_edge_payload(name: Symbol, fields: List<Edge>) -> Edge {
 }
 
 fn sdr_emit_text(name: Symbol, params: List<Symbol>, node: Node) -> Outcome<String> {
-  match emit_semantic_type_decl(name: name, params: params, node: node, target: swift_target_model()) {
+  match emit_semantic_type_decl(name: name, params: params, node: node, target: swift_target_model(), realization_host: swift_target_model()) {
     Accepted { value: medium, diagnostics: _ } => Accepted { value: medium.carried, diagnostics: None }
     Rejected { diagnostics: r } => Rejected { diagnostics: r }
   }
@@ -74,7 +74,7 @@ fn sdr_emits(name: Symbol, params: List<Symbol>, node: Node, golden: String) ->
 fn sdr_point_record() -> Node {
   Node {
     kind: TypeNode { connective: Conj },
-    children: [ sdr_field_edge(name: ^x, type_name: ^Int), sdr_field_edge(name: ^y, type_name: ^Int) ],
+    children: [ sdr_field_edge(name: ^x, type_name: ^dag_binding_type_int), sdr_field_edge(name: ^y, type_name: ^dag_binding_type_int) ],
     occurrence_id: OccurrenceSynthetic
   }
 }
@@ -91,8 +91,8 @@ fn sdr_answer_coproduct() -> Node {
   Node {
     kind: TypeNode { connective: Disj },
     children: [
-      sdr_variant_edge_payload(name: ^Yes, fields: [ sdr_field_edge(name: ^n, type_name: ^Int) ]),
-      sdr_variant_edge_payload(name: ^No, fields: [ sdr_field_edge(name: ^code, type_name: ^Int) ])
+      sdr_variant_edge_payload(name: ^Yes, fields: [ sdr_field_edge(name: ^n, type_name: ^dag_binding_type_int) ]),
+      sdr_variant_edge_payload(name: ^No, fields: [ sdr_field_edge(name: ^code, type_name: ^dag_binding_type_int) ])
     ],
     occurrence_id: OccurrenceSynthetic
   }
@@ -115,7 +115,7 @@ fn sdr_wire_decode_coproduct() -> Node {
       sdr_variant_edge_payload(name: ^WireDecoded, fields: [ sdr_field_edge(name: ^value, type_name: ^T) ]),
       sdr_variant_edge_payload(
         name: ^WireRefused,
-        fields: [ sdr_field_edge(name: ^at, type_name: ^NonEmptyStr), sdr_field_edge(name: ^cause, type_name: ^NonEmptyStr) ]
+        fields: [ sdr_field_edge(name: ^at, type_name: ^dag_binding_type_int), sdr_field_edge(name: ^cause, type_name: ^dag_binding_type_int) ]
       )
     ],
     occurrence_id: OccurrenceSynthetic
diff --git a/src/v2/test/claim/execution/c_type_decl_emit_host_run_test.dag b/src/v2/test/claim/execution/c_type_decl_emit_host_run_test.dag
index 0b94a22de61..6f2a961884d 100644
--- a/src/v2/test/claim/execution/c_type_decl_emit_host_run_test.dag
+++ b/src/v2/test/claim/execution/c_type_decl_emit_host_run_test.dag
@@ -78,9 +78,9 @@ fn ctd_bool_coproduct() -> Node {
 }
 
 fn ctd_emit_decl_source() -> Medium<String> {
-  match emit_semantic_type_decl(name: ^Point, params: Empty, node: ctd_point_record(), target: c_type_decl_target_model()) {
+  match emit_semantic_type_decl(name: ^Point, params: Empty, node: ctd_point_record(), target: c_type_decl_target_model(), realization_host: c_type_decl_target_model()) {
     Accepted { value: point, diagnostics: _ } =>
-      match emit_semantic_type_decl(name: ^Bool, params: Empty, node: ctd_bool_coproduct(), target: c_type_decl_target_model()) {
+      match emit_semantic_type_decl(name: ^Bool, params: Empty, node: ctd_bool_coproduct(), target: c_type_decl_target_model(), realization_host: c_type_decl_target_model()) {
         Accepted { value: bool_decl, diagnostics: _ } =>
           Medium {
             carried: concat(concat(point.carried, bool_decl.carried), "\n"),
diff --git a/src/v2/test/claim/manual/body_lowering_normalize_add_test.dag b/src/v2/test/claim/manual/body_lowering_normalize_add_test.dag
index d04352fdbd4..48eead5fd56 100644
--- a/src/v2/test/claim/manual/body_lowering_normalize_add_test.dag
+++ b/src/v2/test/claim/manual/body_lowering_normalize_add_test.dag
@@ -8,7 +8,7 @@ import v2.compiler.body_lowering_fold {
   body_lower_unwrap_captured
 }
 import v2.std.declaration_marker { test_marker_channel_empty }
-import v2.compiler.normalized_tree { NormalizedTree, admit_normalized_tree, no_import_bindings, no_record_declarations}
+import v2.compiler.normalized_tree { NormalizedTree, admit_normalized_tree, no_import_bindings, no_type_declaration_kinds }
 import v2.compiler.normalize { normalize }
 import v2.compiler.resolve { resolve }
 import v2.compiler.parse { parse_module }
@@ -352,7 +352,7 @@ fn body_lowering_tree_contains_atom(root: Node, wanted: Symbol) -> Bool {
 
 test fn body_lowering_fixture_resolves() -> Bool {
   let lm = dag_language_model()
-  match admit_normalized_tree(import_bindings: no_import_bindings(), record_declarations: no_record_declarations(), test_markers: test_marker_channel_empty(), root: dag_add_arrow_with_body_fixture, diagnostics: None) {
+  match admit_normalized_tree(import_bindings: no_import_bindings(), type_declaration_kinds: no_type_declaration_kinds(), test_markers: test_marker_channel_empty(), root: dag_add_arrow_with_body_fixture, diagnostics: None) {
     Rejected { diagnostics: _ } => false
     Accepted { value: admitted, diagnostics: _ } =>
       match resolve(tree: admitted, lm: lm) {
@@ -722,7 +722,7 @@ test fn body_lowering_normalized_arrow_root_resolves() -> Bool {
       match body_lower_find_arrow_in_module(root: tree.root) {
         Absent => false
         Present { value: arrow } =>
-          match admit_normalized_tree(import_bindings: no_import_bindings(), record_declarations: no_record_declarations(), test_markers: test_marker_channel_empty(), root: arrow, diagnostics: None) {
+          match admit_normalized_tree(import_bindings: no_import_bindings(), type_declaration_kinds: no_type_declaration_kinds(), test_markers: test_marker_channel_empty(), root: arrow, diagnostics: None) {
             Rejected { diagnostics: _ } => false
             Accepted { value: admitted_arrow, diagnostics: _ } =>
               match resolve(tree: admitted_arrow, lm: lm) {
diff --git a/src/v2/test/claim/manual/resolve_compile_anchor_test.dag b/src/v2/test/claim/manual/resolve_compile_anchor_test.dag
index ec8e1c7b99a..1526b9f0a2e 100644
--- a/src/v2/test/claim/manual/resolve_compile_anchor_test.dag
+++ b/src/v2/test/claim/manual/resolve_compile_anchor_test.dag
@@ -2,7 +2,7 @@ module v2.test.manual.resolve_compile_anchor
 
 import std.occurrence_identity { OccurrenceSynthetic }
 import v2.std.declaration_marker { test_marker_channel_empty }
-import v2.compiler.normalized_tree { NormalizedTree, admit_unmarked_normalized_roots, admit_normalized_tree, no_import_bindings, no_record_declarations}
+import v2.compiler.normalized_tree { NormalizedTree, admit_unmarked_normalized_roots, admit_normalized_tree, no_import_bindings, no_type_declaration_kinds }
 import v2.compiler.name_resolve {
   Admission,
   Import,
@@ -61,7 +61,7 @@ fn service_atom_conj_tree() -> Node {
 }
 
 fn anchor_resolve_service_atom_via_canonical_symbols() -> Outcome<ResolvedTree> {
-  match admit_normalized_tree(import_bindings: no_import_bindings(), record_declarations: no_record_declarations(), test_markers: test_marker_channel_empty(), root: service_atom_conj_tree(), diagnostics: None) {
+  match admit_normalized_tree(import_bindings: no_import_bindings(), type_declaration_kinds: no_type_declaration_kinds(), test_markers: test_marker_channel_empty(), root: service_atom_conj_tree(), diagnostics: None) {
     Rejected { diagnostics: r } => Rejected { diagnostics: r }
     Accepted { value: tree, diagnostics: _ } =>
       resolve(tree: tree, lm: dag_language_model_void())
@@ -69,7 +69,7 @@ fn anchor_resolve_service_atom_via_canonical_symbols() -> Outcome<ResolvedTree>
 }
 
 fn anchor_resolve_empty_prelude_service_atom() -> Outcome<ResolvedTree> {
-  match admit_normalized_tree(import_bindings: no_import_bindings(), record_declarations: no_record_declarations(), test_markers: test_marker_channel_empty(), root: service_atom_conj_tree(), diagnostics: None) {
+  match admit_normalized_tree(import_bindings: no_import_bindings(), type_declaration_kinds: no_type_declaration_kinds(), test_markers: test_marker_channel_empty(), root: service_atom_conj_tree(), diagnostics: None) {
     Rejected { diagnostics: r } => Rejected { diagnostics: r }
     Accepted { value: tree, diagnostics: _ } =>
       resolve(tree: tree, lm: dag_language_model_surface_empty_prelude())
@@ -77,7 +77,7 @@ fn anchor_resolve_empty_prelude_service_atom() -> Outcome<ResolvedTree> {
 }
 
 fn anchor_resolve_multi_edge_conj_via_canonical_symbols() -> Outcome<ResolvedTree> {
-  match admit_normalized_tree(import_bindings: no_import_bindings(), record_declarations: no_record_declarations(), 
+  match admit_normalized_tree(import_bindings: no_import_bindings(), type_declaration_kinds: no_type_declaration_kinds(), 
     test_markers: test_marker_channel_empty(),
     root: Node {
       kind: TypeNode { connective: Conj },
@@ -113,7 +113,7 @@ fn anchor_resolve_multi_edge_conj_via_canonical_symbols() -> Outcome<ResolvedTre
 }
 
 fn anchor_resolve_bind_binder_use() -> Outcome<ResolvedTree> {
-  match admit_normalized_tree(import_bindings: no_import_bindings(), record_declarations: no_record_declarations(), 
+  match admit_normalized_tree(import_bindings: no_import_bindings(), type_declaration_kinds: no_type_declaration_kinds(), 
     test_markers: test_marker_channel_empty(),
     root: Node {
       kind: TypeNode { connective: Conj },
diff --git a/src/v2/test/claim/match_arm_binder_frame_test.dag b/src/v2/test/claim/match_arm_binder_frame_test.dag
index cd8cdd2479e..4bf71942058 100644
--- a/src/v2/test/claim/match_arm_binder_frame_test.dag
+++ b/src/v2/test/claim/match_arm_binder_frame_test.dag
@@ -1,5 +1,6 @@
 module v2.test.claim.match_arm_binder_frame
 
+import v2.compiler.normalized_tree { normalized_tree_record_declarations }
 import v2.compiler.resolve { ResolvedTree }
 import extdeps.communication.medium { Lossless, Medium }
 import v2.compiler.name_resolve {
@@ -341,7 +342,7 @@ fn mab_record_declarations(src: String) -> Outcome<FreeMonoid<Symbol>> {
               match normalize(parse_tree: artifact.tree) {
                 Rejected { diagnostics: r } => Rejected { diagnostics: r }
                 Accepted { value: tree, diagnostics: d } =>
-                  Accepted { value: tree.record_declarations, diagnostics: d }
+                  Accepted { value: normalized_tree_record_declarations(t: tree), diagnostics: d }
               }
           }
       }
diff --git a/src/v2/test/claim/name_resolve/admission_fail_closed_test.dag b/src/v2/test/claim/name_resolve/admission_fail_closed_test.dag
index 033c9f8b805..46e449e9dbd 100644
--- a/src/v2/test/claim/name_resolve/admission_fail_closed_test.dag
+++ b/src/v2/test/claim/name_resolve/admission_fail_closed_test.dag
@@ -19,7 +19,7 @@ import v2.compiler.name_resolve {
   validate_module_roots
 }
 import v2.std.declaration_marker { test_marker_channel_empty }
-import v2.compiler.normalized_tree { NormalizedTree, admit_normalized_tree, no_import_bindings, no_record_declarations}
+import v2.compiler.normalized_tree { NormalizedTree, admit_normalized_tree, no_import_bindings, no_type_declaration_kinds }
 import v2.std.cross_tree.resolution { source_root_index_empty }
 import v2.extdeps.languages.dag {
   dag_grammar_atom,
@@ -127,7 +127,7 @@ fn fc_with_roots(
 }
 
 fn fc_admitted(n: Node) -> Outcome<NormalizedTree> {
-  admit_normalized_tree(import_bindings: no_import_bindings(), record_declarations: no_record_declarations(), test_markers: test_marker_channel_empty(), root: n, diagnostics: None)
+  admit_normalized_tree(import_bindings: no_import_bindings(), type_declaration_kinds: no_type_declaration_kinds(), test_markers: test_marker_channel_empty(), root: n, diagnostics: None)
 }
 
 fn fc_duplicate_roots() -> Outcome<FreeMonoid<NormalizedTree>> {
diff --git a/src/v2/test/claim/name_resolve/malformed_imported_root_test.dag b/src/v2/test/claim/name_resolve/malformed_imported_root_test.dag
index 5ea98dfbae0..1fbb17f9c02 100644
--- a/src/v2/test/claim/name_resolve/malformed_imported_root_test.dag
+++ b/src/v2/test/claim/name_resolve/malformed_imported_root_test.dag
@@ -10,7 +10,7 @@ import v2.compiler.name_resolve {
   admit_import_entry
 }
 import v2.std.declaration_marker { test_marker_channel_empty }
-import v2.compiler.normalized_tree { NormalizedTree, admit_normalized_tree, no_import_bindings, no_record_declarations}
+import v2.compiler.normalized_tree { NormalizedTree, admit_normalized_tree, no_import_bindings, no_type_declaration_kinds }
 import v2.std.cross_tree.resolution { source_root_index_empty }
 import v2.std.diagnostic { Accepted, None, Outcome, Rejected, bind_outcome, outcome_accepted }
 import v2.extdeps.languages.dag {
@@ -64,7 +64,7 @@ fn malformed_entry_name() -> QualifiedName {
 }
 
 fn roots_with_malformed_entry() -> Outcome<FreeMonoid<NormalizedTree>> {
-  bind_outcome(o: admit_normalized_tree(import_bindings: no_import_bindings(), record_declarations: no_record_declarations(), test_markers: test_marker_channel_empty(), root: malformed_root_node(), diagnostics: None), f: fn(a) {
+  bind_outcome(o: admit_normalized_tree(import_bindings: no_import_bindings(), type_declaration_kinds: no_type_declaration_kinds(), test_markers: test_marker_channel_empty(), root: malformed_root_node(), diagnostics: None), f: fn(a) {
     outcome_accepted(value: Cons { head: a, tail: Empty })
   })
 }
diff --git a/src/v2/test/claim/name_resolve/one_member_cost_probe_test.dag b/src/v2/test/claim/name_resolve/one_member_cost_probe_test.dag
index ea26121683e..b8b5ef873e3 100644
--- a/src/v2/test/claim/name_resolve/one_member_cost_probe_test.dag
+++ b/src/v2/test/claim/name_resolve/one_member_cost_probe_test.dag
@@ -6,7 +6,7 @@ import v2.compiler.name_resolve {
   ResolutionSubject,
   resolve_with_admission
 }
-import v2.compiler.normalized_tree { NormalizedTree, admit_normalized_tree, no_import_bindings, no_record_declarations}
+import v2.compiler.normalized_tree { NormalizedTree, admit_normalized_tree, no_import_bindings, no_type_declaration_kinds }
 import v2.std.declaration_marker { test_marker_channel_empty }
 import v2.compiler.parse { parse_module }
 import v2.compiler.resolve { ResolvedTree }
@@ -72,7 +72,7 @@ fn probe_one_member_qn() -> QualifiedName {
 
 fn probe_roots_for_export(export_sym: Symbol) -> Outcome<FreeMonoid<NormalizedTree>> {
   bind_outcome(
-    o: admit_normalized_tree(import_bindings: no_import_bindings(), record_declarations: no_record_declarations(), 
+    o: admit_normalized_tree(import_bindings: no_import_bindings(), type_declaration_kinds: no_type_declaration_kinds(), 
       test_markers: test_marker_channel_empty(),
       root: probe_one_member_root_export(export_sym: export_sym),
       diagnostics: None
diff --git a/src/v2/test/claim/name_resolve/test_code_reference_wall_test.dag b/src/v2/test/claim/name_resolve/test_code_reference_wall_test.dag
index e8c70d9c2db..99474a7dc7a 100644
--- a/src/v2/test/claim/name_resolve/test_code_reference_wall_test.dag
+++ b/src/v2/test/claim/name_resolve/test_code_reference_wall_test.dag
@@ -111,7 +111,7 @@ fn wall_channel(marked: List<Symbol>) -> TestMarkerChannel {
 }
 
 fn wall_tree(root: Node, marked: List<Symbol>) -> Outcome<NormalizedTree> {
-  admit_normalized_tree(import_bindings: no_import_bindings(), record_declarations: no_record_declarations(), root: root, test_markers: wall_channel(marked: marked), diagnostics: None)
+  admit_normalized_tree(import_bindings: no_import_bindings(), type_declaration_kinds: no_type_declaration_kinds(), root: root, test_markers: wall_channel(marked: marked), diagnostics: None)
 }
 
 // THE PEER'S NAMES ARE BOUND, BECAUSE UNDER THE CANDIDATE RULE THAT IS THE ONLY WAY TO REACH THEM.
@@ -142,7 +142,7 @@ fn wall_peer_import_bindings() -> FreeMonoid<AliasBindingRow> {
 fn wall_tree_importing_peer(root: Node, marked: List<Symbol>) -> Outcome<NormalizedTree> {
   admit_normalized_tree(
     import_bindings: wall_peer_import_bindings(),
-    record_declarations: no_record_declarations(),
+    type_declaration_kinds: no_type_declaration_kinds(),
     root: root,
     test_markers: wall_channel(marked: marked),
     diagnostics: None
diff --git a/src/v2/test/claim/parse/parse_binding_fidelity_test.dag b/src/v2/test/claim/parse/parse_binding_fidelity_test.dag
index b5eed2410ab..4f0d14b22b2 100644
--- a/src/v2/test/claim/parse/parse_binding_fidelity_test.dag
+++ b/src/v2/test/claim/parse/parse_binding_fidelity_test.dag
@@ -2,7 +2,7 @@ module v2.test.parse.parse_binding_fidelity
 
 import std.occurrence_identity { OccurrenceSynthetic }
 import v2.std.declaration_marker { test_marker_channel_empty }
-import v2.compiler.normalized_tree { NormalizedTree, admit_unmarked_normalized_roots, admit_normalized_tree, no_import_bindings, no_record_declarations}
+import v2.compiler.normalized_tree { NormalizedTree, admit_unmarked_normalized_roots, admit_normalized_tree, no_import_bindings, no_type_declaration_kinds }
 import v2.compiler.name_resolve {
   Admission,
   Import,
@@ -202,7 +202,7 @@ fn pbf_unbound_atom_tree() -> Node {
 }
 
 fn pbf_resolve_unbound_symbol_rejects() -> Bool {
-  match admit_normalized_tree(import_bindings: no_import_bindings(), record_declarations: no_record_declarations(), test_markers: test_marker_channel_empty(), root: pbf_unbound_atom_tree(), diagnostics: None) {
+  match admit_normalized_tree(import_bindings: no_import_bindings(), type_declaration_kinds: no_type_declaration_kinds(), test_markers: test_marker_channel_empty(), root: pbf_unbound_atom_tree(), diagnostics: None) {
     Rejected { diagnostics: _ } => false
     Accepted { value: admitted_tree, diagnostics: _ } =>
   match resolve(
diff --git a/src/v2/test/claim/provenance/loaded_carrier_receipts_test.dag b/src/v2/test/claim/provenance/loaded_carrier_receipts_test.dag
index c59a299c7a7..ea27bbb1da2 100644
--- a/src/v2/test/claim/provenance/loaded_carrier_receipts_test.dag
+++ b/src/v2/test/claim/provenance/loaded_carrier_receipts_test.dag
@@ -1,7 +1,7 @@
 module v2.test.claim.provenance.loaded_carrier_receipts
 
 import v2.compiler.program_assembly { module_roots_from_source_root_ingest }
-import v2.compiler.normalized_tree { NormalizedTree, no_import_bindings }
+import v2.compiler.normalized_tree { NormalizedTree, no_import_bindings, normalized_tree_record_declarations }
 import v2.compiler.source_authority { DagSourceReadWitness, SourceRootIngest }
 import v2.compiler.symbol_index_fill { symbol_index_fill_module_roots }
 import v2.extdeps.languages.dag {
@@ -124,7 +124,7 @@ fn lcr_declaration_source_step(
     item: ModuleBindingSource {
       root: tree.root,
       import_bindings: no_import_bindings(),
-      record_declarations: tree.record_declarations
+      record_declarations: normalized_tree_record_declarations(t: tree)
     }
   )
 }
diff --git a/src/v2/test/claim/resolve/single_tree_module_body_test.dag b/src/v2/test/claim/resolve/single_tree_module_body_test.dag
index acc6c24f686..83f3125f9e6 100644
--- a/src/v2/test/claim/resolve/single_tree_module_body_test.dag
+++ b/src/v2/test/claim/resolve/single_tree_module_body_test.dag
@@ -2,7 +2,7 @@ module v2.test.claim.resolve.single_tree_module_body
 
 import std.algebra { Cons, Empty }
 import std.occurrence_identity { OccurrenceSynthetic }
-import v2.compiler.normalized_tree { admit_normalized_tree, no_import_bindings, no_record_declarations }
+import v2.compiler.normalized_tree { admit_normalized_tree, no_import_bindings, no_type_declaration_kinds }
 import v2.compiler.resolve { build_program_namespace }
 import v2.extdeps.languages.dag { dag_language_model }
 import v2.std.collection { map_lookup }
@@ -62,7 +62,7 @@ type StmbBinds
   | StmbBindings { leaked: Bool, t: Bool }
 
 fn stmb_binds(root: Node) -> StmbBinds {
-  match admit_normalized_tree(import_bindings: no_import_bindings(), record_declarations: no_record_declarations(), test_markers: test_marker_channel_empty(), root: root, diagnostics: None) {
+  match admit_normalized_tree(import_bindings: no_import_bindings(), type_declaration_kinds: no_type_declaration_kinds(), test_markers: test_marker_channel_empty(), root: root, diagnostics: None) {
     Rejected { diagnostics: _ } => StmbNotAdmitted
     Accepted { value: tree, diagnostics: _ } => {
       let ns = build_program_namespace(tree: tree, lm: dag_language_model())
diff --git a/src/v2/test/claim/type_param_binder_frame_test.dag b/src/v2/test/claim/type_param_binder_frame_test.dag
index 6693e596bf6..358c73e5de1 100644
--- a/src/v2/test/claim/type_param_binder_frame_test.dag
+++ b/src/v2/test/claim/type_param_binder_frame_test.dag
@@ -528,8 +528,15 @@ fn tpb_type_decl_emit_generic() -> Outcome<Node> {
 }
 
 test fn tpb_translator_refuses_a_generic_type_decl_member() -> Bool {
-  tpb_accepts(o: tpb_type_decl_emit_twin())
-    && tpb_refuses_with(o: tpb_type_decl_emit_generic(), reason: ^translate_reason_generic_type_decl_not_rendered)
+  let accepted = match tpb_type_decl_emit_twin() {
+    Accepted { value: _, diagnostics: _ } => true
+    Rejected { diagnostics: _ } => false
+  }
+  let refused = match tpb_type_decl_emit_generic() {
+    Accepted { value: _, diagnostics: _ } => false
+    Rejected { diagnostics: d } => diagnostics_fatal_reason(d: d) == ^translate_reason_generic_type_decl_not_rendered
+  }
+  accepted && refused
 }
 
 // A GENERIC DECLARATION'S BINDERS SIT BESIDE ITS MEMBER (v2.std.type_binder type_decl_wrapper), so a
@@ -603,7 +610,8 @@ fn tpb_semantic_emit(with_params: Bool) -> Outcome<Medium<String>> {
     name: ^Box,
     params: Empty,
     node: tpb_box_member(with_params: with_params),
-    target: rust_semantic_decl_target_model_staging()
+    target: rust_semantic_decl_target_model_staging(),
+    realization_host: rust_semantic_decl_target_model_staging()
   )
 }
 
diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag
index afc0f2948b0..c10ebdd7668 100644
--- a/src/v2/workflow/floor_pure_producer_share.dag
+++ b/src/v2/workflow/floor_pure_producer_share.dag
@@ -798,6 +798,13 @@ data floor_cross_claim_pure_producers_warm: List<String> = [
   "v2.test.claim.emit.module_member_emission.member_emission_alias_verdict",
   "v2.test.claim.emit.module_member_emission.member_emission_opaque_verdict",
   "v2.test.claim.emit.module_member_emission.member_emission_generic_verdict",
+  "v2.test.claim.emit.module_member_emission.member_emission_payload_variant_verdict",
+  "v2.test.claim.emit.module_member_emission.member_emission_label_spelled_record_verdict",
+  "v2.test.claim.emit.module_member_emission.member_emission_bool_signature_verdict",
+  "v2.test.claim.emit.module_member_emission.member_emission_declared_type_signature_verdict",
+  "v2.test.claim.emit.module_member_emission.member_emission_bare_parameter_body_verdict",
+  "v2.test.claim.emit.module_member_emission.member_emission_bare_literal_body_verdict",
+  "v2.test.claim.emit.module_member_emission.member_emission_supplied_refinement",
   "v2.test.execution.infer_declaration_formation.formation_coproduct_verdict",
   "v2.test.execution.infer_declaration_formation.formation_payload_coproduct_verdict",
   "v2.test.execution.infer_declaration_formation.formation_plain_alias_verdict",