diff --git a/differential/src/act.rs b/differential/src/act.rs
index 8474623f..7561f87d 100644
--- a/differential/src/act.rs
+++ b/differential/src/act.rs
@@ -37,7 +37,7 @@ impl<'t, S: AsRef<[u8]>> ReadSource for ACTZipper<'t, S, u64> {
 /// Decode and execute a fuzzer input with an ACT built from map1 as the read
 /// source.  See `bin/act_trace.rs` for what this does and does not exercise.
 pub fn run_act(bytes: &[u8], check: bool) -> String {
-    let mut d = Dec { bytes, pos: 0 };
+    let Some(mut d) = Dec::new(bytes) else { return "EMPTY\n".to_string(); };
     let (mut map0, map1, root0, root1) = match decode_header(&mut d) {
         Some(x) => x,
         None => return "EMPTY\n".to_string(),
diff --git a/differential/src/bin/act_trace.rs b/differential/src/bin/act_trace.rs
index ffe17a26..a3cbd734 100644
--- a/differential/src/bin/act_trace.rs
+++ b/differential/src/bin/act_trace.rs
@@ -27,6 +27,10 @@ use differential::*;
 
 fn main() {
     let args: Vec<String> = std::env::args().skip(1).collect();
+    if args.iter().any(|a| a == "--input-header") {
+        println!("{}", hex_path(&input_header()));
+        return;
+    }
     let check = args.iter().any(|a| a == "--check");
     // Resident mode: one process, many inputs over stdin.  See `serve`.
     if args.iter().any(|a| a == "--server") {
diff --git a/differential/src/bin/pathmap_trace.rs b/differential/src/bin/pathmap_trace.rs
index 64bd28c3..03991f91 100644
--- a/differential/src/bin/pathmap_trace.rs
+++ b/differential/src/bin/pathmap_trace.rs
@@ -10,6 +10,10 @@ use differential::*;
 fn main() {
     // `--check` also asserts the structural invariants after every operation.
     let args: Vec<String> = std::env::args().skip(1).collect();
+    if args.iter().any(|a| a == "--input-header") {
+        println!("{}", hex_path(&input_header()));
+        return;
+    }
     let check = args.iter().any(|a| a == "--check");
     // Resident mode: one process, many inputs over stdin.  See `serve`.
     if args.iter().any(|a| a == "--server") {
diff --git a/differential/src/harness.rs b/differential/src/harness.rs
index e822db99..6ce9d761 100644
--- a/differential/src/harness.rs
+++ b/differential/src/harness.rs
@@ -24,8 +24,20 @@ use pathmap::zipper::*;
 // `str::lines()` recovers them then.
 use core::fmt::Write as _;
 
-/// Number of distinct operations. Must match `PathMapModel.Fuzz.nops`.
-pub const NOPS: usize = 56;
+/// Selector count for newly generated inputs. Keep operation IDs permanently assigned.
+pub const NOPS: usize = 57;
+/// Unversioned inputs retain their original operation decoding.
+pub const LEGACY_NOPS: usize = 56;
+/// Input header marker, followed by a little-endian u16 selector count (1..=256).
+pub const WIRE_MAGIC: &[u8] = b"PMFUZZ\x01\x00";
+
+/// Header for new inputs. Decoding always uses the recorded count, never `NOPS`.
+pub fn input_header() -> Vec<u8> {
+    assert!((1..=256).contains(&NOPS));
+    let mut header = WIRE_MAGIC.to_vec();
+    header.extend_from_slice(&(NOPS as u16).to_le_bytes());
+    header
+}
 /// Maximum operations executed. Must match the `maxSteps` default in `Fuzz.run`.
 pub const MAX_STEPS: usize = 256;
 /// Maximum entries in a `dump`. Must match `Fuzz.dumpAt`.
@@ -34,9 +46,24 @@ pub const DUMP_CAP: usize = 64;
 pub struct Dec<'a> {
     pub bytes: &'a [u8],
     pub pos: usize,
+    op_count: usize,
 }
 
 impl<'a> Dec<'a> {
+    pub fn new(bytes: &'a [u8]) -> Option<Self> {
+        let (pos, op_count) = if bytes.starts_with(WIRE_MAGIC) {
+            let count_bytes = bytes.get(WIRE_MAGIC.len()..WIRE_MAGIC.len() + 2)?;
+            let count = u16::from_le_bytes([count_bytes[0], count_bytes[1]]) as usize;
+            if !(1..=256).contains(&count) { return None; }
+            (WIRE_MAGIC.len() + 2, count)
+        } else {
+            (0, LEGACY_NOPS)
+        };
+        Some(Self { bytes, pos, op_count })
+    }
+    pub fn op(&mut self) -> Option<usize> {
+        self.modn(self.op_count)
+    }
     pub fn u8(&mut self) -> Option<u8> {
         let b = *self.bytes.get(self.pos)?;
         self.pos += 1;
@@ -427,7 +454,7 @@ pub fn decode_header(d: &mut Dec) -> Option<(PathMap<u64>, PathMap<u64>, Vec<u8>
 /// Decode and execute a fuzzer input against a `PathMap` read source.
 ///
 pub fn run(bytes: &[u8], check: bool) -> String {
-    let mut d = Dec { bytes, pos: 0 };
+    let Some(mut d) = Dec::new(bytes) else { return "EMPTY\n".to_string(); };
     let (mut map0, map1, root0, root1) = match decode_header(&mut d) {
         Some(x) => x,
         None => return "EMPTY\n".to_string(),
@@ -478,7 +505,7 @@ pub fn run_ops<R: ReadSource>(
             if step >= MAX_STEPS {
                 break;
             }
-            let op = get!(d.u8()) as usize % NOPS;
+            let op = get!(d.op());
             let (name, ret): (&str, String) = match op {
                 0 => {
                     let t = get!(d.modn(2));
@@ -903,6 +930,10 @@ pub fn run_ops<R: ReadSource>(
                     let p = get!(d.path(6));
                     ("meet_2", show_status_opt((*rz).do_meet_2(&mut wz, &p)))
                 }
+                56 => {
+                    let pr = get!(d.boolean());
+                    ("remove_subtrie", show_bool(wz.remove_subtrie(pr)).to_string())
+                }
                 47 => {
                     let t = get!(d.modn(2));
                     // The blind-zipper addition: `descend_until` reporting the
@@ -932,3 +963,89 @@ pub fn run_ops<R: ReadSource>(
     }
 
 }
+
+#[cfg(test)]
+mod input_format_tests {
+    use super::*;
+    use crate::{emit_repro, run_act};
+
+    #[test]
+    fn unversioned_inputs_keep_legacy_operation_decoding() {
+        let bytes: Vec<u8> = (0..=255).collect();
+        let mut d = Dec::new(&bytes).unwrap();
+        for byte in 0..=255 {
+            assert_eq!(d.op(), Some(byte % 56));
+        }
+    }
+
+    #[test]
+    fn input_header_count_controls_decoding_independently_of_current_operation_count() {
+        for count in [1u16, 32, 56, 57, 58, 256] {
+            let mut bytes = WIRE_MAGIC.to_vec();
+            bytes.extend_from_slice(&count.to_le_bytes());
+            bytes.extend(0..=255);
+            let mut d = Dec::new(&bytes).unwrap();
+            for byte in 0..=255 {
+                assert_eq!(d.op(), Some(byte % count as usize));
+            }
+        }
+    }
+
+    #[test]
+    fn invalid_or_truncated_input_headers_are_rejected() {
+        let mut bytes = WIRE_MAGIC.to_vec();
+        assert!(Dec::new(&bytes).is_none());
+        bytes.push(57);
+        assert!(Dec::new(&bytes).is_none());
+        for count in [0u16, 257, u16::MAX] {
+            let mut bytes = WIRE_MAGIC.to_vec();
+            bytes.extend_from_slice(&count.to_le_bytes());
+            assert!(Dec::new(&bytes).is_none());
+            assert_eq!(run(&bytes, true), "EMPTY\n");
+            assert_eq!(run_act(&bytes, true), "EMPTY\n");
+        }
+    }
+
+    #[test]
+    fn header_count_56_preserves_legacy_replay_and_reproducer() {
+        for legacy in [
+            include_bytes!("../../lean/corpus/status-imprecise-join_map_into.bin").as_slice(),
+            include_bytes!("../../lean/corpus/status-imprecise-restrict.bin").as_slice(),
+        ] {
+            let mut bytes = WIRE_MAGIC.to_vec();
+            bytes.extend_from_slice(&56u16.to_le_bytes());
+            bytes.extend_from_slice(legacy);
+            assert_eq!(run(&bytes, false), run(legacy, false));
+            assert_eq!(run_act(&bytes, false), run_act(legacy, false));
+            assert_eq!(emit_repro(&bytes, 256), emit_repro(legacy, 256));
+        }
+    }
+
+    #[test]
+    fn trace_and_reproducer_decode_headered_write_operations() {
+        // Clear [0] and its descendant, prune the dangling focus, then write there again.
+        let mut bytes = input_header();
+        bytes.extend_from_slice(&[
+            4, 0, 9, 1, 0, 10, 2, 0, 1, 12, 1, 1, 11, // map0 entries.
+            1, 1, 2, 13, // map1 entry.
+            0, 0, // Zipper roots.
+            0, 0, 1, 0, // Descend to [0].
+            56, 0, 56, 1, 27, 14, // Remove, prune, then reuse.
+        ]);
+        let trace = run(&bytes, true);
+        assert!(
+            trace.contains("1 remove_subtrie ret=1 W=00 o00 e1 v- c0 n0"),
+            "{trace}"
+        );
+        assert!(
+            trace.contains("2 remove_subtrie ret=0 W=00 o00 e0 v- c0 n0"),
+            "{trace}"
+        );
+        assert!(trace.contains("MAP0 _:9,00:14,01:11"), "{trace}");
+        assert!(trace.contains("MAP1 _:-,02:13"), "{trace}");
+        let repro = emit_repro(&bytes, 256);
+        assert!(repro.contains("wz.remove_subtrie(false);"));
+        assert!(repro.contains("wz.remove_subtrie(true);"));
+        assert!(repro.contains("wz.set_val(14);"));
+    }
+}
diff --git a/differential/src/repro.rs b/differential/src/repro.rs
index 105638ee..21cd8697 100644
--- a/differential/src/repro.rs
+++ b/differential/src/repro.rs
@@ -45,7 +45,9 @@ pub fn rs_mask(p: &[u8]) -> String {
 /// `upto` is the number of operations to emit; the divergent step from a trace
 /// line `N <op> ...` is reproduced by `upto = N + 1`.
 pub fn emit_repro(bytes: &[u8], upto: usize) -> String {
-    let mut d = Dec { bytes, pos: 0 };
+    let Some(mut d) = Dec::new(bytes) else {
+        return "// Invalid fuzzer input header.\nfn main() {}\n".to_string();
+    };
     let mut o = String::new();
     o.push_str(
         "//! Generated by `pathmap_trace --repro`.  Reproduces a fuzzer input as\n\
@@ -113,8 +115,8 @@ pub fn emit_repro(bytes: &[u8], upto: usize) -> String {
     }
     let mut step = 0usize;
     while step < upto {
-        let op = match d.u8() {
-            Some(b) => b as usize % NOPS,
+        let op = match d.op() {
+            Some(op) => op,
             None => break,
         };
         // `z!` picks the zipper the target byte selects, exactly as `tgt!` does.
@@ -213,6 +215,7 @@ pub fn emit_repro(bytes: &[u8], upto: usize) -> String {
             55 => { let p = g!(d.path(6));
                     format!("{{ let mut b = map1.read_zipper_at_path({}); b.descend_to({}); wz.meet_2(&rz, &b); }}",
                             rs_bytes(&r1), rs_bytes(&p)) }
+            56 => { let pr = g!(d.boolean()); format!("wz.remove_subtrie({pr});") }
             _ => "// nop".to_string(),
         };
         o.push_str(&format!("    /* {step:3} */ {line}\n"));
diff --git a/lean/PathMapModel/Check.lean b/lean/PathMapModel/Check.lean
index 0e3b5dab..8f0c2b23 100644
--- a/lean/PathMapModel/Check.lean
+++ b/lean/PathMapModel/Check.lean
@@ -1,4 +1,5 @@
 import PathMapModel.Spec
+import PathMapModel.Fuzz
 
 /-!
 # Build-time checks
@@ -51,6 +52,20 @@ def probes : List Path := [[], [0], [1], [0,0], [0,1], [1,1], [0,1,2], [3]]
 def allZips : List (Zip UInt64) :=
   fixtures.flatMap (fun t => probes.map (fun p => zipAt t [] p))
 
+/-! The selector count belongs to each input, independent of the current operation table. -/
+
+def inputWithCount (lo hi : UInt8) : ByteArray :=
+  ByteArray.mk (Fuzz.wireMagic ++ [lo, hi]).toArray
+
+#guard ((Fuzz.Dec.init (ByteArray.mk #[])).map (·.opCount)) == some 56
+#guard ((Fuzz.Dec.init (inputWithCount 56 0)).map (·.opCount)) == some 56
+#guard ((Fuzz.Dec.init (inputWithCount 58 0)).map (·.opCount)) == some 58
+#guard ((Fuzz.Dec.init (inputWithCount 0 1)).map (·.opCount)) == some 256
+#guard (Fuzz.Dec.init (inputWithCount 0 0)).isNone
+#guard (Fuzz.Dec.init (inputWithCount 1 1)).isNone
+#guard (Fuzz.Dec.init (ByteArray.mk Fuzz.wireMagic.toArray)).isNone
+#guard (Fuzz.Dec.init (ByteArray.mk (Fuzz.wireMagic ++ [57]).toArray)).isNone
+
 /-! ## Regression fixtures from `src/write_zipper.rs` -/
 
 /-- `write_zipper_prune_path_test2`, first phase: removing the value at
@@ -127,6 +142,39 @@ def dropT1Result : T := ((zipAt dropT1 [0x31,0x32,0x33,0x3a] []).joinKPathInto o
 #guard dropT1Result.valAt [0x31,0x32,0x33,0x3a,0x42,0x6f,0x62,0x3a,0x46,0x69,0x64,0x6f] == some 1
 #guard dropT1Result.valCount [] == 2
 
+/-! ## Subtrie removal -/
+
+/-! `remove_subtrie` clears the focus and descendants, preserves other content,
+and prunes only up to the zipper root. Dangling descendants count as branches;
+pruning an already dangling focus does not count as removing content. -/
+
+#guard ((zipAt fBranch [] [0]).removeSubtrie false).1
+#guard ((zipAt fBranch [] [0]).removeSubtrie false).2.pathExists
+#guard !((zipAt fBranch [] [0]).removeSubtrie false).2.isVal
+#guard ((zipAt fBranch [] [0]).removeSubtrie false).2.childCount == 0
+#guard ((zipAt fBranch [] [0]).removeSubtrie true).2.trie.valAt [] == some 0
+#guard ((zipAt fBranch [] [0]).removeSubtrie true).2.trie.valAt [1] == some 4
+#guard !((zipAt fBranch [] [0]).removeSubtrie true).2.pathExists
+#guard ((zipAt fBranch [] []).removeSubtrie true).2.trie.isEmptyMap
+#guard !(((zipAt fBranch [] []).removeSubtrie true).2.removeSubtrie true).1
+#guard ((zipAt fDangle [] [0,1]).removeSubtrie false).1
+#guard !((zipAt fDangle [] [0,1,2]).removeSubtrie true).1
+#guard !((zipAt fDangle [] [0,1,2]).removeSubtrie true).2.pathExists
+#guard !((zipAt fEmpty [] [3]).removeSubtrie true).1
+#guard !((zipAt fEmpty [] [3]).removeSubtrie true).2.pathExists
+#guard ((zipAt fRun [0,0] [0]).removeSubtrie true).2.trie.pathExists [0,0]
+#guard !((zipAt fRun [0,0] [0]).removeSubtrie true).2.trie.pathExists [0,0,0]
+#guard ((zipAt fRun [0,0] []).removeSubtrie true).2.pathExists
+
+#guard allZips.all (fun z => [false, true].all (fun pr =>
+  let (removed, after) := z.removeSubtrie pr
+  let (branches, z1) := z.removeBranches pr
+  let (value, composed) := z1.removeVal pr
+  removed == (branches || value.isSome) &&
+    after.trie.vals == composed.trie.vals && after.trie.paths == composed.trie.paths &&
+    after.path == z.path && after.root == z.root &&
+    !after.isVal && after.childCount == 0))
+
 /-! ## Structural invariants over every fixture -/
 
 #guard fixtures.all valsExist
diff --git a/lean/PathMapModel/Fuzz.lean b/lean/PathMapModel/Fuzz.lean
index 9175ec6b..5d789eb9 100644
--- a/lean/PathMapModel/Fuzz.lean
+++ b/lean/PathMapModel/Fuzz.lean
@@ -23,9 +23,14 @@ header:
   r0        := u8 % 4 ; r0 × pathbyte    -- write zipper root
   r1        := u8 % 4 ; r1 × pathbyte    -- read  zipper root
 body:
-  repeated: op := u8 % 56 ; operands per op (see `Op.decode`)
+  repeated: op := u8 % 56 ; operands per op (see `step`)
 ```
 
+Inputs prefixed with `PMFUZZ\x01\x00` followed by a little-endian u16 selector
+count (1..=256) use the same map/zipper header but decode operations modulo that
+recorded count. Headerless inputs use 56. Operation 56 is `remove_subtrie`,
+followed by a prune byte.
+
 Every **path byte** is masked to `b % 4`, so the generated tries share prefixes
 heavily — that is where the interesting trie shapes (branch points, dangling
 chains, single-child runs) live.
@@ -115,6 +120,7 @@ def dumpAt (t : PathMap V) (root : Path) : String :=
 structure Dec where
   bytes : ByteArray
   pos : Nat
+  opCount : Nat := 56
 
 /-- Read one byte; `none` once the input is exhausted, which ends the program. -/
 def Dec.u8 (d : Dec) : Option (UInt8 × Dec) :=
@@ -188,12 +194,22 @@ def showBool (b : Bool) : String := if b then "1" else "0"
 
 /-! ## The operation table
 
-`op % 56` selects the operation.  Ops `0`–`26` act on a target zipper chosen by
-a following `u8 % 2` byte (`0` = write zipper, `1` = read zipper); ops `27`–`46`
-are write-zipper operations. -/
+`op % selector_count` selects the operation (56 for headerless inputs). Ops `0`–`26`
+act on a target zipper chosen by a following `u8 % 2` byte (`0` = write zipper,
+`1` = read zipper); ops `27`–`46` and `56` are write-zipper operations. -/
+
+/-- Input header marker. Must match `WIRE_MAGIC` in the Rust harness. -/
+def wireMagic : List UInt8 := [80, 77, 70, 85, 90, 90, 1, 0]
 
-/-- Number of distinct operations.  Must match `NOPS` in `differential/src/harness.rs`. -/
-def nops : Nat := 56
+def Dec.init (bytes : ByteArray) : Option Dec := do
+  if bytes.data.toList.take wireMagic.length == wireMagic then
+    let d : Dec := { bytes, pos := wireMagic.length }
+    let (lo, d) ← d.u8
+    let (hi, d) ← d.u8
+    let count := lo.toNat + 256 * hi.toNat
+    if count == 0 || count > 256 then none
+    else some { d with opCount := count }
+  else some { bytes, pos := 0 }
 
 /-- A full `k`-path iteration: `descend_first_k_path` followed by
 `to_next_k_path` until it runs out (capped at 32 stops).  Returns the locations
@@ -225,7 +241,7 @@ def getTarget (s : St) (t : Nat) : Zip V := if t == 0 then s.wz else s.rz
 which ends the program. -/
 def step (s : St) (d : Dec) : Option (St × Dec) := do
   let (opRaw, d) ← d.u8
-  let op := opRaw.toNat % nops
+  let op := opRaw.toNat % d.opCount
   match op with
   | 0 => do let (t, d) ← d.mod 2; let (p, d) ← d.path
             let (_, s) := onTarget s t (fun z => ((), z.descendTo p))
@@ -510,6 +526,9 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do
                let b := { s.rz with path := s.rz.path ++ p }
                let (st, z) := s.wz.meet2 ops s.rz b
                some (emit { s with wz := z } "meet_2" (toString st), d)
+  | 56 => do let (pr, d) ← d.bool
+             let (removed, z) := s.wz.removeSubtrie pr
+             some (emit { s with wz := z } "remove_subtrie" (showBool removed), d)
   | _ => some (emit s "nop" "-", d)
 
 /-- Run operations until the input is exhausted or `fuel` runs out. -/
@@ -553,7 +572,7 @@ def header (d : Dec) (act : Bool) : Option (St × Dec) := do
 
 /-- Decode and run a fuzzer input, returning the trace lines. -/
 def run (bytes : ByteArray) (maxSteps : Nat := 256) (act : Bool := false) : List String :=
-  match header { bytes, pos := 0 } act with
+  match Dec.init bytes >>= (fun d => header d act) with
   | none => ["EMPTY"]
   | some (s0, d) =>
       let s := loop maxSteps s0 d
diff --git a/lean/PathMapModel/Write.lean b/lean/PathMapModel/Write.lean
index c5e43eed..7f6f5ad4 100644
--- a/lean/PathMapModel/Write.lean
+++ b/lean/PathMapModel/Write.lean
@@ -114,6 +114,14 @@ def removeBranches (prune : Bool) : Bool × Zip V :=
   let z' := z.withTrie (z.trie.removeBelow z.focus)
   (removed, if prune then (z'.prunePath).2 else z')
 
+/-- `ZipperWriting::remove_subtrie`: remove the focus value and all descendants,
+then optionally prune. Returns whether a value or branch was removed; pruning
+alone does not count as removal. The cursor and zipper root do not move. -/
+def removeSubtrie (prune : Bool) : Bool × Zip V :=
+  let (branches, z1) := z.removeBranches false
+  let (value, z2) := z1.removeVal false
+  (branches || value.isSome, if prune then (z2.prunePath).2 else z2)
+
 /-- `ZipperWriting::remove_unmasked_branches`: keep only the child bytes set in
 `mask`; delete the rest along with their subtries. -/
 def removeUnmaskedBranches (mask : ByteMask) (prune : Bool) : Zip V :=
diff --git a/lean/README.md b/lean/README.md
index 7d39c2c8..240b64d9 100644
--- a/lean/README.md
+++ b/lean/README.md
@@ -211,6 +211,20 @@ body:
   repeated: op := u8 % 56 ; operands per op
 ```
 
+This is the headerless format, whose selector count is permanently 56. New
+inputs start with the eight bytes `PMFUZZ\x01\x00`, then a little-endian u16
+selector count (1 through 256), followed by the same map/zipper header. Operation
+bytes are reduced modulo the recorded count, independently of the running
+software's operation table. Truncated headers and invalid counts are rejected.
+Operation 56 is `remove_subtrie`, with one boolean prune operand.
+
+The random-input generator obtains the header from the selected Rust trace
+producer's `--input-header` option. `NOPS` in `differential/src/harness.rs` is
+the only definition of the current generation count; Lean and replay never
+consult it. Keep existing operation IDs and argument-decoding rules stable.
+Adding an operation requires its Lean/Rust handlers and reproducer entry, plus
+updating `NOPS`; the input format and old repros need no changes.
+
 Every path byte is masked to `b % 4`, so generated tries share prefixes heavily
 and actually branch — that is where the interesting shapes are (branch points,
 single-child runs, dangling chains).  Decoding stops when the input runs out.
@@ -223,6 +237,12 @@ is a textual diff.
 The op table lives in `Fuzz.lean` (`PathMapModel.Fuzz.step`) and
 `differential/src/harness.rs`; **the two must be changed together.**
 
+`Zip.removeSubtrie` clears the focus value and all descendants, then optionally
+prunes. Its boolean result counts removal of a value or branch, including a
+dangling descendant, but not pruning an already dangling focus. Build-time
+checks cover removal, unrelated content, cursor stability, and the zipper-root
+bound; differential operation 56 exercises the optimized Rust implementation.
+
 ### Front ends
 
 | binary | drives | built with |
diff --git a/lean/differential.py b/lean/differential.py
index cf5f6160..25f9ea84 100755
--- a/lean/differential.py
+++ b/lean/differential.py
@@ -481,8 +481,9 @@ class RandomInputs(InputSource):
     `randbytes` alone is ~39x faster than that loop.
     """
 
-    def __init__(self, seed, count, maxlen):
+    def __init__(self, seed, count, maxlen, input_header):
         self.seed, self.count, self.maxlen = seed, count, maxlen
+        self.input_header = input_header
 
     def __len__(self):
         return self.count
@@ -492,7 +493,7 @@ def name(self, idx):
 
     def get(self, idx):
         rng = random.Random((self.seed << 32) ^ idx)
-        return rng.randbytes(rng.randrange(8, self.maxlen))
+        return self.input_header + rng.randbytes(rng.randrange(8, self.maxlen))
 
 
 class FileInputs(InputSource):
@@ -606,7 +607,9 @@ def main():
     if args.files:
         sources.append(FileInputs(args.files))
     if args.random:
-        sources.append(RandomInputs(args.seed, args.random, args.maxlen))
+        # The Rust producer owns the count for new inputs; never duplicate it here or in Lean.
+        header_hex = subprocess.check_output([trace_bin, "--input-header"], text=True).strip()
+        sources.append(RandomInputs(args.seed, args.random, args.maxlen, bytes.fromhex(header_hex)))
     source = ChainInputs(sources)
     n_inputs = len(source)
 
diff --git a/pathmap-book/src/1.02.06_zipper_writing.md b/pathmap-book/src/1.02.06_zipper_writing.md
index ae0fb04a..742d4214 100644
--- a/pathmap-book/src/1.02.06_zipper_writing.md
+++ b/pathmap-book/src/1.02.06_zipper_writing.md
@@ -20,11 +20,12 @@ The [`ZipperWriting`] trait provides methods to modify the trie structure and va
 - [`remove_prefix`] removes the specified number of bytes from paths above the focus
 
 ## Subtrie Moving and Copying
-- [`graft`] replaces the subtrie below the focus with content from another zipper's focus
-- [`graft_map`] replaces the subtrie below the focus with the contents of a [`PathMap`]
-- [`take_map`] extracts the subtrie below the focus into a new [`PathMap`], removing it from the original
+- [`graft`] replaces the subtrie at the focus with the subtrie at another zipper's focus
+- [`graft_map`] replaces the subtrie at the focus with the contents of a [`PathMap`]
+- [`take_map`] extracts the subtrie at the focus into a new [`PathMap`], removing it from the original
 
 ## Branch Removal
+- [`remove_subtrie`] removes the focus value and all downstream branches
 - [`remove_branches`] removes all child branches below the focus
 - [`remove_unmasked_branches`] selectively removes branches based on a byte mask
 
diff --git a/pathmap-book/src/api_links.md b/pathmap-book/src/api_links.md
index 877a488a..373c83d7 100644
--- a/pathmap-book/src/api_links.md
+++ b/pathmap-book/src/api_links.md
@@ -115,6 +115,7 @@
 [`remove_branches_at`]: https://docs.rs/pathmap/latest/pathmap/struct.PathMap.html#method.remove_branches_at
 [`remove_branches`]: https://docs.rs/pathmap/latest/pathmap/zipper/trait.ZipperWriting.html#tymethod.remove_branches
 [`remove_prefix`]: https://docs.rs/pathmap/latest/pathmap/zipper/trait.ZipperWriting.html#tymethod.remove_prefix
+[`remove_subtrie`]: https://docs.rs/pathmap/latest/pathmap/zipper/trait.ZipperWriting.html#method.remove_subtrie
 [`remove_unmasked_branches`]: https://docs.rs/pathmap/latest/pathmap/zipper/trait.ZipperWriting.html#tymethod.remove_unmasked_branches
 [`remove_val`]: https://docs.rs/pathmap/latest/pathmap/zipper/trait.ZipperWriting.html#tymethod.remove_val
 [`reserve_buffers`]: https://docs.rs/pathmap/latest/pathmap/zipper/trait.ZipperPathBuffer.html#tymethod.reserve_buffers
diff --git a/src/write_zipper.rs b/src/write_zipper.rs
index e1e62aa3..4793cf9c 100644
--- a/src/write_zipper.rs
+++ b/src/write_zipper.rs
@@ -82,29 +82,30 @@ pub trait ZipperWriting<V: Clone + Send + Sync, A: Allocator = GlobalAlloc>: Wri
     /// Creates a [ZipperHead] at the zipper's current focus
     fn zipper_head<'z>(&'z mut self) -> Self::ZipperHead<'z>;
 
-    /// Replaces the trie below the zipper's focus with the subtrie downstream from the focus of `read_zipper`
-    ///
-    /// GOAT: This method's behavior is affected by the `graft_root_vals` feature
-    /// Without `graft_root_vals`, If there is a value at the zipper's focus, it will not be affected.
+    /// Replaces the subtrie at the zipper's focus with the subtrie at the focus of `read_zipper`
     ///
     /// NOTE: If the `read_zipper` is not on an existing path (according to [Zipper::path_exists]) then the
-    /// effect will be the same as calling both [remove_branches](ZipperWriting::remove_branches) and
-    /// [remove_val](ZipperWriting::remove_val)
+    /// effect will be the same as calling [remove_subtrie](ZipperWriting::remove_subtrie) with
+    /// `prune=false`.
     fn graft<Z: ZipperInfallibleSubtries<V, A>>(&mut self, read_zipper: &Z);
 
     /// Replaces the subtrie at the zipper's focus with the subtrie located at `path`, relative to the focus of
     /// the `src` zipper
     ///
-    /// If `path` does not specify an existing path then the effect will be the same as calling both
-    /// [remove_branches](ZipperWriting::remove_branches) and [remove_val](ZipperWriting::remove_val)
+    /// The destination focus value is replaced with the source value at `path`, or removed if the
+    /// source has no value there.
+    ///
+    /// If `path` does not specify an existing path then the effect will be the same as calling
+    /// [remove_subtrie](ZipperWriting::remove_subtrie) with `prune=false`.
     fn graft_src_at<Z: ZipperInfallibleSubtries<V, A>, K: AsRef<[u8]>>(&mut self, src: &Z, path: K);
 
-    /// Replaces the trie below the zipper's focus with the contents of a [PathMap], consuming the map
+    /// Replaces the subtrie at the zipper's focus with the contents of a [PathMap], consuming the map
     ///
-    /// If there is a value at the zipper's focus, it will not be affected.
-    /// GOAT: This method's behavior is affected by the `graft_root_vals` feature
+    /// The destination focus value is replaced with the map's root value, or removed if the map has
+    /// no root value.
     ///
-    /// NOTE: If the `map` is empty then the effect will be the same as [remove_branches](ZipperWriting::remove_branches)
+    /// NOTE: If the `map` is empty then the effect will be the same as calling
+    /// [remove_subtrie](ZipperWriting::remove_subtrie) with `prune=false`.
     fn graft_map(&mut self, map: PathMap<V, A>);
 
     /// Grafts each [PathMap] returned by the `maps` iterator at the corresponding child byte indicated by a 
@@ -321,6 +322,18 @@ pub trait ZipperWriting<V: Clone + Send + Sync, A: Allocator = GlobalAlloc>: Wri
     /// afterward, including at a pre-existing dangling tip. See the [pruning guide](https://pathmap-rs.github.io/1.02.06_zipper_writing.html#pruning-behavior).
     fn remove_branches(&mut self, prune: bool) -> bool;
 
+    /// Removes the subtrie at the zipper's focus, including its value and all downstream branches.
+    /// Returns `true` if a value or branch was removed, otherwise returns `false`.
+    /// The focus value is removed regardless of the `graft_root_vals` feature.
+    ///
+    /// `prune=false` leaves an emptied focus dangling; `prune=true` applies [Self::prune_path]
+    /// afterward, including at a pre-existing dangling tip. See the [pruning guide](https://pathmap-rs.github.io/1.02.06_zipper_writing.html#pruning-behavior).
+    fn remove_subtrie(&mut self, prune: bool) -> bool {
+        let removed_branches = self.remove_branches(prune);
+        let removed_val = self.remove_val(prune).is_some();
+        removed_branches || removed_val
+    }
+
     /// Removes multiple branches below the zipper's focus based on the supplied 256-bit `mask`
     ///
     /// Key bytes for which the corresponding `mask` bit is `0` will be removed.
@@ -398,6 +411,7 @@ impl<V: Clone + Send + Sync, Z, A: Allocator> ZipperWriting<V, A> for &mut Z whe
     fn restricting<RZ: ZipperInfallibleSubtries<V, A>>(&mut self, read_zipper: &RZ) -> bool { (**self).restricting(read_zipper) }
     fn take_map(&mut self, prune: bool) -> Option<PathMap<V, A>> { (**self).take_map(prune) }
     fn remove_branches(&mut self, prune: bool) -> bool { (**self).remove_branches(prune) }
+    fn remove_subtrie(&mut self, prune: bool) -> bool { (**self).remove_subtrie(prune) }
     fn remove_unmasked_branches(&mut self, mask: ByteMask, prune: bool) { (**self).remove_unmasked_branches(mask, prune) }
     fn create_path(&mut self) -> bool { (**self).create_path() }
     fn prune_path(&mut self) -> usize { (**self).prune_path() }
@@ -568,6 +582,7 @@ impl<'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> ZipperWriting
     fn restricting<Z: ZipperInfallibleSubtries<V, A>>(&mut self, read_zipper: &Z) -> bool { self.z.restricting(read_zipper) }
     fn take_map(&mut self, prune: bool) -> Option<PathMap<V, A>> { self.z.take_map(prune) }
     fn remove_branches(&mut self, prune: bool) -> bool { self.z.remove_branches(prune) }
+    fn remove_subtrie(&mut self, prune: bool) -> bool { self.z.remove_subtrie(prune) }
     fn remove_unmasked_branches(&mut self, mask: ByteMask, prune: bool) { self.z.remove_unmasked_branches(mask, prune) }
     fn create_path(&mut self) -> bool { self.z.create_path() }
     fn prune_path(&mut self) -> usize { self.z.prune_path() }
@@ -739,6 +754,7 @@ impl<'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> ZipperWriting
     fn restricting<Z: ZipperInfallibleSubtries<V, A>>(&mut self, read_zipper: &Z) -> bool { self.z.restricting(read_zipper) }
     fn take_map(&mut self, prune: bool) -> Option<PathMap<V, A>> { self.z.take_map(prune) }
     fn remove_branches(&mut self, prune: bool) -> bool { self.z.remove_branches(prune) }
+    fn remove_subtrie(&mut self, prune: bool) -> bool { self.z.remove_subtrie(prune) }
     fn remove_unmasked_branches(&mut self, mask: ByteMask, prune: bool) { self.z.remove_unmasked_branches(mask, prune) }
     fn create_path(&mut self) -> bool { self.z.create_path() }
     fn prune_path(&mut self) -> usize { self.z.prune_path() }
@@ -880,6 +896,7 @@ impl<V: Clone + Send + Sync + Unpin, A: Allocator> ZipperWriting<V, A> for Write
     fn restricting<Z: ZipperInfallibleSubtries<V, A>>(&mut self, read_zipper: &Z) -> bool { self.z.restricting(read_zipper) }
     fn take_map(&mut self, prune: bool) -> Option<PathMap<V, A>> { self.z.take_map(prune) }
     fn remove_branches(&mut self, prune: bool) -> bool { self.z.remove_branches(prune) }
+    fn remove_subtrie(&mut self, prune: bool) -> bool { self.z.remove_subtrie(prune) }
     fn remove_unmasked_branches(&mut self, mask: ByteMask, prune: bool) { self.z.remove_unmasked_branches(mask, prune) }
     fn create_path(&mut self) -> bool { self.z.create_path() }
     fn prune_path(&mut self) -> usize { self.z.prune_path() }
@@ -2302,6 +2319,30 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC
             }
         }
     }
+    /// Optimized implementation of [ZipperWriting::remove_subtrie].
+    pub fn remove_subtrie(&mut self, prune: bool) -> bool {
+        if self.key.node_key().is_empty() {
+            // At the map root, the value is stored separately from the branches.
+            let removed_branches = self.remove_branches(false);
+            let removed_val = self.remove_val(false).is_some();
+            return removed_branches || removed_val;
+        }
+
+        let prune_limit = self.node_prune_limit(prune);
+        let removed = {
+            // Hold one mutable node guard and defer pruning until both removals are complete.
+            let mut focus_node = self.focus_stack.top_mut().unwrap();
+            let key = self.key.node_key();
+            let removed_branches = focus_node.node_remove_all_branches(key, usize::MAX);
+            let removed_val = focus_node.node_remove_val(key, prune_limit).is_some();
+            removed_branches || removed_val
+        };
+        if prune {
+            self.prune_path_internal(false);
+        }
+        removed
+    }
+
     /// See [WriteZipper::take_map]
     pub fn take_map(&mut self, prune: bool) -> Option<PathMap<V, A>> {
         #[cfg(not(feature = "graft_root_vals"))]
@@ -7663,6 +7704,95 @@ mod tests {
         }
     }
 
+    #[test]
+    fn remove_subtrie_removes_focus_and_descendants() {
+        for prune in [false, true] {
+            for siblings in [1u8, 8] {
+                for root_len in [0, 1, 3] {
+                    // Include a long compressed continuation and a dangling descendant.
+                    let focus = [0u8, 0, 0];
+                    for shape in 0..6 {
+                        let mut original = PathMap::<u64>::new();
+                        original.set_val_at([], 99);
+                        for byte in 1..=siblings {
+                            original.set_val_at([byte], byte as u64);
+                        }
+                        match shape {
+                            0 => {}, // Absent focus.
+                            1 => { original.create_path(focus); },
+                            2 => { original.set_val_at(focus, 42); },
+                            3 => { original.set_val_at([0; 64], 43); },
+                            4 => {
+                                original.set_val_at(focus, 42);
+                                original.set_val_at([0; 64], 43);
+                                original.create_path([0, 0, 0, 1]);
+                            },
+                            5 => { original.create_path([0; 64]); },
+                            _ => unreachable!(),
+                        }
+                        let before = all_locations(&original);
+                        let mut expected = original.clone();
+                        let mut actual = original.clone();
+                        let expected_removed = {
+                            let mut z = expected.write_zipper_at_path(&focus[..root_len]);
+                            z.descend_to(&focus[root_len..]);
+                            let branches = z.remove_branches(prune);
+                            let value = z.remove_val(prune).is_some();
+                            branches || value
+                        };
+                        {
+                            let mut z = actual.write_zipper_at_path(&focus[..root_len]);
+                            z.descend_to(&focus[root_len..]);
+                            assert_eq!(z.remove_subtrie(prune), expected_removed,
+                                "shape={shape}, siblings={siblings}, root_len={root_len}, prune={prune}");
+                            assert_eq!(z.path(), &focus[root_len..]);
+                            assert!(!z.is_val());
+                            assert_eq!(z.child_count(), 0);
+                        }
+                        assert_eq!(all_locations(&actual), all_locations(&expected),
+                            "shape={shape}, siblings={siblings}, root_len={root_len}, prune={prune}");
+                        assert_valid_trie(actual.root());
+                        assert_eq!(all_locations(&original), before, "shared source changed");
+                    }
+                }
+            }
+        }
+    }
+
+    #[test]
+    fn remove_subtrie_clears_map_root_and_allows_owned_zipper_reuse() {
+        fn remove<Z: ZipperWriting<u64>>(mut z: Z, prune: bool) -> bool {
+            z.remove_subtrie(prune)
+        }
+        for prune in [false, true] {
+            for shape in 0..4 {
+                let mut map = PathMap::<u64>::new();
+                if shape & 1 != 0 { map.set_val_at([], 1); }
+                if shape & 2 != 0 { map.set_val_at(b"child", 2); }
+                {
+                    let mut z = map.write_zipper();
+                    assert_eq!(remove(&mut z, prune), shape != 0);
+                    assert!(!z.remove_subtrie(prune));
+                    assert!(z.at_root());
+                }
+                assert!(map.is_empty());
+                assert_valid_trie(map.root());
+
+                let mut owned = map.into_write_zipper([]);
+                owned.set_val(3);
+                assert!(owned.remove_subtrie(prune));
+                assert!(!owned.is_val());
+                owned.descend_to(b"child");
+                owned.set_val(4);
+                assert!(owned.remove_subtrie(prune));
+                assert_eq!(owned.path(), b"child");
+                // Reusing the zipper after pruning must still write at the same focus.
+                owned.set_val(5);
+                assert_eq!(owned.val(), Some(&5));
+            }
+        }
+    }
+
     #[test]
     fn remove_branches_at_dangling_focus_reports_no_branches() {
         for (shape, siblings, allocated_child) in [