diff --git a/src/v2/compiler/04_infer.dag b/src/v2/compiler/04_infer.dag
index 56bb4325fde..b4a07fc6d24 100644
--- a/src/v2/compiler/04_infer.dag
+++ b/src/v2/compiler/04_infer.dag
@@ -7,7 +7,11 @@ import v2.std.bounded_lattice_completeness {
   partial_bounded_lattice_instances_in_tree
 }
 import v2.compiler.resolve { ResolvedTree }
-import v2.extdeps.languages.dag { dag_node_is_int_literal_atom }
+import v2.extdeps.languages.dag {
+  DagCanonicalBoolLiteral,
+  DagCanonicalIntLiteral,
+  dag_canonical_literal_from_node
+}
 import v2.std.cardinality { TerminationProof, termination_proof_witness_for_node }
 import v2.std.collection {
   List,
@@ -24,9 +28,7 @@ import v2.std.optional {
 import v2.std.constraints {
   CanonicalGrounding,
   CanonicalGroundingWitness,
-  ConstraintGraph,
-  ConstraintSolvePolicy,
-  solve_constraints
+  canonical_grounding_from_derived_type
 }
 import v2.std.diagnostic {
   Diagnostic,
@@ -51,10 +53,14 @@ import v2.std.logic { Bool, bool_node }
 import v2.std.node {
   Arrow,
   Atom,
+  Bind,
   Branch,
+  Cardinality,
   ComputationNode,
   Conj,
+  Disj,
   Edge,
+  Instantiation,
   Loop,
   Match,
   Named,
@@ -62,7 +68,9 @@ import v2.std.node {
   NodeFold,
   Symbol,
   SyntheticOccurrence,
+  Transform,
   TypeNode,
+  Value,
   all_edges_positional,
   fold_node,
   loop_edge_contributes_to_iteration_fold,
@@ -78,21 +86,81 @@ type AlgebraRef {
   witness: Node
 }
 
+data node_grounding_frontier_note: String = "GroundingNotDerived is v2's typed inference frontier, not a failure arm and not an escape hatch. v2 derives a node's type for exactly three of the closed vocabulary's twelve node kinds (Branch, Match, Loop — 6 connectives + 6 behaviors = 12); the other nine have no derivation rule yet. Before this carrier existed the nine were routed through solve_constraints with the singleton candidate set [root] under a predicate that reduces to root == root, and the resulting grounding carried the SOURCE NODE as its structural evidence — i.e. as the node's resolved type (inferred_facts_resolved_type reads that field), so every literal, binding and operation in v2 was typed as itself and every downstream consumer read that as an established judgment. Each frontier node now carries a typed, located, counted diagnostic (infer_grounding_not_derived) on the Accepted path, so the deficit's frequency is observable and prioritizable rather than zeroed by construction (DESIGN §5). dissolve-on: a behavior-specific derivation rule lands for a kind, at which point that kind moves to DerivedGrounding and its frontier count drops; the carrier deletes when all twelve kinds derive."
+
+type NodeGrounding
+  = DerivedGrounding { grounding: CanonicalGrounding }
+  | GroundingNotDerived { node: Node }
+
 type InferredFacts {
-  grounding: CanonicalGrounding
+  grounding: NodeGrounding
   descent: Witness<v2.std.cardinality.TerminationProof>
 }
 
-fn inferred_facts_resolved_type(facts: InferredFacts) -> Node {
-  facts.grounding.witness.structural.evidence
+fn infer_grounding_not_derived_diagnostic(at: Locus) -> Diagnostic {
+  Diagnostic {
+    reason: ^infer_grounding_not_derived,
+    at: at,
+    correction: Unavailable { reason: ExternalContractUnknown }
+  }
+}
+
+fn inferred_facts_subject_node(facts: InferredFacts) -> Node {
+  match facts.grounding {
+    DerivedGrounding { grounding: g } => g.node
+    GroundingNotDerived { node: n } => n
+  }
+}
+
+fn inferred_facts_cover_node(facts: InferredFacts, node: Node) -> Bool {
+  inferred_facts_subject_node(facts: facts) == node
+}
+
+fn inferred_facts_grounding_derived(facts: InferredFacts) -> Bool {
+  match facts.grounding {
+    DerivedGrounding { grounding: _ } => true
+    GroundingNotDerived { node: _ } => false
+  }
+}
+
+fn inferred_facts_canonical_admitted(facts: InferredFacts) -> Bool {
+  match facts.grounding {
+    DerivedGrounding { grounding: g } => canonical_grounding_admits_infer_facts(grounding: g)
+    GroundingNotDerived { node: _ } => false
+  }
+}
+
+fn inferred_facts_grounding_witness(facts: InferredFacts) -> Witness<CanonicalGrounding> {
+  match facts.grounding {
+    DerivedGrounding { grounding: g } => Holds { value: g }
+    GroundingNotDerived { node: n } =>
+      Violates { diagnostic: infer_grounding_not_derived_diagnostic(at: node_locus(node: n)) }
+  }
+}
+
+fn inferred_facts_resolved_type(facts: InferredFacts) -> Witness<Node> {
+  match facts.grounding {
+    DerivedGrounding { grounding: g } => Holds { value: g.witness.structural.evidence }
+    GroundingNotDerived { node: n } =>
+      Violates { diagnostic: infer_grounding_not_derived_diagnostic(at: node_locus(node: n)) }
+  }
 }
 
-fn inferred_facts_algebra_ref(facts: InferredFacts) -> AlgebraRef {
-  algebra_ref_from_grounding(grounding: facts.grounding)
+fn inferred_facts_algebra_ref(facts: InferredFacts) -> Witness<AlgebraRef> {
+  match facts.grounding {
+    DerivedGrounding { grounding: g } =>
+      Holds { value: algebra_ref_from_grounding(grounding: g) }
+    GroundingNotDerived { node: n } =>
+      Violates { diagnostic: infer_grounding_not_derived_diagnostic(at: node_locus(node: n)) }
+  }
 }
 
-fn inferred_facts_canonical_witness(facts: InferredFacts) -> CanonicalGroundingWitness {
-  facts.grounding.witness
+fn inferred_facts_canonical_witness(facts: InferredFacts) -> Witness<CanonicalGroundingWitness> {
+  match facts.grounding {
+    DerivedGrounding { grounding: g } => Holds { value: g.witness }
+    GroundingNotDerived { node: n } =>
+      Violates { diagnostic: infer_grounding_not_derived_diagnostic(at: node_locus(node: n)) }
+  }
 }
 
 fn inferred_facts_descent(facts: InferredFacts) -> Witness<v2.std.cardinality.TerminationProof> {
@@ -267,6 +335,8 @@ fn algebra_ref_from_grounding(grounding: CanonicalGrounding) -> AlgebraRef {
   }
 }
 
+data canonical_grounding_admission_scope_note: String = "This predicate deliberately does NOT carry an 'evidence != node' conjunct, and the reason is worth recording because that conjunct was tried and withdrawn. As a read-path backstop against hand-built self-groundings it looked free, but it is a PROXY for the property actually at issue — 'was this grounding produced by a derivation?' — and the NodeGrounding carrier already answers that exactly. Proxies are what produced the defect in the first place: algebra_ref_is_grounded is a shape test on the connective, which is precisely why Conj/Disj type-node self-groundings walked through it. The proxy also has real false positives: v2_evaluator's bool fixture uses ONE atom as both the evaluand and the runtime value's primitive_type, so resolved == algebra there is the fixture's coherent encoding of 'this atom denotes Bool', not a fabrication. Refusing it would have meant rewriting a thesis-proof fixture to make a check go green — the inversion DESIGN §5 names explicitly. The wall therefore lives where it is exact: canonical_grounding_from_derived_type refuses self-evidence for every grounding the COMPILER mints, and GroundingNotDerived is what an underived node carries. A structurally hand-written CanonicalGrounding remains writable by any module; that residue is stated, not silently covered."
+
 fn canonical_grounding_admits_infer_facts(grounding: CanonicalGrounding) -> Bool {
   well_formed(n: grounding.node)
     && well_formed(n: grounding.witness.structural.evidence)
@@ -282,7 +352,7 @@ fn inferred_facts_construction(
   if canonical_grounding_admits_infer_facts(grounding: grounding) {
     Accepted {
       value: InferredFacts {
-        grounding: grounding,
+        grounding: DerivedGrounding { grounding: grounding },
         descent: descent
       },
       diagnostics: None
@@ -301,6 +371,23 @@ fn inferred_facts_from_grounding(
   inferred_facts_construction(grounding: grounding, descent: descent)
 }
 
+fn inferred_facts_not_derived(
+  node: Node,
+  descent: Witness<v2.std.cardinality.TerminationProof>,
+) -> Outcome<InferredFacts> {
+  Accepted {
+    value: InferredFacts {
+      grounding: GroundingNotDerived { node: node },
+      descent: descent
+    },
+    diagnostics: Some {
+      diagnostics: diagnostics_singleton(
+        d: infer_grounding_not_derived_diagnostic(at: node_locus(node: node))
+      )
+    }
+  }
+}
+
 fn empty_inferred_facts_entry_list() -> List<InferredFactsEntry> {
   []
 }
@@ -314,22 +401,7 @@ fn concat_inferred_facts_entries(
   })
 }
 
-fn infer_constraint_graph(n: Node) -> ConstraintGraph {
-  ConstraintGraph { root: n }
-}
-
-fn infer_grounding_from_constraint_solve(grounding: CanonicalGrounding) -> CanonicalGrounding {
-  CanonicalGrounding {
-    node: grounding.node,
-    witness: CanonicalGroundingWitness {
-      structural: StructuralPropertyWitness {
-        property: ^constraint_property_being_canonical,
-        evidence: grounding.witness.structural.evidence
-      },
-      closedness: grounding.witness.closedness
-    }
-  }
-}
+data infer_node_facts_no_derivation_note: String = "infer_node_facts used to reach solve_constraints with the singleton candidate set [root] and the constraint-satisfaction predicate, whose preservation rule is (algebra == source_facts && candidate == source_facts) with algebra bound to the root itself — so the witness search reduced to root == root and always succeeded. The grounding it minted carried the source node as its own structural evidence, which inferred_facts_resolved_type reads as the node's resolved type. That is source identity standing where a derivation belongs. The Bool and Int arms now consume the typed canonical-literal query and raise those derivations to leaf facts; every other node on this path carries the typed GroundingNotDerived frontier. solve_constraints itself is untouched — it remains the structural-solve authority named by dag/gunbc/plans/solve_higher_order_design.dag, to be EXTENDED with real candidate generation, never forked."
 
 fn infer_node_facts(n: Node, partials: List<Node>) -> Outcome<InferredFacts> {
   match infer_bounded_lattice_consumer_gate(consumer: n, partials: partials) {
@@ -339,19 +411,25 @@ fn infer_node_facts(n: Node, partials: List<Node>) -> Outcome<InferredFacts> {
         Violates { diagnostic: d } =>
           Rejected { diagnostics: diagnostics_singleton(d: d) }
         Holds { value: descent_proof } =>
-          bind_outcome(
-            o: solve_constraints(
-              policy: ConstraintSolvePolicy {
-                graph: infer_constraint_graph(n: n)
-              }
-            ),
-            f: fn(grounding) {
-              inferred_facts_from_grounding(
-                grounding: infer_grounding_from_constraint_solve(grounding: grounding),
+          match dag_canonical_literal_from_node(node: n) {
+            Accepted { value: DagCanonicalBoolLiteral { value: _ }, diagnostics: _ } =>
+              inferred_facts_from_derived_type(
+                node: n,
+                derived_type: bool_node(),
                 descent: Holds { value: descent_proof }
               )
-            }
-          )
+            Accepted { value: DagCanonicalIntLiteral { magnitude: _ }, diagnostics: _ } =>
+              inferred_facts_from_derived_type(
+                node: n,
+                derived_type: infer_branch_int_binding_type_node(),
+                descent: Holds { value: descent_proof }
+              )
+            Rejected { diagnostics: _ } =>
+              inferred_facts_not_derived(
+                node: n,
+                descent: Holds { value: descent_proof }
+              )
+          }
       }
   }
 }
@@ -382,7 +460,7 @@ fn facts_map_from_entries(entries: List<InferredFactsEntry>) -> Outcome<Map<Node
     match acc {
       Rejected { diagnostics: r } => Rejected { diagnostics: r }
       Accepted { value: ok_entries, diagnostics: d } =>
-        if entry.node == entry.facts.grounding.node {
+        if inferred_facts_cover_node(facts: entry.facts, node: entry.node) {
           Accepted { value: list_snoc_item(xs: ok_entries, item: entry), diagnostics: d }
         } else {
           Rejected {
@@ -414,17 +492,22 @@ fn canonical_grounding_from_inferred_facts(
   node: Node,
   facts: InferredFacts,
 ) -> Outcome<CanonicalGrounding> {
-  if node != facts.grounding.node {
-    outcome_rejected(infer_canonical_grounding_incoherent_diagnostic(node: node))
-  } else if !algebra_ref_is_grounded(algebra: inferred_facts_algebra_ref(facts: facts).algebra) {
-    outcome_rejected(infer_algebra_ref_ungrounded_diagnostic(node: node))
-  } else if canonical_grounding_admits_infer_facts(grounding: facts.grounding) {
-    Accepted {
-      value: facts.grounding,
-      diagnostics: None
-    }
-  } else {
-    outcome_rejected(infer_canonical_grounding_incoherent_diagnostic(node: node))
+  match facts.grounding {
+    GroundingNotDerived { node: n } =>
+      outcome_rejected(infer_grounding_not_derived_diagnostic(at: node_locus(node: n)))
+    DerivedGrounding { grounding: g } =>
+      if node != g.node {
+        outcome_rejected(infer_canonical_grounding_incoherent_diagnostic(node: node))
+      } else if !algebra_ref_is_grounded(algebra: algebra_ref_from_grounding(grounding: g).algebra) {
+        outcome_rejected(infer_algebra_ref_ungrounded_diagnostic(node: node))
+      } else if canonical_grounding_admits_infer_facts(grounding: g) {
+        Accepted {
+          value: g,
+          diagnostics: None
+        }
+      } else {
+        outcome_rejected(infer_canonical_grounding_incoherent_diagnostic(node: node))
+      }
   }
 }
 
@@ -438,7 +521,7 @@ fn canonical_grounding_for_node(tree: InferredTree, node: Node) -> Outcome<Canon
 }
 
 fn admitted_inferred_facts_entry(node: Node, facts: InferredFacts) -> Outcome<InferredFactsEntry> {
-  if node == facts.grounding.node {
+  if inferred_facts_cover_node(facts: facts, node: node) {
     Accepted {
       value: InferredFactsEntry { node: node, facts: facts },
       diagnostics: None
@@ -456,18 +539,6 @@ fn infer_branch_int_binding_type_node() -> Node {
   }
 }
 
-fn infer_branch_is_bool_literal_atom(node: Node) -> Bool {
-  match node.kind {
-    TypeNode { connective: Atom { identity: id } } =>
-      (id == ^dag_token_kw_true) || (id == ^dag_token_kw_false)
-    _ => false
-  }
-}
-
-fn infer_branch_is_int_literal_atom(node: Node) -> Bool {
-  dag_node_is_int_literal_atom(node: node)
-}
-
 fn infer_atom_binding_sym(node: Node) -> Optional<Symbol> {
   match node.kind {
     TypeNode { connective: Atom { identity: sym } } => Present { value: sym }
@@ -527,45 +598,45 @@ fn infer_find_arrow_domain_type_in_tree(root: Node, binding: Symbol) -> Optional
   }
 }
 
+data infer_branch_operand_type_frontier_note: String = "The literal and arrow-domain arms below derive a real type for the operand; the remaining arm falls through to the operand's own inferred facts. When those facts are the GroundingNotDerived frontier there is no operand type, and this now refuses (Violates) instead of returning the operand NODE as its own type. That fallback was the path by which the self-grounding fabrication entered branch/match/loop unification: two arms whose 'types' were their own expression nodes compared unequal and were reported as an arm-type mismatch, while two structurally identical arms compared equal and were reported as unified — in both cases the verdict was about node identity, not about types."
+
 fn infer_branch_operand_resolved_type_in_tree(
   node: Node,
   facts: InferredFacts,
   tree: Node,
-) -> Node {
-  if infer_branch_is_bool_literal_atom(node: node) {
-    bool_node()
-  } else if infer_branch_is_int_literal_atom(node: node) {
-    infer_branch_int_binding_type_node()
-  } else {
-    match infer_atom_binding_sym(node: node) {
-      Present { value: binding } =>
-        match infer_find_arrow_domain_type_in_tree(root: tree, binding: binding) {
-          Present { value: domain_ty } => domain_ty
-          Absent => inferred_facts_resolved_type(facts: facts)
-        }
-      Absent => inferred_facts_resolved_type(facts: facts)
-    }
+) -> Witness<Node> {
+  match dag_canonical_literal_from_node(node: node) {
+    Accepted { value: DagCanonicalBoolLiteral { value: _ }, diagnostics: _ } =>
+      Holds { value: bool_node() }
+    Accepted { value: DagCanonicalIntLiteral { magnitude: _ }, diagnostics: _ } =>
+      Holds { value: infer_branch_int_binding_type_node() }
+    Rejected { diagnostics: _ } =>
+      match infer_atom_binding_sym(node: node) {
+        Present { value: binding } =>
+          match infer_find_arrow_domain_type_in_tree(root: tree, binding: binding) {
+            Present { value: domain_ty } => Holds { value: domain_ty }
+            Absent => inferred_facts_resolved_type(facts: facts)
+          }
+        Absent => inferred_facts_resolved_type(facts: facts)
+      }
   }
 }
 
-fn infer_branch_operand_resolved_type(node: Node, facts: InferredFacts) -> Node {
+fn infer_branch_operand_resolved_type(node: Node, facts: InferredFacts) -> Witness<Node> {
   infer_branch_operand_resolved_type_in_tree(node: node, facts: facts, tree: node)
 }
 
-fn infer_branch_canonical_grounding(node: Node, unified_type: Node) -> CanonicalGrounding {
-  CanonicalGrounding {
-    node: node,
-    witness: CanonicalGroundingWitness {
-      structural: StructuralPropertyWitness {
-        property: ^constraint_property_being_canonical,
-        evidence: unified_type
-      },
-      closedness: StructuralPropertyWitness {
-        property: ^constraint_property_candidate_set_closedness,
-        evidence: node
-      }
+fn inferred_facts_from_derived_type(
+  node: Node,
+  derived_type: Node,
+  descent: Witness<v2.std.cardinality.TerminationProof>,
+) -> Outcome<InferredFacts> {
+  bind_outcome(
+    o: canonical_grounding_from_derived_type(node: node, derived_type: derived_type),
+    f: fn(grounding) {
+      inferred_facts_from_grounding(grounding: grounding, descent: descent)
     }
-  }
+  )
 }
 
 fn infer_branch_type_atoms_equal(a: Node, b: Node) -> Bool {
@@ -586,6 +657,13 @@ fn infer_branch_type_is_bool(type_node: Node) -> Bool {
   }
 }
 
+fn infer_branch_cond_type_is_bool(cond_target: Node, cond_facts: InferredFacts) -> Bool {
+  match infer_branch_operand_resolved_type(node: cond_target, facts: cond_facts) {
+    Holds { value: cond_type } => infer_branch_type_is_bool(type_node: cond_type)
+    Violates { diagnostic: _ } => false
+  }
+}
+
 fn infer_branch_type_is_int(type_node: Node) -> Bool {
   match type_node.kind {
     TypeNode { connective: Atom { identity: id } } => id == ^dag_binding_type_int
@@ -618,12 +696,18 @@ fn infer_match_bool_arm_body_type(
   body_target: Node,
   body_facts: InferredFacts,
   scrutinee_type: Node
-) -> Node {
-  if infer_branch_type_is_int(type_node: scrutinee_type)
-      && infer_branch_is_bool_literal_atom(node: body_target) {
-    infer_branch_int_binding_type_node()
-  } else {
-    infer_branch_operand_resolved_type(node: body_target, facts: body_facts)
+) -> Witness<Node> {
+  match dag_canonical_literal_from_node(node: body_target) {
+    Accepted { value: DagCanonicalBoolLiteral { value: _ }, diagnostics: _ } =>
+      if infer_branch_type_is_int(type_node: scrutinee_type) {
+        Holds { value: infer_branch_int_binding_type_node() }
+      } else {
+        infer_branch_operand_resolved_type(node: body_target, facts: body_facts)
+      }
+    Accepted { value: DagCanonicalIntLiteral { magnitude: _ }, diagnostics: _ } =>
+      infer_branch_operand_resolved_type(node: body_target, facts: body_facts)
+    Rejected { diagnostics: _ } =>
+      infer_branch_operand_resolved_type(node: body_target, facts: body_facts)
   }
 }
 
@@ -665,11 +749,9 @@ fn infer_match_bool_arm_rows_accept(
                     Rejected { diagnostics: diagnostics_singleton(d: d) }
                   Holds { value: descent_proof } =>
                     bind_outcome(
-                      o: inferred_facts_from_grounding(
-                        grounding: infer_branch_canonical_grounding(
-                          node: node,
-                          unified_type: first_body
-                        ),
+                      o: inferred_facts_from_derived_type(
+                        node: node,
+                        derived_type: first_body,
                         descent: Holds { value: descent_proof }
                       ),
                       f: fn(facts) {
@@ -701,12 +783,18 @@ fn infer_unify_branch_arm_types(
   else_node: Node,
   else_facts: InferredFacts,
 ) -> Outcome<Node> {
-  let then_type = infer_branch_operand_resolved_type(node: then_node, facts: then_facts)
-  let else_type = infer_branch_operand_resolved_type(node: else_node, facts: else_facts)
-  if infer_branch_type_atoms_equal(a: then_type, b: else_type) {
-    Accepted { value: then_type, diagnostics: None }
-  } else {
-    outcome_rejected(infer_branch_arm_type_mismatch_diagnostic(node: then_node))
+  match infer_branch_operand_resolved_type(node: then_node, facts: then_facts) {
+    Violates { diagnostic: d } => outcome_rejected(d)
+    Holds { value: then_type } =>
+      match infer_branch_operand_resolved_type(node: else_node, facts: else_facts) {
+        Violates { diagnostic: d } => outcome_rejected(d)
+        Holds { value: else_type } =>
+          if infer_branch_type_atoms_equal(a: then_type, b: else_type) {
+            Accepted { value: then_type, diagnostics: None }
+          } else {
+            outcome_rejected(infer_branch_arm_type_mismatch_diagnostic(node: then_node))
+          }
+      }
   }
 }
 
@@ -740,11 +828,9 @@ fn infer_branch_bool_if_else(
                             match infer_bounded_lattice_consumer_gate(consumer: node, partials: partials) {
                               Rejected { diagnostics: r } => Rejected { diagnostics: r }
                               Accepted { value: _, diagnostics: cd } =>
-                                if !infer_branch_type_is_bool(
-                                  type_node: infer_branch_operand_resolved_type(
-                                    node: cond_target,
-                                    facts: cond_facts
-                                  )
+                                if !infer_branch_cond_type_is_bool(
+                                  cond_target: cond_target,
+                                  cond_facts: cond_facts
                                 ) {
                                   outcome_rejected(infer_branch_cond_not_bool_diagnostic(node: node))
                                 } else {
@@ -761,11 +847,9 @@ fn infer_branch_bool_if_else(
                                           Rejected { diagnostics: diagnostics_singleton(d: d) }
                                         Holds { value: descent_proof } =>
                                           bind_outcome(
-                                            o: inferred_facts_from_grounding(
-                                              grounding: infer_branch_canonical_grounding(
-                                                node: node,
-                                                unified_type: unified_type
-                                              ),
+                                            o: inferred_facts_from_derived_type(
+                                              node: node,
+                                              derived_type: unified_type,
                                               descent: Holds { value: descent_proof }
                                             ),
                                             f: fn(facts) {
@@ -809,27 +893,15 @@ type InferMatchArmRow {
   body_type: Node
 }
 
-fn infer_branch_is_bool_true_literal_atom(node: Node) -> Bool {
-  match node.kind {
-    TypeNode { connective: Atom { identity: id } } => id == ^dag_token_kw_true
-    _ => false
-  }
-}
-
-fn infer_branch_is_bool_false_literal_atom(node: Node) -> Bool {
-  match node.kind {
-    TypeNode { connective: Atom { identity: id } } => id == ^dag_token_kw_false
-    _ => false
-  }
-}
-
 fn infer_bool_literal_pattern_classify(pattern: Node) -> InferBoolLiteralPattern {
-  if infer_branch_is_bool_true_literal_atom(node: pattern) {
-    InferBoolLiteralPatternTrue
-  } else if infer_branch_is_bool_false_literal_atom(node: pattern) {
-    InferBoolLiteralPatternFalse
-  } else {
-    InferBoolLiteralPatternOther
+  match dag_canonical_literal_from_node(node: pattern) {
+    Accepted { value: DagCanonicalBoolLiteral { value: true }, diagnostics: _ } =>
+      InferBoolLiteralPatternTrue
+    Accepted { value: DagCanonicalBoolLiteral { value: false }, diagnostics: _ } =>
+      InferBoolLiteralPatternFalse
+    Accepted { value: DagCanonicalIntLiteral { magnitude: _ }, diagnostics: _ } =>
+      InferBoolLiteralPatternOther
+    Rejected { diagnostics: _ } => InferBoolLiteralPatternOther
   }
 }
 
@@ -890,16 +962,20 @@ fn infer_match_bool_arm_row(
                   match lookup_inferred_facts_in_entries(entries: entries, key: body_target) {
                     Absent => outcome_rejected(infer_facts_lookup_miss_diagnostic(key: body_target))
                     Present { value: body_facts } =>
-                      Accepted {
-                        value: InferMatchArmRow {
-                          coverage: coverage,
-                          body_type: infer_match_bool_arm_body_type(
-                            body_target: body_target,
-                            body_facts: body_facts,
-                            scrutinee_type: scrutinee_type
-                          )
-                        },
-                        diagnostics: diagnostics_merge(outer: pd, inner: bd)
+                      match infer_match_bool_arm_body_type(
+                        body_target: body_target,
+                        body_facts: body_facts,
+                        scrutinee_type: scrutinee_type
+                      ) {
+                        Violates { diagnostic: d } => outcome_rejected(d)
+                        Holds { value: body_type } =>
+                          Accepted {
+                            value: InferMatchArmRow {
+                              coverage: coverage,
+                              body_type: body_type
+                            },
+                            diagnostics: diagnostics_merge(outer: pd, inner: bd)
+                          }
                       }
                   }
               }
@@ -934,28 +1010,31 @@ fn infer_match_bool(
                     match infer_bounded_lattice_consumer_gate(consumer: node, partials: partials) {
                       Rejected { diagnostics: r } => Rejected { diagnostics: r }
                       Accepted { value: _, diagnostics: cd } =>
-                        let scrutinee_type = infer_branch_operand_resolved_type_in_tree(
+                        match infer_branch_operand_resolved_type_in_tree(
                           node: scrutinee_target,
                           facts: scrutinee_facts,
                           tree: tree
-                        )
-                        if infer_branch_type_is_bool(type_node: scrutinee_type)
-                            || infer_branch_type_is_int(type_node: scrutinee_type) {
-                          infer_match_bool_arm_rows_accept(
-                            node: node,
-                            partials: partials,
-                            entries: entries,
-                            first_arm_target: first_arm_target,
-                            second_arm_target: second_arm_target,
-                            cd: infer_match_bool_consumer_diagnostics_with_int_scrutinee_scaffold(
-                              consumer: node,
-                              cd: cd,
-                              scrutinee_type: scrutinee_type
-                            ),
-                            scrutinee_type: scrutinee_type
-                          )
-                        } else {
-                          outcome_rejected(infer_match_scrutinee_not_bool_diagnostic(node: node))
+                        ) {
+                          Violates { diagnostic: d } => outcome_rejected(d)
+                          Holds { value: scrutinee_type } =>
+                            if infer_branch_type_is_bool(type_node: scrutinee_type)
+                                || infer_branch_type_is_int(type_node: scrutinee_type) {
+                              infer_match_bool_arm_rows_accept(
+                                node: node,
+                                partials: partials,
+                                entries: entries,
+                                first_arm_target: first_arm_target,
+                                second_arm_target: second_arm_target,
+                                cd: infer_match_bool_consumer_diagnostics_with_int_scrutinee_scaffold(
+                                  consumer: node,
+                                  cd: cd,
+                                  scrutinee_type: scrutinee_type
+                                ),
+                                scrutinee_type: scrutinee_type
+                              )
+                            } else {
+                              outcome_rejected(infer_match_scrutinee_not_bool_diagnostic(node: node))
+                            }
                         }
                     }
                 }
@@ -981,9 +1060,13 @@ fn infer_loop_body_type_at(target: Node, entries: List<InferredFactsEntry>) -> O
   match lookup_inferred_facts_in_entries(entries: entries, key: target) {
     Absent => outcome_rejected(infer_facts_lookup_miss_diagnostic(key: target))
     Present { value: facts } =>
-      Accepted {
-        value: infer_branch_operand_resolved_type(node: target, facts: facts),
-        diagnostics: None
+      match infer_branch_operand_resolved_type(node: target, facts: facts) {
+        Violates { diagnostic: d } => outcome_rejected(d)
+        Holds { value: body_type } =>
+          Accepted {
+            value: body_type,
+            diagnostics: None
+          }
       }
   }
 }
@@ -1039,11 +1122,9 @@ fn infer_loop_iteration(
               Rejected { diagnostics: diagnostics_singleton(d: d) }
             Holds { value: descent_proof } =>
               bind_outcome(
-                o: inferred_facts_from_grounding(
-                  grounding: infer_branch_canonical_grounding(
-                    node: node,
-                    unified_type: carrier
-                  ),
+                o: inferred_facts_from_derived_type(
+                  node: node,
+                  derived_type: carrier,
                   descent: Holds { value: descent_proof }
                 ),
                 f: fn(facts) {
@@ -1259,6 +1340,44 @@ fn infer_gather_loop_row_on_entries(
   }
 }
 
+data infer_gather_dispatch_totality_note: String = "This dispatch is TOTAL over the closed node vocabulary (6 connectives + 6 behaviors) with no wildcard arm, and that is the construction half of the wall. The wildcard it replaces is what let nine kinds fall silently into the self-grounding fabrication; enumerating them means a thirteenth kind cannot be added without deciding, at this site, whether it derives its type or joins the counted frontier — the decision cannot be defaulted into by omission (DESIGN §4 closed vocabulary, §5 unwritable-by-construction)."
+
+fn infer_gather_fold_not_derived(n: Node, partials: List<Node>) -> InferGatherFoldAcc {
+  match infer_node_facts(n: n, partials: partials) {
+    Rejected { diagnostics: r } =>
+      infer_gather_fold_acc_failed(
+        node: n,
+        pending: r,
+        await_branch_row: false,
+        await_match_row: false,
+        await_loop_row: false,
+        children_remaining: 0
+      )
+    Accepted { value: facts, diagnostics: d } =>
+      match admitted_inferred_facts_entry(node: n, facts: facts) {
+        Rejected { diagnostics: r } =>
+          infer_gather_fold_acc_failed(
+            node: n,
+            pending: r,
+            await_branch_row: false,
+            await_match_row: false,
+            await_loop_row: false,
+            children_remaining: 0
+          )
+        Accepted { value: entry, diagnostics: ed } =>
+          infer_gather_fold_acc_ok(
+            node: n,
+            entries: [entry],
+            pending: diagnostics_merge(outer: d, inner: ed),
+            await_branch_row: false,
+            await_match_row: false,
+            await_loop_row: false,
+            children_remaining: 0
+          )
+      }
+  }
+}
+
 fn infer_gather_fold_init(n: Node, partials: List<Node>) -> InferGatherFoldAcc {
   match n.kind {
     ComputationNode { behavior: Branch } =>
@@ -1291,40 +1410,15 @@ fn infer_gather_fold_init(n: Node, partials: List<Node>) -> InferGatherFoldAcc {
         await_loop_row: true,
         children_remaining: length(xs: n.children)
       )
-    _ =>
-      match infer_node_facts(n: n, partials: partials) {
-        Rejected { diagnostics: r } =>
-          infer_gather_fold_acc_failed(
-            node: n,
-            pending: r,
-            await_branch_row: false,
-            await_match_row: false,
-            await_loop_row: false,
-            children_remaining: 0
-          )
-        Accepted { value: facts, diagnostics: d } =>
-          match admitted_inferred_facts_entry(node: n, facts: facts) {
-            Rejected { diagnostics: r } =>
-              infer_gather_fold_acc_failed(
-                node: n,
-                pending: r,
-                await_branch_row: false,
-                await_match_row: false,
-                await_loop_row: false,
-                children_remaining: 0
-              )
-            Accepted { value: entry, diagnostics: ed } =>
-              infer_gather_fold_acc_ok(
-                node: n,
-                entries: [entry],
-                pending: diagnostics_merge(outer: d, inner: ed),
-                await_branch_row: false,
-                await_match_row: false,
-                await_loop_row: false,
-                children_remaining: 0
-              )
-          }
-      }
+    ComputationNode { behavior: Value } => infer_gather_fold_not_derived(n: n, partials: partials)
+    ComputationNode { behavior: Transform } => infer_gather_fold_not_derived(n: n, partials: partials)
+    ComputationNode { behavior: Bind } => infer_gather_fold_not_derived(n: n, partials: partials)
+    TypeNode { connective: Atom { identity: _ } } => infer_gather_fold_not_derived(n: n, partials: partials)
+    TypeNode { connective: Conj } => infer_gather_fold_not_derived(n: n, partials: partials)
+    TypeNode { connective: Disj } => infer_gather_fold_not_derived(n: n, partials: partials)
+    TypeNode { connective: Arrow } => infer_gather_fold_not_derived(n: n, partials: partials)
+    TypeNode { connective: Cardinality } => infer_gather_fold_not_derived(n: n, partials: partials)
+    TypeNode { connective: Instantiation } => infer_gather_fold_not_derived(n: n, partials: partials)
   }
 }
 
@@ -1338,6 +1432,20 @@ fn infer_gather_failed_non_empty(acc: InferGatherFoldAcc) -> NonEmptyDiagnostics
   }
 }
 
+data infer_literal_subtree_diagnostic_discharge_note: String = "An integer literal's modeled type derives from its canonical representation, including its sole named magnitude subtree. Its derivation discharges only that edge's local type frontier; propagating it past the literal would report GroundingNotDerived after Int was derived. Boolean literals are canonical only with no children, so no boolean payload can be discharged. Malformed literals remain GroundingNotDerived and retain every child diagnostic."
+
+fn infer_literal_edge_diagnostics_derived(parent: Node, edge: Edge) -> Bool {
+  match dag_canonical_literal_from_node(node: parent) {
+    Accepted { value: DagCanonicalIntLiteral { magnitude: _ }, diagnostics: _ } =>
+      match edge.label {
+        Named { name: field } => field == ^integer_literal_magnitude_field
+        Positional => false
+      }
+    Accepted { value: DagCanonicalBoolLiteral { value: _ }, diagnostics: _ } => false
+    Rejected { diagnostics: _ } => false
+  }
+}
+
 fn infer_gather_fold_step(
   acc: InferGatherFoldAcc,
   edge: Edge,
@@ -1361,7 +1469,11 @@ fn infer_gather_fold_step(
     )
   } else {
     let merged_entries = concat_inferred_facts_entries(a: acc.entries, b: child.entries)
-    let merged_pending = diagnostics_merge(outer: acc.pending, inner: child.pending)
+    let merged_pending = if infer_literal_edge_diagnostics_derived(parent: acc.node, edge: edge) {
+      acc.pending
+    } else {
+      diagnostics_merge(outer: acc.pending, inner: child.pending)
+    }
     let children_remaining = acc.children_remaining - 1
     if acc.await_branch_row && children_remaining == 0 {
       infer_gather_branch_row_on_entries(
diff --git a/src/v2/compiler/05_eval.dag b/src/v2/compiler/05_eval.dag
index 0f0fdc04c21..480b00f2128 100644
--- a/src/v2/compiler/05_eval.dag
+++ b/src/v2/compiler/05_eval.dag
@@ -1,11 +1,15 @@
 module v2.compiler.eval
 
 import v2.compiler.infer {
+  DerivedGrounding,
+  GroundingNotDerived,
   InferredFacts,
   InferredTree,
-  canonical_grounding_admits_infer_facts,
   infer_facts_lookup_miss_diagnostic,
+  inferred_facts_canonical_admitted,
+  inferred_facts_cover_node,
   inferred_facts_descent,
+  inferred_facts_grounding_derived,
   inferred_facts_resolved_type
 }
 import std.algebra { Cons, Empty }
@@ -780,18 +784,36 @@ fn descent_witness_digest(d: Witness<v2.std.cardinality.TerminationProof>) -> Ha
   }
 }
 
+fn eval_grounding_not_derived_digest_node() -> Node {
+  Node {
+    kind: TypeNode { connective: Atom { identity: ^eval_grounding_not_derived_digest_tag } },
+    children: [],
+    occurrence_id: SyntheticOccurrence
+  }
+}
+
 fn inferred_facts_digest(facts: InferredFacts) -> Hash {
-  let g = facts.grounding
-  combine_hash(
-    a: content_hash(n: g.node),
-    b: combine_hash(
-      a: combine_hash(
-        a: structural_property_witness_digest(w: g.witness.structural),
-        b: structural_property_witness_digest(w: g.witness.closedness)
-      ),
-      b: descent_witness_digest(d: inferred_facts_descent(facts: facts))
-    )
-  )
+  match facts.grounding {
+    DerivedGrounding { grounding: g } =>
+      combine_hash(
+        a: content_hash(n: g.node),
+        b: combine_hash(
+          a: combine_hash(
+            a: structural_property_witness_digest(w: g.witness.structural),
+            b: structural_property_witness_digest(w: g.witness.closedness)
+          ),
+          b: descent_witness_digest(d: inferred_facts_descent(facts: facts))
+        )
+      )
+    GroundingNotDerived { node: n } =>
+      combine_hash(
+        a: combine_hash(
+          a: content_hash(n: eval_grounding_not_derived_digest_node()),
+          b: content_hash(n: n)
+        ),
+        b: descent_witness_digest(d: inferred_facts_descent(facts: facts))
+      )
+  }
 }
 
 fn inferred_node_facts_cache_digest(tree: InferredTree, node: Node) -> Hash {
@@ -979,13 +1001,19 @@ fn inferred_facts_witness_for_eval(tree: InferredTree, node: Node) -> Witness<In
 fn inferred_facts_for_eval(tree: InferredTree, node: Node) -> Outcome<InferredFacts> {
   match inferred_facts_witness_for_eval(tree: tree, node: node) {
     Holds { value: facts } =>
-      if facts.grounding.node != node {
+      if !inferred_facts_grounding_derived(facts: facts) {
+        Rejected {
+          diagnostics: diagnostics_singleton(
+            d: eval_diagnostic(reason: ^eval_rejected_grounding_not_derived, node: node)
+          )
+        }
+      } else if !inferred_facts_cover_node(facts: facts, node: node) {
         Rejected {
           diagnostics: diagnostics_singleton(
             d: eval_diagnostic(reason: ^eval_rejected_grounding_node_mismatch, node: node)
           )
         }
-      } else if !canonical_grounding_admits_infer_facts(grounding: facts.grounding) {
+      } else if !inferred_facts_canonical_admitted(facts: facts) {
         Rejected {
           diagnostics: diagnostics_singleton(
             d: eval_diagnostic(reason: ^eval_rejected_canonical_mismatch, node: node)
@@ -1052,21 +1080,28 @@ fn eval_runtime_value_acceptance_witness(
   value: RuntimeValue
 ) -> RuntimeValueAcceptanceWitness {
   RuntimeValueAcceptanceWitness {
-    resolved_type: if inferred_facts_resolved_type(facts: facts) == runtime_value_resolved_type(value: value) {
-      Holds { value: runtime_value_resolved_type(value: value) }
-    } else {
-      Violates {
-        diagnostic: eval_diagnostic(reason: ^eval_rejected_resolved_type_mismatch, node: node)
-      }
+    resolved_type: match inferred_facts_resolved_type(facts: facts) {
+      Violates { diagnostic: _ } =>
+        Violates {
+          diagnostic: eval_diagnostic(reason: ^eval_rejected_grounding_not_derived, node: node)
+        }
+      Holds { value: declared } =>
+        if declared == runtime_value_resolved_type(value: value) {
+          Holds { value: runtime_value_resolved_type(value: value) }
+        } else {
+          Violates {
+            diagnostic: eval_diagnostic(reason: ^eval_rejected_resolved_type_mismatch, node: node)
+          }
+        }
     },
-    inhabitance: if canonical_grounding_admits_infer_facts(grounding: facts.grounding) {
+    inhabitance: if inferred_facts_canonical_admitted(facts: facts) {
       Holds { value: facts }
     } else {
       Violates {
         diagnostic: eval_diagnostic(reason: ^eval_rejected_inhabitance_mismatch, node: node)
       }
     },
-    canonical: if canonical_grounding_admits_infer_facts(grounding: facts.grounding) {
+    canonical: if inferred_facts_canonical_admitted(facts: facts) {
       Holds { value: facts }
     } else {
       Violates {
diff --git a/src/v2/compiler/06_translate.dag b/src/v2/compiler/06_translate.dag
index 5db05ee4fdf..1a3f8e54b5e 100644
--- a/src/v2/compiler/06_translate.dag
+++ b/src/v2/compiler/06_translate.dag
@@ -38,6 +38,7 @@ import v2.std.coercion {
   CoercionCandidateSet,
   CoercionResult,
   coercion_candidate_set_from_declared_inhabitants,
+  coercion_identity_from_target_model,
   coercion_fold_with_declared_priority
 }
 import v2.std.diagnostic {
@@ -1245,28 +1246,31 @@ fn coerce_grounded_node(
   tree: InferredTree,
   target: TargetModel
 ) -> Outcome<CoercionResult> {
-  bind_outcome(
-    o: canonical_grounding_for_node(tree: tree, node: source),
-    f: fn(grounding) {
+  match coercion_identity_from_target_model(source: source, target: target) {
+    Accepted { value: identity, diagnostics: d } =>
+      Accepted { value: identity, diagnostics: d }
+    Rejected { diagnostics: _ } =>
       bind_outcome(
         o: target_selection_priority_from_model(target: target),
         f: fn(priority) {
           bind_outcome(
-            o: coercion_candidates_from_target_model(
-              target: target
-            ),
+            o: coercion_candidates_from_target_model(target: target),
             f: fn(candidates) {
-              coercion_fold_with_declared_priority(
-                source: grounding,
-                candidates: candidates,
-                priority: priority
+              bind_outcome(
+                o: canonical_grounding_for_node(tree: tree, node: source),
+                f: fn(grounding) {
+                  coercion_fold_with_declared_priority(
+                    source: grounding,
+                    candidates: candidates,
+                    priority: priority
+                  )
+                }
               )
             }
           )
         }
       )
-    }
-  )
+  }
 }
 fn translate_type_expression_shape_missing_diagnostic(node: Node) -> Diagnostic {
   Diagnostic {
diff --git a/src/v2/compiler/program_partition.dag b/src/v2/compiler/program_partition.dag
index 0aeaea7062e..772aca8aa42 100644
--- a/src/v2/compiler/program_partition.dag
+++ b/src/v2/compiler/program_partition.dag
@@ -6,7 +6,8 @@ import v2.compiler.infer {
   InferredFactsEntry,
   InferredTree,
   admitted_inferred_facts_entry,
-  facts_map_from_entries
+  facts_map_from_entries,
+  inferred_facts_subject_node
 }
 import extdeps.communication.medium { Medium }
 import v2.compiler.translate {
@@ -389,7 +390,7 @@ fn partition_grounding_subject_in_segment(
 ) -> Bool {
   node_in_subtree_by_identity(
     root: segment_root,
-    needle: facts.grounding.node
+    needle: inferred_facts_subject_node(facts: facts)
   )
 }
 
diff --git a/src/v2/extdeps/languages/dag.dag b/src/v2/extdeps/languages/dag.dag
index 587e0339753..525ffbfcb5a 100644
--- a/src/v2/extdeps/languages/dag.dag
+++ b/src/v2/extdeps/languages/dag.dag
@@ -144,7 +144,7 @@ import v2.std.compilers.target_model {
   derive_bodied_arrow_scaffold}
 import v2.std.logic { Bool }
 import std.algebra { Cons, Empty }
-import v2.std.algebra { fold_list, for_all, is_empty, list_append, list_snoc_item }
+import v2.std.algebra { fold_list, for_all, is_empty, length, list_append, list_snoc_item }
 import v2.std.diagnostic {
   Accepted,
   Diagnostic,
@@ -4190,6 +4190,40 @@ fn dag_int_literal_magnitude_int_from_node(node: Node) -> Outcome<Int> {
   }
 }
 
+type DagCanonicalLiteral
+  = DagCanonicalBoolLiteral { value: Bool }
+  | DagCanonicalIntLiteral { magnitude: Int }
+
+fn dag_canonical_literal_shape_diagnostic(node: Node) -> Diagnostic {
+  Diagnostic {
+    reason: ^dag_literal_shape_invalid,
+    at: node_locus(node: node),
+    correction: None
+  }
+}
+
+data dag_canonical_literal_query_note: String = "dag_canonical_literal_from_node is the single typed query for inference-facing DAG literal shape. It preserves the Bool-vs-Int distinction and the decoded integer magnitude in a coproduct instead of publishing sibling is_* predicates over Node storage. Bool literals admit exactly the childless true/false atoms. Int literals admit exactly one named, decodable magnitude child. Every other shape is a typed refusal."
+
+fn dag_canonical_literal_from_node(node: Node) -> Outcome<DagCanonicalLiteral> {
+  if dag_node_is_kw_true_atom(node: node) && (length(xs: node.children) == 0) {
+    outcome_accepted(value: DagCanonicalBoolLiteral { value: true })
+  } else if dag_node_is_kw_false_atom(node: node) && (length(xs: node.children) == 0) {
+    outcome_accepted(value: DagCanonicalBoolLiteral { value: false })
+  } else if dag_node_is_int_literal_atom(node: node) && (length(xs: node.children) == 1) {
+    match dag_int_literal_magnitude_int_from_node(node: node) {
+      Accepted { value: magnitude, diagnostics: d } =>
+        Accepted {
+          value: DagCanonicalIntLiteral { magnitude: magnitude },
+          diagnostics: d
+        }
+      Rejected { diagnostics: _ } =>
+        outcome_rejected(dag_canonical_literal_shape_diagnostic(node: node))
+    }
+  } else {
+    outcome_rejected(dag_canonical_literal_shape_diagnostic(node: node))
+  }
+}
+
 fn dag_type_atom_node(identity: Symbol) -> Node {
   Node {
     kind: TypeNode { connective: Atom { identity: identity } },
diff --git a/src/v2/lens/common/infer_fixture.dag b/src/v2/lens/common/infer_fixture.dag
index 9113126fb15..f27eecf4fb7 100644
--- a/src/v2/lens/common/infer_fixture.dag
+++ b/src/v2/lens/common/infer_fixture.dag
@@ -1,6 +1,6 @@
 module v2.test.lens_common.infer_fixture
 
-import v2.compiler.infer { InferredFacts, InferredTree, infer_facts_lookup_miss_diagnostic }
+import v2.compiler.infer { DerivedGrounding, InferredFacts, InferredTree, infer_facts_lookup_miss_diagnostic }
 import v2.std.cardinality { RankingDimension, TerminationProof }
 import v2.std.collection { Map }
 import v2.std.constraints {
@@ -45,7 +45,7 @@ fn claim_inferred_facts_witness(
   descent: Witness<v2.std.cardinality.TerminationProof>
 ) -> InferredFacts {
   InferredFacts {
-    grounding: grounding,
+    grounding: DerivedGrounding { grounding: grounding },
     descent: descent
   }
 }
diff --git a/src/v2/lens/parallelism.dag b/src/v2/lens/parallelism.dag
index 3d8d3ba8dca..4431cab2d4c 100644
--- a/src/v2/lens/parallelism.dag
+++ b/src/v2/lens/parallelism.dag
@@ -13,7 +13,7 @@ import v2.lens.common.algebraic_composition {
 }
 import std.disposition { SingleAuthority }
 
-import v2.compiler.infer { InferredFacts, InferredTree, inferred_facts_descent, infer_facts_lookup_miss_diagnostic }
+import v2.compiler.infer { InferredFacts, InferredTree, inferred_facts_descent, inferred_facts_subject_node, infer_facts_lookup_miss_diagnostic }
 import v2.std.algebra { bag_eq, list_snoc_item }
 import v2.std.collection {
   List,
@@ -76,7 +76,7 @@ fn parallelism_facts_for_source(tree: InferredTree, view: DependencyView) -> Wit
 fn parallelism_coupling_absent_diagnostic(facts: InferredFacts) -> Diagnostic {
   Diagnostic {
     reason: ^parallelism_reason_coupling_carrier_absent,
-    at: node_locus(node: facts.grounding.node),
+    at: node_locus(node: inferred_facts_subject_node(facts: facts)),
     correction: Unavailable { reason: AmbiguousIntent }
   }
 }
diff --git a/src/v2/std/coercion.dag b/src/v2/std/coercion.dag
index fbe6928439c..b04ef10d258 100644
--- a/src/v2/std/coercion.dag
+++ b/src/v2/std/coercion.dag
@@ -6,6 +6,7 @@ import v2.std.collection { List }
 import v2.std.constraints { CanonicalGrounding, CanonicalGroundingWitness }
 import v2.std.diagnostic {
   Accepted,
+  bind_outcome,
   Diagnostic,
   ExternalContractUnknown,
   None,
@@ -18,6 +19,11 @@ import v2.std.diagnostic {
   Unavailable,
   outcome_rejected
 }
+import v2.std.compilers.target_model {
+  TargetModel,
+  target_model_declared_inhabitants,
+  target_model_selection_priority
+}
 import v2.std.find_witness {
   CandidateSet,
   FindWitnessResult,
@@ -125,6 +131,79 @@ fn coercion_candidate_set_from_declared_inhabitants(
     )
   }
 }
+data identity_coercion_grounding_ruling: String = "Identity admission and semantic coercion are distinct judgments. coercion_identity_from_target_model accepts the TargetModel itself — never a caller-supplied CoercionCandidateSet — and reads its unique target_model_edge_declared_inhabitants and target_model_edge_selection_policy children inside this authority. Exact selection from that authored roster grounds CoercionQuality.Identity without claiming a resolved type for source. A candidate roster derived from source cannot enter this API; generic candidate sets remain available only to the semantic coercion path whose source is a compiler-derived CanonicalGrounding. This is the API-level wall between target-model membership and self-certification."
+
+fn coercion_homomorphism_evidence_for_node(
+  source: Node,
+  fw: FindWitnessResult,
+) -> Node {
+  Node {
+    kind: TypeNode { connective: Conj },
+    children: [
+      Edge { label: Named { name: ^coercion_homomorphism_evidence_source }, target: source },
+      Edge { label: Named { name: ^coercion_homomorphism_evidence_candidate }, target: fw.candidate },
+      Edge {
+        label: Named { name: ^coercion_homomorphism_evidence_find_witness },
+        target: fw.witness.evidence
+      }
+    ],
+    occurrence_id: SyntheticOccurrence
+  }
+}
+
+fn coercion_identity_from_target_model(
+  source: Node,
+  target: TargetModel,
+) -> Outcome<CoercionResult> {
+  bind_outcome(
+    o: target_model_declared_inhabitants(target: target),
+    f: fn(inhabitants_root) {
+      bind_outcome(
+        o: target_model_selection_priority(target: target),
+        f: fn(priority) {
+          bind_outcome(
+            o: coercion_candidate_set_from_declared_inhabitants(
+              inhabitants_root: inhabitants_root,
+              closedness_property: ^target_model_edge_declared_inhabitants
+            ),
+            f: fn(candidates) {
+              match find_witness(
+                source_facts: source,
+                candidates: candidates.set,
+                predicate: PreservationPredicate {
+                  algebra: source,
+                  preservation_rule: ^preservation_rule_exact_structural_equality_zip_fold
+                },
+                multiplicity_policy: TargetSelection {
+                  policy: TargetDeclaredPriority { priority: priority }
+                }
+              ) {
+                Accepted { value: fw, diagnostics: fw_d } =>
+                  Accepted {
+                    value: CoercionResult {
+                      target: fw.candidate,
+                      quality: Identity,
+                      witness: CoercionWitness {
+                        homomorphism: HomomorphismWitness {
+                          rule: ^homomorphism_rule_exact_structural_equality,
+                          evidence: coercion_homomorphism_evidence_for_node(
+                            source: source,
+                            fw: fw
+                          )
+                        }
+                      }
+                    },
+                    diagnostics: fw_d
+                  }
+                Rejected { diagnostics: r } => Rejected { diagnostics: r }
+              }
+            }
+          )
+        }
+      )
+    }
+  )
+}
 fn coercion_quality_for_witness(
   source: CanonicalGrounding,
   fw: FindWitnessResult,
@@ -224,15 +303,7 @@ fn coercion_homomorphism_evidence(
   source: CanonicalGrounding,
   fw: FindWitnessResult,
 ) -> Node {
-  Node {
-    kind: TypeNode { connective: Conj },
-    children: [
-      Edge { label: Named { name: ^coercion_homomorphism_evidence_source }, target: source.node },
-      Edge { label: Named { name: ^coercion_homomorphism_evidence_candidate }, target: fw.candidate },
-      Edge { label: Named { name: ^coercion_homomorphism_evidence_find_witness }, target: fw.witness.evidence }
-    ],
-    occurrence_id: SyntheticOccurrence
-}
+  coercion_homomorphism_evidence_for_node(source: source.node, fw: fw)
 }
 fn coercion_fold_exact_structural(
   source: CanonicalGrounding,
diff --git a/src/v2/std/compilers/target_model.dag b/src/v2/std/compilers/target_model.dag
index 4f205b9cd2c..dabad52b7cd 100644
--- a/src/v2/std/compilers/target_model.dag
+++ b/src/v2/std/compilers/target_model.dag
@@ -129,6 +129,20 @@ type TargetModel {
   runtime_row: TargetEmitHostRuntimeRow
 }
 
+fn target_model_declared_inhabitants(target: TargetModel) -> Outcome<Node> {
+  projection_bundle_child(
+    bundle: target.bundle,
+    name: ^target_model_edge_declared_inhabitants
+  )
+}
+
+fn target_model_selection_priority(target: TargetModel) -> Outcome<Node> {
+  projection_bundle_child(
+    bundle: target.bundle,
+    name: ^target_model_edge_selection_policy
+  )
+}
+
 data target_model_emit_transforms_empty: Map<Symbol, fn(String) -> String> = empty_map()
 
 fn target_model_make_with_emit_transforms(
@@ -11698,7 +11712,7 @@ fn target_transform_surface_op_atom(node: Node) -> Outcome<Symbol> {
 }
 
 fn target_value_expr_declared_inhabitants_from_target(target: TargetModel) -> Outcome<Node> {
-  projection_bundle_child(bundle: target.bundle, name: ^target_model_edge_declared_inhabitants)
+  target_model_declared_inhabitants(target: target)
 }
 
 fn target_value_expr_add_signature_matches_for_target(
diff --git a/src/v2/std/constraints.dag b/src/v2/std/constraints.dag
index 8d4cc1a6c73..41dcc1451e0 100644
--- a/src/v2/std/constraints.dag
+++ b/src/v2/std/constraints.dag
@@ -62,6 +62,42 @@ fn constraints_ill_formed_root_diagnostic(graph: ConstraintGraph) -> Diagnostic
   }
 }
 
+data canonical_grounding_construction_authority_note: String = "v2.std.constraints.canonical_grounding_from_derived_type is the SINGLE construction authority for CanonicalGrounding: a grounding's structural evidence IS the node's resolved type (v2.compiler.infer.inferred_facts_resolved_type reads exactly this field), so a grounding whose evidence is the source node states 'this expression's type is itself' — source identity standing where a derivation belongs. That state is refused here rather than checked downstream (DESIGN §5 construction, not validation), which is why the refusal lives on the constructor and not in a lens. The derivations that legitimately inhabit it pass a type derived from the node's children (v2.compiler.infer's branch/match/loop derivations pass the unified arm type, the match body type, and the loop carrier type respectively, all via inferred_facts_from_derived_type; the claim fixtures in v2.lens.common.infer_fixture pass the declared i64/bool type node)."
+
+fn grounding_evidence_is_source_diagnostic(node: Node) -> Diagnostic {
+  Diagnostic {
+    reason: ^grounding_evidence_is_source,
+    at: node_locus(node: node),
+    correction: Unavailable { reason: ExternalContractUnknown }
+  }
+}
+
+fn canonical_grounding_from_derived_type(
+  node: Node,
+  derived_type: Node,
+) -> Outcome<CanonicalGrounding> {
+  if derived_type == node {
+    outcome_rejected(grounding_evidence_is_source_diagnostic(node: node))
+  } else {
+    Accepted {
+      value: CanonicalGrounding {
+        node: node,
+        witness: CanonicalGroundingWitness {
+          structural: StructuralPropertyWitness {
+            property: ^constraint_property_being_canonical,
+            evidence: derived_type
+          },
+          closedness: StructuralPropertyWitness {
+            property: ^constraint_property_candidate_set_closedness,
+            evidence: node
+          }
+        }
+      },
+      diagnostics: None
+    }
+  }
+}
+
 fn constraint_satisfaction_holds(
   source_facts: Node,
   candidate: Node,
diff --git a/src/v2/test/claim/compiler/compile_eval_thesis_proof_test.dag b/src/v2/test/claim/compiler/compile_eval_thesis_proof_test.dag
index 1b64d4903de..c76f5af0d2c 100644
--- a/src/v2/test/claim/compiler/compile_eval_thesis_proof_test.dag
+++ b/src/v2/test/claim/compiler/compile_eval_thesis_proof_test.dag
@@ -93,14 +93,15 @@ test fn compile_eval_bool_reaches_node_value_holds() -> Bool {
   }
 }
 
-test fn compile_eval_bool_via_compile_entry_holds() -> Bool {
+data compile_entry_refuses_underived_note: String = "BEHAVIOUR CHANGE, recorded rather than papered over. This witness previously asserted that the compile entry — which runs the REAL infer rather than the hand-built fixture tree the other witnesses supply — reached a node value. It passed only because infer fabricated the atom's grounding with the atom itself as its structural evidence, i.e. as its resolved type; eval's resolved_type check then compared v2_eval_bool_literal_pin against v2_eval_bool_literal_pin (the runtime value's primitive_type is that same node) and matched. The equality held because both sides were the same node, not because a type was derived. v2 has no derivation rule for the Atom type-node kind, so the honest outcome is the typed, located refusal this now asserts. The thesis that compile -> eval reaches a node value is UNCHANGED and still proven by compile_eval_bool_reaches_node_value_holds / isolate_t1, which supply the facts via compile_inferred; what is no longer claimed is that v2 can infer those facts itself. dissolve-on: a derivation rule for literal atoms lands, at which point this flips back to asserting the value and the fixture path stops being the only green one."
+
+test fn compile_eval_bool_via_compile_entry_refuses_underived_holds() -> Bool {
   match compile(
     source: v2_eval_bool_literal_pin,
     mode: Eval { runtime: v2_eval_bool_literal_pin }
   ) {
-    Accepted { value: EvalResult { value: actual }, diagnostics: _ } =>
-      compile_eval_thesis_medium_matches_expected(medium: actual)
-    Rejected { diagnostics: _ } => false
+    Rejected { diagnostics: d } => d.head.reason == ^infer_grounding_not_derived
+    Accepted { value: _, diagnostics: _ } => false
   }
 }
 
@@ -120,7 +121,7 @@ test fn isolate_t1_holds() -> Bool {
 }
 
 test fn isolate_t2_holds() -> Bool {
-  compile_eval_bool_via_compile_entry_holds()
+  compile_eval_bool_via_compile_entry_refuses_underived_holds()
 }
 
 test fn isolate_t3_holds() -> Bool {
diff --git a/src/v2/test/claim/infer_self_grounding_wall_test.dag b/src/v2/test/claim/infer_self_grounding_wall_test.dag
new file mode 100644
index 00000000000..0e2c75f0d32
--- /dev/null
+++ b/src/v2/test/claim/infer_self_grounding_wall_test.dag
@@ -0,0 +1,196 @@
+module v2.test.claim.infer_self_grounding_wall
+
+data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly
+
+data wall_subject_note: String = "Discriminating witnesses for the v2 self-grounding wall. The defect these pin was measured by execution on main at a589c5f0179: v2's infer routed nine of the closed vocabulary's twelve node kinds through solve_constraints with the singleton candidate set [root] under a predicate reducing to root == root, and stamped the result canonical. Because a grounding's structural evidence IS the node's resolved type, every such node was typed as ITSELF. Two arms are asserted in both directions: the construction authority refuses self-evidence (and still accepts a real derived type), and canonical_grounding_for_node — the reader 06_translate's coerce_grounded_node funnels through — now refuses the Conj/Disj groundings it previously handed back with evidence == source."
+
+fn wall_atom(s: Symbol) -> Node {
+  Node {
+    kind: TypeNode { connective: Atom { identity: s } },
+    children: [],
+    occurrence_id: SyntheticOccurrence
+  }
+}
+
+fn wall_conj_node() -> Node {
+  Node {
+    kind: TypeNode { connective: Conj },
+    children: [],
+    occurrence_id: SyntheticOccurrence
+  }
+}
+
+fn wall_disj_node() -> Node {
+  Node {
+    kind: TypeNode { connective: Disj },
+    children: [],
+    occurrence_id: SyntheticOccurrence
+  }
+}
+
+fn wall_value_node() -> Node {
+  Node {
+    kind: ComputationNode { behavior: Value },
+    children: [],
+    occurrence_id: SyntheticOccurrence
+  }
+}
+
+fn wall_malformed_bool_with_payload() -> Node {
+  Node {
+    kind: TypeNode { connective: Atom { identity: ^dag_token_kw_true } },
+    children: [
+      Edge {
+        label: Named { name: ^wall_malformed_bool_payload_field },
+        target: wall_value_node()
+      }
+    ],
+    occurrence_id: SyntheticOccurrence
+  }
+}
+
+fn wall_malformed_int_with_extra_payload() -> Node {
+  let literal = dag_int_literal_fixture_one()
+  Node {
+    kind: literal.kind,
+    children: list_snoc_item(
+      xs: literal.children,
+      item: Edge {
+        label: Named { name: ^wall_malformed_int_payload_field },
+        target: wall_value_node()
+      }
+    ),
+    occurrence_id: literal.occurrence_id
+  }
+}
+
+fn wall_derived_type_node() -> Node {
+  wall_atom(s: ^wall_derived_type_marker)
+}
+
+fn wall_self_grounding(node: Node) -> CanonicalGrounding {
+  CanonicalGrounding {
+    node: node,
+    witness: CanonicalGroundingWitness {
+      structural: StructuralPropertyWitness {
+        property: ^constraint_property_being_canonical,
+        evidence: node
+      },
+      closedness: StructuralPropertyWitness {
+        property: ^constraint_property_candidate_set_closedness,
+        evidence: node
+      }
+    }
+  }
+}
+
+fn wall_derived_grounding(node: Node) -> CanonicalGrounding {
+  CanonicalGrounding {
+    node: node,
+    witness: CanonicalGroundingWitness {
+      structural: StructuralPropertyWitness {
+        property: ^constraint_property_being_canonical,
+        evidence: wall_derived_type_node()
+      },
+      closedness: StructuralPropertyWitness {
+        property: ^constraint_property_candidate_set_closedness,
+        evidence: node
+      }
+    }
+  }
+}
+
+fn wall_grounding_for_node_refused(root: Node) -> Bool {
+  match infer(tree: root) {
+    Rejected { diagnostics: _ } => false
+    Accepted { value: tree, diagnostics: _ } =>
+      match canonical_grounding_for_node(tree: tree, node: root) {
+        Rejected { diagnostics: r } => r.head.reason == ^infer_grounding_not_derived
+        Accepted { value: _, diagnostics: _ } => false
+      }
+  }
+}
+
+fn wall_resolved_type_refused(root: Node) -> Bool {
+  match infer(tree: root) {
+    Rejected { diagnostics: _ } => false
+    Accepted { value: tree, diagnostics: _ } =>
+      match inferred_facts_witness_for_node(tree: tree, node: root) {
+        Violates { diagnostic: _ } => false
+        Holds { value: facts } =>
+          match inferred_facts_resolved_type(facts: facts) {
+            Violates { diagnostic: d } => d.reason == ^infer_grounding_not_derived
+            Holds { value: _ } => false
+          }
+      }
+  }
+}
+
+fn wall_infer_counts_frontier(root: Node) -> Bool {
+  match infer(tree: root) {
+    Rejected { diagnostics: _ } => false
+    Accepted { value: _, diagnostics: d } =>
+      match d {
+        Some { diagnostics: nds } => nds.head.reason == ^infer_grounding_not_derived
+        None => false
+      }
+  }
+}
+
+test fn wall_construction_authority_refuses_self_evidence() -> Bool {
+  match canonical_grounding_from_derived_type(
+    node: wall_conj_node(),
+    derived_type: wall_conj_node()
+  ) {
+    Rejected { diagnostics: r } => r.head.reason == ^grounding_evidence_is_source
+    Accepted { value: _, diagnostics: _ } => false
+  }
+}
+
+test fn wall_construction_authority_accepts_derived_type() -> Bool {
+  match canonical_grounding_from_derived_type(
+    node: wall_conj_node(),
+    derived_type: wall_derived_type_node()
+  ) {
+    Rejected { diagnostics: _ } => false
+    Accepted { value: g, diagnostics: _ } =>
+      (g.node == wall_conj_node())
+        && (g.witness.structural.evidence == wall_derived_type_node())
+  }
+}
+
+data wall_hand_built_residue_note: String = "The stated residue: a CanonicalGrounding written field-by-field, bypassing the construction authority, is still admitted. This is asserted rather than left implicit so the wall's edge is documented by a test and not by optimism — see canonical_grounding_admission_scope_note for why the 'evidence != node' read-path proxy was withdrawn (it false-positives on v2_evaluator's bool fixture, which uses one atom as both evaluand and primitive_type). Closing this residue needs CanonicalGrounding to stop being structurally constructible, not a wider predicate."
+
+test fn wall_hand_built_self_grounding_is_the_stated_residue() -> Bool {
+  canonical_grounding_admits_infer_facts(grounding: wall_self_grounding(node: wall_conj_node()))
+}
+
+test fn wall_admission_admits_hand_built_derived_grounding() -> Bool {
+  canonical_grounding_admits_infer_facts(grounding: wall_derived_grounding(node: wall_conj_node()))
+}
+
+test fn wall_conj_grounding_no_longer_returns_source_as_its_own_type() -> Bool {
+  wall_grounding_for_node_refused(root: wall_conj_node())
+}
+
+test fn wall_disj_grounding_no_longer_returns_source_as_its_own_type() -> Bool {
+  wall_grounding_for_node_refused(root: wall_disj_node())
+}
+
+test fn wall_frontier_node_has_no_resolved_type() -> Bool {
+  wall_resolved_type_refused(root: wall_value_node())
+}
+
+test fn wall_frontier_is_counted_on_the_accepted_path() -> Bool {
+  wall_infer_counts_frontier(root: wall_value_node())
+}
+
+test fn wall_malformed_bool_payload_is_not_grounded_or_discharged() -> Bool {
+  wall_grounding_for_node_refused(root: wall_malformed_bool_with_payload())
+    && wall_infer_counts_frontier(root: wall_malformed_bool_with_payload())
+}
+
+test fn wall_malformed_int_payload_is_not_grounded_or_discharged() -> Bool {
+  wall_grounding_for_node_refused(root: wall_malformed_int_with_extra_payload())
+    && wall_infer_counts_frontier(root: wall_malformed_int_with_extra_payload())
+}
diff --git a/src/v2/test/claim/loop_infer_iteration_test.dag b/src/v2/test/claim/loop_infer_iteration_test.dag
index 8ca01726510..ffcd18938e2 100644
--- a/src/v2/test/claim/loop_infer_iteration_test.dag
+++ b/src/v2/test/claim/loop_infer_iteration_test.dag
@@ -51,10 +51,14 @@ fn loop_infer_run(root: Node) -> Outcome<InferredTree> {
 fn loop_infer_loop_type_is_int(tree: InferredTree, body: Node) -> Bool {
   match inferred_facts_witness_for_node(tree: tree, node: body) {
     Holds { value: facts } =>
-      infer_branch_type_atoms_equal(
-        a: inferred_facts_resolved_type(facts: facts),
-        b: loop_infer_int_binding_type_node()
-      )
+      match inferred_facts_resolved_type(facts: facts) {
+        Holds { value: resolved } =>
+          infer_branch_type_atoms_equal(
+            a: resolved,
+            b: loop_infer_int_binding_type_node()
+          )
+        Violates { diagnostic: _ } => false
+      }
     Violates { diagnostic: _ } => false
   }
 }
diff --git a/src/v2/test/claim/manual/branch_infer_if_then_else_test.dag b/src/v2/test/claim/manual/branch_infer_if_then_else_test.dag
index b24733f4ab2..0e2f4cbc898 100644
--- a/src/v2/test/claim/manual/branch_infer_if_then_else_test.dag
+++ b/src/v2/test/claim/manual/branch_infer_if_then_else_test.dag
@@ -41,10 +41,11 @@ test fn branch_infer_bool_cond_accepts_holds() -> Bool {
   }
 }
 
-test fn branch_infer_arm_mismatch_red_holds() -> Bool {
+data branch_infer_underived_arm_ruling_note: String = "The else arm is the bare dag_token_ident token-class atom, not a literal with a modeled type. After the self-grounding wall it cannot participate in an arm-type comparison: inference must refuse infer_grounding_not_derived before claiming a mismatch. The discriminating mismatch RED remains covered by branch_infer_test using two genuinely derived operand types."
+
+test fn branch_infer_underived_arm_refuses_before_mismatch_holds() -> Bool {
   match infer(tree: branch_infer_arm_mismatch_body()) {
     Accepted { value: _, diagnostics: _ } => false
-    Rejected { diagnostics: d } => d.head.reason == ^infer_branch_arm_type_mismatch
+    Rejected { diagnostics: d } => d.head.reason == ^infer_grounding_not_derived
   }
 }
-
diff --git a/src/v2/test/claim/manual/branch_infer_test.dag b/src/v2/test/claim/manual/branch_infer_test.dag
index 8976a41a282..d053fe3d1a9 100644
--- a/src/v2/test/claim/manual/branch_infer_test.dag
+++ b/src/v2/test/claim/manual/branch_infer_test.dag
@@ -83,9 +83,11 @@ fn branch_infer_cond_child_is_bool(tree: InferredTree, body: Node) -> Bool {
   let cond = branch_infer_positional_target(body: body, index: 0)
   match inferred_facts_witness_for_node(tree: tree, node: cond) {
     Holds { value: facts } =>
-      infer_branch_type_is_bool(
-        type_node: infer_branch_operand_resolved_type(node: cond, facts: facts)
-      )
+      match infer_branch_operand_resolved_type(node: cond, facts: facts) {
+        Holds { value: cond_type } =>
+          infer_branch_type_is_bool(type_node: cond_type)
+        Violates { diagnostic: _ } => false
+      }
     Violates { diagnostic: _ } => false
   }
 }
@@ -93,10 +95,14 @@ fn branch_infer_cond_child_is_bool(tree: InferredTree, body: Node) -> Bool {
 fn branch_infer_branch_result_is_int(tree: InferredTree, body: Node) -> Bool {
   match inferred_facts_witness_for_node(tree: tree, node: body) {
     Holds { value: facts } =>
-      infer_branch_type_atoms_equal(
-        a: inferred_facts_resolved_type(facts: facts),
-        b: branch_infer_int_binding_type_node()
-      )
+      match inferred_facts_resolved_type(facts: facts) {
+        Holds { value: resolved } =>
+          infer_branch_type_atoms_equal(
+            a: resolved,
+            b: branch_infer_int_binding_type_node()
+          )
+        Violates { diagnostic: _ } => false
+      }
     Violates { diagnostic: _ } => false
   }
 }
diff --git a/src/v2/test/claim/manual/infer_algebra_ref_grounding_anchor.dag b/src/v2/test/claim/manual/infer_algebra_ref_grounding_anchor.dag
index c3c2ed06fb2..08e428a2164 100644
--- a/src/v2/test/claim/manual/infer_algebra_ref_grounding_anchor.dag
+++ b/src/v2/test/claim/manual/infer_algebra_ref_grounding_anchor.dag
@@ -32,16 +32,18 @@ data algebra_ref_computation_node_is_ungrounded: Bool = !algebra_ref_is_grounded
 
 fn anchor_inferred_facts_bare_atom_algebra() -> InferredFacts {
   InferredFacts {
-    grounding: CanonicalGrounding {
-      node: anchor_atom_node(s: ^anchor_resolved_type_sym),
-      witness: CanonicalGroundingWitness {
-        structural: StructuralPropertyWitness {
-          property: ^constraint_property_being_canonical,
-          evidence: anchor_atom_node(s: ^anchor_algebra_ungrounded_sym)
-        },
-        closedness: StructuralPropertyWitness {
-          property: ^constraint_property_candidate_set_closedness,
-          evidence: anchor_atom_node(s: ^anchor_resolved_type_sym)
+    grounding: DerivedGrounding {
+      grounding: CanonicalGrounding {
+        node: anchor_atom_node(s: ^anchor_resolved_type_sym),
+        witness: CanonicalGroundingWitness {
+          structural: StructuralPropertyWitness {
+            property: ^constraint_property_being_canonical,
+            evidence: anchor_atom_node(s: ^anchor_algebra_ungrounded_sym)
+          },
+          closedness: StructuralPropertyWitness {
+            property: ^constraint_property_candidate_set_closedness,
+            evidence: anchor_atom_node(s: ^anchor_resolved_type_sym)
+          }
         }
       }
     },
diff --git a/src/v2/test/claim/manual/ingest_bridge_test.dag b/src/v2/test/claim/manual/ingest_bridge_test.dag
index c74846beefb..f4fc6a213f2 100644
--- a/src/v2/test/claim/manual/ingest_bridge_test.dag
+++ b/src/v2/test/claim/manual/ingest_bridge_test.dag
@@ -8,6 +8,8 @@ import v2.compiler.ingest {
   parse_tree_to_emitted_node,
   parse_tree_to_target_model_bridge
 }
+import v2.compiler.infer { canonical_grounding_for_node, infer }
+import v2.compiler.translate { coerce_grounded_node }
 import v2.compiler.parse {
   grammar_validate_for_parse,
   parse_production,
@@ -37,6 +39,7 @@ import v2.std.compilers.lexing { Token }
 import v2.std.compilers.target_model {
   TargetModel, target_model_emit_transforms_empty
 }
+import v2.std.coercion { Identity }
 import v2.std.diagnostic { Accepted, None, Outcome, Rejected, port_locus }
 import v2.std.logic { Bool }
 import v2.std.node {
@@ -202,6 +205,50 @@ test fn ingest_bridge_to_canonical_holds() -> Bool {
   }
 }
 
+test fn ingest_identity_coercion_needs_roster_membership_not_derived_grounding() -> Bool {
+  let source = dag_fixture_emitted_add_fn
+  match infer(tree: source) {
+    Rejected { diagnostics: _ } => false
+    Accepted { value: inferred, diagnostics: _ } =>
+      match canonical_grounding_for_node(tree: inferred, node: source) {
+        Accepted { value: _, diagnostics: _ } => false
+        Rejected { diagnostics: grounding_r } =>
+          (grounding_r.head.reason == ^infer_grounding_not_derived)
+            && match coerce_grounded_node(
+              source: source,
+              tree: inferred,
+              target: ingest_fixture_model(
+                emitted: source,
+                spine_class: ^ingest_fixture_tok
+              )
+            ) {
+              Rejected { diagnostics: _ } => false
+              Accepted { value: coerced, diagnostics: _ } =>
+                (coerced.quality == Identity) && (coerced.target == source)
+            }
+      }
+  }
+}
+
+test fn ingest_identity_coercion_refuses_source_absent_from_authored_roster() -> Bool {
+  let source = ingest_unstamped_node()
+  match infer(tree: source) {
+    Rejected { diagnostics: _ } => false
+    Accepted { value: inferred, diagnostics: _ } =>
+      match coerce_grounded_node(
+        source: source,
+        tree: inferred,
+        target: ingest_fixture_model(
+          emitted: dag_fixture_emitted_add_fn,
+          spine_class: ^ingest_fixture_tok
+        )
+      ) {
+        Accepted { value: _, diagnostics: _ } => false
+        Rejected { diagnostics: d } => d.head.reason == ^infer_grounding_not_derived
+      }
+  }
+}
+
 test fn ingest_fails_closed_off_frontier_holds() -> Bool {
   match ingest_parse() {
     Accepted { value: tree, diagnostics: _ } =>
@@ -273,4 +320,3 @@ test fn ingest_bridge_realized() -> Bool {
     && ingest_cross_language_compile_holds()
 }
 
-