diff --git a/src/v2/test/claim/manual/body_lowering_match.dag b/src/v2/test/claim/manual/body_lowering_match.dag
index d8163545c6e..f16b34ed64f 100644
--- a/src/v2/test/claim/manual/body_lowering_match.dag
+++ b/src/v2/test/claim/manual/body_lowering_match.dag
@@ -26,7 +26,6 @@ import v2.std.node {
   Match,
   Node,
   TypeNode,
-  node_subtree_count,
   node_synthetic
 }
 import v2.std.verification {
@@ -113,25 +112,21 @@ fn body_lowering_match_lowers_to_match() -> Bool {
       match body_lowering_find_match_expr(root: tree) {
         Absent => false
         Present { value: shell } =>
-          match body_lower_unwrap_captured(remaining: node_subtree_count(n: shell), shell: shell) {
-            Rejected { diagnostics: _ } => false
-            Accepted { value: captured_opt, diagnostics: _ } =>
-              match captured_opt {
-                Present { value: captured } =>
-                  match body_lower_try_match_from_captured(remaining: node_subtree_count(n: captured), captured: captured) {
-                    Rejected { diagnostics: _ } => false
-                    Accepted { value: lowered_opt, diagnostics: _ } =>
-                      match lowered_opt {
-                        Present { value: lowered } =>
-                          match lowered.kind {
-                            ComputationNode { behavior: Match } => true
-                            _ => false
-                          }
-                        Absent => false
+          match body_lower_unwrap_captured(shell: shell) {
+            Present { value: captured } =>
+              match body_lower_try_match_from_captured(captured: captured) {
+                Rejected { diagnostics: _ } => false
+                Accepted { value: lowered_opt, diagnostics: _ } =>
+                  match lowered_opt {
+                    Present { value: lowered } =>
+                      match lowered.kind {
+                        ComputationNode { behavior: Match } => true
+                        _ => false
                       }
+                    Absent => false
                   }
-                Absent => false
               }
+            Absent => false
           }
       }
   }
@@ -178,21 +173,17 @@ fn body_lowering_match_arms_found() -> Bool {
       match body_lowering_find_match_expr(root: tree) {
         Absent => false
         Present { value: shell } =>
-          match body_lower_unwrap_captured(remaining: node_subtree_count(n: shell), shell: shell) {
-            Rejected { diagnostics: _ } => false
-            Accepted { value: captured_opt, diagnostics: _ } =>
-              match captured_opt {
-                Present { value: captured } =>
-                  match body_lower_match_arms_optional(remaining: node_subtree_count(n: captured), captured: captured) {
-                    Rejected { diagnostics: _ } => false
-                    Accepted { value: arms_opt, diagnostics: _ } =>
-                      match arms_opt {
-                        Present { value: arms } => length(xs: arms) > 0
-                        Absent => false
-                      }
+          match body_lower_unwrap_captured(shell: shell) {
+            Present { value: captured } =>
+              match body_lower_match_arms_optional(captured: captured) {
+                Rejected { diagnostics: _ } => false
+                Accepted { value: arms_opt, diagnostics: _ } =>
+                  match arms_opt {
+                    Present { value: arms } => length(xs: arms) > 0
+                    Absent => false
                   }
-                Absent => false
               }
+            Absent => false
           }
       }
   }
@@ -205,40 +196,33 @@ fn body_lowering_match_first_arm_wires() -> Bool {
       match body_lowering_find_match_expr(root: tree) {
         Absent => false
         Present { value: shell } =>
-          match body_lower_unwrap_captured(remaining: node_subtree_count(n: shell), shell: shell) {
-            Rejected { diagnostics: _ } => false
-            Accepted { value: captured_opt, diagnostics: _ } =>
-              match captured_opt {
-                Present { value: captured } =>
-                  match parse_subtree_find_production_captured(
-                    root: captured,
-                    emitted: ^dag_surface_match_arm
-                  ) {
-                    ParseSubtreeFound { captured: arm } =>
-                      match body_lower_wire_match_arm_capture(remaining: node_subtree_count(n: arm), arm_capture: arm) {
-                        Accepted { value: _, diagnostics: _ } => true
-                        Rejected { diagnostics: _ } => false
-                      }
-                    ParseSubtreeAbsent => false
+          match body_lower_unwrap_captured(shell: shell) {
+            Present { value: captured } =>
+              match parse_subtree_find_production_captured(
+                root: captured,
+                emitted: ^dag_surface_match_arm
+              ) {
+                ParseSubtreeFound { captured: arm } =>
+                  match body_lower_wire_match_arm_capture(arm_capture: arm) {
+                    Accepted { value: _, diagnostics: _ } => true
+                    Rejected { diagnostics: _ } => false
                   }
-                Absent => false
+                ParseSubtreeAbsent => false
               }
+            Absent => false
           }
       }
   }
 }
 
-data unnavigable_arm_budget_note: String = "The step budget carries slack past the synthetic arm's own subtree count (1) so the walk reaches arm navigation and refuses with the pinned ^body_lowering_reason_match_arm_navigation_refused — an exact-count budget exhausts first and the witness would assert the wrong refusal (^body_lowering_reason_descent_not_proven)."
+data unnavigable_arm_budget_note: String = "Synthetic empty Conj arm capture has no navigable match_arm production spine — body_lower_wire_match_arm_capture must refuse with ^body_lowering_reason_match_arm_navigation_refused (structural termination; no fuel budget)."
 
 fn body_lowering_match_unnavigable_arm_refuses() -> Bool {
   let unnavigable_arm = node_synthetic(
     kind: TypeNode { connective: Conj },
     children: Empty
   )
-  match body_lower_wire_match_arm_capture(
-    remaining: node_subtree_count(n: unnavigable_arm) + 8,
-    arm_capture: unnavigable_arm
-  ) {
+  match body_lower_wire_match_arm_capture(arm_capture: unnavigable_arm) {
     Rejected { diagnostics: d } =>
       d.head.reason == ^body_lowering_reason_match_arm_navigation_refused
     Accepted { value: _, diagnostics: _ } => false
diff --git a/src/v2/test/claim/manual/body_lowering_normalize_add.dag b/src/v2/test/claim/manual/body_lowering_normalize_add.dag
index f03a82b355e..c8df517757e 100644
--- a/src/v2/test/claim/manual/body_lowering_normalize_add.dag
+++ b/src/v2/test/claim/manual/body_lowering_normalize_add.dag
@@ -32,7 +32,6 @@ import v2.std.node {
   Node,
   Transform,
   TypeNode,
-  node_subtree_count,
   node_synthetic,
   well_formed
 }
@@ -154,17 +153,13 @@ fn body_lowering_fn_body_subtree_holds() -> Bool {
   match body_lowering_parsed_fn_decl() {
     Absent => false
     Present { value: fn_decl } =>
-      match body_lower_unwrap_captured(remaining: node_subtree_count(n: fn_decl), shell: fn_decl) {
-        Rejected { diagnostics: _ } => false
-        Accepted { value: captured_opt, diagnostics: _ } =>
-          match captured_opt {
-            Present { value: captured } =>
-              match parse_subtree_find_production_captured(root: captured, emitted: ^dag_surface_fn_body) {
-                ParseSubtreeFound { captured: _ } => true
-                ParseSubtreeAbsent => false
-              }
-            Absent => false
+      match body_lower_unwrap_captured(shell: fn_decl) {
+        Present { value: captured } =>
+          match parse_subtree_find_production_captured(root: captured, emitted: ^dag_surface_fn_body) {
+            ParseSubtreeFound { captured: _ } => true
+            ParseSubtreeAbsent => false
           }
+        Absent => false
       }
   }
 }
@@ -173,13 +168,9 @@ fn body_lowering_arrow_token_holds() -> Bool {
   match body_lowering_parsed_fn_decl() {
     Absent => false
     Present { value: fn_decl } =>
-      match body_lower_unwrap_captured(remaining: node_subtree_count(n: fn_decl), shell: fn_decl) {
-        Rejected { diagnostics: _ } => false
-        Accepted { value: captured_opt, diagnostics: _ } =>
-          match captured_opt {
-            Present { value: captured } => body_lower_has_arrow_token(root: captured)
-            Absent => false
-          }
+      match body_lower_unwrap_captured(shell: fn_decl) {
+        Present { value: captured } => body_lower_has_arrow_token(root: captured)
+        Absent => false
       }
   }
 }
@@ -198,18 +189,14 @@ fn body_lowering_has_plus_token() -> Bool {
   match body_lowering_parsed_fn_decl() {
     Absent => false
     Present { value: fn_decl } =>
-      match body_lower_unwrap_captured(remaining: node_subtree_count(n: fn_decl), shell: fn_decl) {
-        Rejected { diagnostics: _ } => false
-        Accepted { value: captured_opt, diagnostics: _ } =>
-          match captured_opt {
-            Present { value: captured } =>
-              fold(
-                body_lower_collect_atoms(root: captured, acc: Empty),
-                init: false,
-                f: fn(acc, sym) { acc || sym == ^dag_token_plus }
-              )
-            Absent => false
-          }
+      match body_lower_unwrap_captured(shell: fn_decl) {
+        Present { value: captured } =>
+          fold(
+            body_lower_collect_atoms(root: captured, acc: Empty),
+            init: false,
+            f: fn(acc, sym) { acc || sym == ^dag_token_plus }
+          )
+        Absent => false
       }
   }
 }
@@ -218,25 +205,17 @@ fn body_lowering_binary_infix_holds() -> Bool {
   match body_lowering_parsed_fn_decl() {
     Absent => false
     Present { value: fn_decl } =>
-      match body_lower_unwrap_captured(remaining: node_subtree_count(n: fn_decl), shell: fn_decl) {
-        Rejected { diagnostics: _ } => false
-        Accepted { value: captured_opt, diagnostics: _ } =>
-          match captured_opt {
-            Present { value: captured } =>
-              match parse_subtree_find_production_captured(root: captured, emitted: ^dag_surface_binary_expr) {
-                ParseSubtreeFound { captured: binary } =>
-                  match body_lower_try_infix_transform(remaining: node_subtree_count(n: binary), node: binary) {
-                    Rejected { diagnostics: _ } => false
-                    Accepted { value: lowered_opt, diagnostics: _ } =>
-                      match lowered_opt {
-                        Present { value: _ } => true
-                        Absent => false
-                      }
-                  }
-                ParseSubtreeAbsent => false
+      match body_lower_unwrap_captured(shell: fn_decl) {
+        Present { value: captured } =>
+          match parse_subtree_find_production_captured(root: captured, emitted: ^dag_surface_binary_expr) {
+            ParseSubtreeFound { captured: binary } =>
+              match body_lower_try_infix_transform(node: binary) {
+                Present { value: _ } => true
+                Absent => false
               }
-            Absent => false
+            ParseSubtreeAbsent => false
           }
+        Absent => false
       }
   }
 }
@@ -245,25 +224,17 @@ fn body_lowering_expr_infix_holds() -> Bool {
   match body_lowering_parsed_fn_decl() {
     Absent => false
     Present { value: fn_decl } =>
-      match body_lower_unwrap_captured(remaining: node_subtree_count(n: fn_decl), shell: fn_decl) {
-        Rejected { diagnostics: _ } => false
-        Accepted { value: captured_opt, diagnostics: _ } =>
-          match captured_opt {
-            Present { value: captured } =>
-              match parse_subtree_find_production_captured(root: captured, emitted: ^dag_surface_expr) {
-                ParseSubtreeFound { captured: expr } =>
-                  match body_lower_try_infix_transform(remaining: node_subtree_count(n: expr), node: expr) {
-                    Rejected { diagnostics: _ } => false
-                    Accepted { value: lowered_opt, diagnostics: _ } =>
-                      match lowered_opt {
-                        Present { value: _ } => true
-                        Absent => false
-                      }
-                  }
-                ParseSubtreeAbsent => false
+      match body_lower_unwrap_captured(shell: fn_decl) {
+        Present { value: captured } =>
+          match parse_subtree_find_production_captured(root: captured, emitted: ^dag_surface_expr) {
+            ParseSubtreeFound { captured: expr } =>
+              match body_lower_try_infix_transform(node: expr) {
+                Present { value: _ } => true
+                Absent => false
               }
-            Absent => false
+            ParseSubtreeAbsent => false
           }
+        Absent => false
       }
   }
 }
@@ -272,25 +243,17 @@ fn body_lowering_fn_body_infix_holds() -> Bool {
   match body_lowering_parsed_fn_decl() {
     Absent => false
     Present { value: fn_decl } =>
-      match body_lower_unwrap_captured(remaining: node_subtree_count(n: fn_decl), shell: fn_decl) {
-        Rejected { diagnostics: _ } => false
-        Accepted { value: captured_opt, diagnostics: _ } =>
-          match captured_opt {
-            Present { value: captured } =>
-              match parse_subtree_find_production_captured(root: captured, emitted: ^dag_surface_fn_body) {
-                ParseSubtreeFound { captured: body } =>
-                  match body_lower_try_infix_transform(remaining: node_subtree_count(n: body), node: body) {
-                    Rejected { diagnostics: _ } => false
-                    Accepted { value: lowered_opt, diagnostics: _ } =>
-                      match lowered_opt {
-                        Present { value: _ } => true
-                        Absent => false
-                      }
-                  }
-                ParseSubtreeAbsent => false
+      match body_lower_unwrap_captured(shell: fn_decl) {
+        Present { value: captured } =>
+          match parse_subtree_find_production_captured(root: captured, emitted: ^dag_surface_fn_body) {
+            ParseSubtreeFound { captured: body } =>
+              match body_lower_try_infix_transform(node: body) {
+                Present { value: _ } => true
+                Absent => false
               }
-            Absent => false
+            ParseSubtreeAbsent => false
           }
+        Absent => false
       }
   }
 }
@@ -306,25 +269,17 @@ fn body_lowering_domain_holds() -> Bool {
   match body_lowering_parsed_fn_decl() {
     Absent => false
     Present { value: fn_decl } =>
-      match body_lower_unwrap_captured(remaining: node_subtree_count(n: fn_decl), shell: fn_decl) {
-        Rejected { diagnostics: _ } => false
-        Accepted { value: captured_opt, diagnostics: _ } =>
-          match captured_opt {
-            Present { value: captured } =>
-              match parse_subtree_find_production_captured(root: captured, emitted: ^dag_surface_param_list) {
-                ParseSubtreeFound { captured: param_list } =>
-                  match body_lower_domain_from_param_list(remaining: node_subtree_count(n: param_list), param_list: param_list) {
-                    Rejected { diagnostics: _ } => false
-                    Accepted { value: lowered_opt, diagnostics: _ } =>
-                      match lowered_opt {
-                        Present { value: _ } => true
-                        Absent => false
-                      }
-                  }
-                ParseSubtreeAbsent => false
+      match body_lower_unwrap_captured(shell: fn_decl) {
+        Present { value: captured } =>
+          match parse_subtree_find_production_captured(root: captured, emitted: ^dag_surface_param_list) {
+            ParseSubtreeFound { captured: param_list } =>
+              match body_lower_domain_from_param_list(param_list: param_list) {
+                Present { value: _ } => true
+                Absent => false
               }
-            Absent => false
+            ParseSubtreeAbsent => false
           }
+        Absent => false
       }
   }
 }
@@ -333,21 +288,17 @@ fn body_lowering_body_holds() -> Bool {
   match body_lowering_parsed_fn_decl() {
     Absent => false
     Present { value: fn_decl } =>
-      match body_lower_unwrap_captured(remaining: node_subtree_count(n: fn_decl), shell: fn_decl) {
-        Rejected { diagnostics: _ } => false
-        Accepted { value: captured_opt, diagnostics: _ } =>
-          match captured_opt {
-            Present { value: captured } =>
-              match body_lower_body_from_fn_captured(remaining: node_subtree_count(n: captured), captured: captured) {
-                Rejected { diagnostics: _ } => false
-                Accepted { value: body_opt, diagnostics: _ } =>
-                  match body_opt {
-                    Present { value: _ } => true
-                    Absent => false
-                  }
+      match body_lower_unwrap_captured(shell: fn_decl) {
+        Present { value: captured } =>
+          match body_lower_body_from_fn_captured(captured: captured) {
+            Rejected { diagnostics: _ } => false
+            Accepted { value: body_opt, diagnostics: _ } =>
+              match body_opt {
+                Present { value: _ } => true
+                Absent => false
               }
-            Absent => false
           }
+        Absent => false
       }
   }
 }
@@ -356,21 +307,13 @@ fn body_lowering_return_holds() -> Bool {
   match body_lowering_parsed_fn_decl() {
     Absent => false
     Present { value: fn_decl } =>
-      match body_lower_unwrap_captured(remaining: node_subtree_count(n: fn_decl), shell: fn_decl) {
-        Rejected { diagnostics: _ } => false
-        Accepted { value: captured_opt, diagnostics: _ } =>
-          match captured_opt {
-            Present { value: captured } =>
-              match body_lower_return_type_from_fn_captured(remaining: node_subtree_count(n: captured), captured: captured) {
-                Rejected { diagnostics: _ } => false
-                Accepted { value: lowered_opt, diagnostics: _ } =>
-                  match lowered_opt {
-                    Present { value: _ } => true
-                    Absent => false
-                  }
-              }
+      match body_lower_unwrap_captured(shell: fn_decl) {
+        Present { value: captured } =>
+          match body_lower_return_type_from_fn_captured(captured: captured) {
+            Present { value: _ } => true
             Absent => false
           }
+        Absent => false
       }
   }
 }
@@ -379,7 +322,7 @@ fn body_lowering_arrow_direct_well_formed() -> Bool {
   match body_lowering_parsed_fn_decl() {
     Absent => false
     Present { value: fn_decl } =>
-      match body_lower_fn_decl_to_arrow(remaining: node_subtree_count(n: fn_decl), shell: fn_decl) {
+      match body_lower_fn_decl_to_arrow(shell: fn_decl) {
         Accepted { value: arrow, diagnostics: _ } => well_formed(n: arrow)
         Rejected { diagnostics: _ } => false
       }
@@ -411,7 +354,7 @@ fn body_lowering_direct_arrow_domain_param_count() -> Int {
   match body_lowering_parsed_fn_decl() {
     Absent => 0
     Present { value: fn_decl } =>
-      match body_lower_fn_decl_to_arrow(remaining: node_subtree_count(n: fn_decl), shell: fn_decl) {
+      match body_lower_fn_decl_to_arrow(shell: fn_decl) {
         Accepted { value: arrow, diagnostics: _ } =>
           body_lowering_arrow_domain_named_count(arrow: arrow)
         Rejected { diagnostics: _ } => 0
diff --git a/src/v2/test/claim/manual/body_lowering_projection_call.dag b/src/v2/test/claim/manual/body_lowering_projection_call.dag
index 6ed196d4fac..e955ea1b9c4 100644
--- a/src/v2/test/claim/manual/body_lowering_projection_call.dag
+++ b/src/v2/test/claim/manual/body_lowering_projection_call.dag
@@ -22,7 +22,6 @@ import v2.std.node {
   Node,
   Transform,
   TypeNode,
-  node_subtree_count,
   node_synthetic
 }
 import v2.std.verification {
@@ -97,25 +96,21 @@ fn body_lowering_projection_lowers_to_transform() -> Bool {
       match body_lowering_find_postfix_expr(root: tree) {
         Absent => false
         Present { value: postfix } =>
-          match body_lower_unwrap_captured(remaining: node_subtree_count(n: postfix), shell: postfix) {
-            Rejected { diagnostics: _ } => false
-            Accepted { value: captured_opt, diagnostics: _ } =>
-              match captured_opt {
-                Present { value: captured } =>
-                  match body_lower_try_postfix_projection(remaining: node_subtree_count(n: captured), node: captured) {
-                    Rejected { diagnostics: _ } => false
-                    Accepted { value: found, diagnostics: _ } =>
-                      match found {
-                        Present { value: lowered } =>
-                          match lowered.kind {
-                            ComputationNode { behavior: Transform } => true
-                            _ => false
-                          }
-                        Absent => false
+          match body_lower_unwrap_captured(shell: postfix) {
+            Present { value: captured } =>
+              match body_lower_try_postfix_projection(node: captured) {
+                Rejected { diagnostics: _ } => false
+                Accepted { value: found, diagnostics: _ } =>
+                  match found {
+                    Present { value: lowered } =>
+                      match lowered.kind {
+                        ComputationNode { behavior: Transform } => true
+                        _ => false
                       }
+                    Absent => false
                   }
-                Absent => false
               }
+            Absent => false
           }
       }
   }
@@ -138,17 +133,13 @@ fn body_lowering_field_access_postfix_rejects() -> Bool {
           match body_lowering_find_postfix_expr(root: artifact.tree) {
             Absent => false
             Present { value: postfix } =>
-              match body_lower_unwrap_captured(remaining: node_subtree_count(n: postfix), shell: postfix) {
-                Rejected { diagnostics: _ } => false
-                Accepted { value: captured_opt, diagnostics: _ } =>
-                  match captured_opt {
-                    Present { value: captured } =>
-                      match body_lower_try_postfix_projection(remaining: node_subtree_count(n: captured), node: captured) {
-                        Rejected { diagnostics: _ } => true
-                        Accepted { value: _, diagnostics: _ } => false
-                      }
-                    Absent => false
+              match body_lower_unwrap_captured(shell: postfix) {
+                Present { value: captured } =>
+                  match body_lower_try_postfix_projection(node: captured) {
+                    Rejected { diagnostics: _ } => true
+                    Accepted { value: _, diagnostics: _ } => false
                   }
+                Absent => false
               }
           }
       }