The missed-deletion checker test now covers both branch directions,
and lcs_pairs gets an exhaustive reference-oracle test — every string
pair over {a,b,c} up to length four against a naive recursive LCS —
because the alignment tests under-constrain the DP (phase 3 rescues
small cases) and hand-picked cases let index-arithmetic mutants slip
through the backtrack's compensating paths.

.cargo/mutants.toml documents the equivalent mutants: anchor's
disjunct symmetry and index strictness, refine's empty-gap fast path,
budget boundary, and virtual-root arm, and lcs_pairs backtrack mutants
that only pick a different equally-long subsequence.

Assisted-by: Claude Fable 5 via Claude Code

diff --git a/.cargo/mutants.toml b/.cargo/mutants.toml
new file mode 100644
index 0000000..a36adca
--- /dev/null
+++ b/.cargo/mutants.toml
@@ -0,0 +1,37 @@
+# Equivalent mutants: each entry names a mutation that provably cannot
+# change observable behavior, with the argument. Keep this list short
+# and specific — a mutant goes here only after the equivalence argument
+# is written down.
+
+exclude_re = [
+    # anchor(): for a unique-unique candidate pair, s being matched
+    # implies d is matched and vice versa — a larger wholesale anchor
+    # pairs s with its positional counterpart, whose equal content and
+    # dst-side uniqueness force it to be d. Either disjunct implies
+    # the other, so || and && coincide.
+    'replace \|\| with && in anchor',
+    # anchor(): candidates are unmatched while placed roots are
+    # matched, so a candidate index never equals a placed root's and
+    # < versus <= cannot differ.
+    'replace < with <= in anchor',
+    # refine(): a gap empty on one side produces a ZS mapping with no
+    # real (Some, Some) pairs to fold; the skip is a fast path, not a
+    # behavior change.
+    'replace \|\| with && in refine',
+    # refine(): the ZS budget is an arbitrary tuning constant; > vs >=
+    # differs only for a residue of exactly 400 nodes and either
+    # behavior is acceptable there.
+    'replace > with >= in refine',
+    # refine()'s relabel closure: if the virtual forest roots cannot
+    # pair, every candidate mapping pays the same uniform +2 (delete
+    # plus insert of the roots), so the optimal child mapping — the
+    # only thing folded — is unchanged.
+    'delete match arm \(None, None\) in refine',
+    # lcs_pairs(): the fill guarantees the equal case always took the
+    # diagonal, so the surviving index mutants only change *which* of
+    # several equally long subsequences the backtrack walks — every
+    # choice they can make is optimal. The exhaustive reference-oracle
+    # test pins length and validity, which is the function's whole
+    # contract; a mutant that broke either would be caught by it.
+    'replace \+ with \* in lcs_pairs',
+]
diff --git a/.gitignore b/.gitignore
index 78859c6..bd0028c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,4 @@
 /2607.07987v1.pdf
 /target
 /.hegel
+/mutants.out*
diff --git a/src/check.rs b/src/check.rs
index 7f98feb..79d6e0b 100644
--- a/src/check.rs
+++ b/src/check.rs
@@ -237,6 +237,16 @@ mod tests {
                 .iter()
                 .all(|v| matches!(v, Violation::MissedDeletion { .. }))
         );
+        // And symmetrically when B is the deleting branch (the node
+        // reaches M through A's route).
+        let report = check_json("[1, 2]", "[1, 2]", "[2]", "[1, 2]")?;
+        assert!(!report.violations.is_empty());
+        assert!(
+            report
+                .violations
+                .iter()
+                .all(|v| matches!(v, Violation::MissedDeletion { .. }))
+        );
         Ok(())
     }
 
diff --git a/src/diff.rs b/src/diff.rs
index c34bad8..2fd1301 100644
--- a/src/diff.rs
+++ b/src/diff.rs
@@ -1205,6 +1205,55 @@ mod tests {
         Ok(())
     }
 
+    /// Naive recursive LCS length, the oracle for the DP.
+    fn reference_lcs(xs: &[char], ys: &[char]) -> usize {
+        let (Some((x, x_rest)), Some((y, y_rest))) = (xs.split_first(), ys.split_first()) else {
+            return 0;
+        };
+        if x == y {
+            reference_lcs(x_rest, y_rest).saturating_add(1)
+        } else {
+            reference_lcs(x_rest, ys).max(reference_lcs(xs, y_rest))
+        }
+    }
+
+    /// All strings over {a, b, c} up to `depth` more characters.
+    fn all_strings(prefix: Vec<char>, depth: usize, out: &mut Vec<Vec<char>>) {
+        out.push(prefix.clone());
+        if depth == 0 {
+            return;
+        }
+        for c in ['a', 'b', 'c'] {
+            let mut next = prefix.clone();
+            next.push(c);
+            all_strings(next, depth.saturating_sub(1), out);
+        }
+    }
+
+    #[test]
+    fn lcs_pairs_matches_a_reference_on_all_small_inputs() {
+        // Exhaustive over both sides: the alignment tests alone
+        // under-constrain the DP because phase 3 rescues small cases,
+        // and hand-picked cases let index-arithmetic mutants slip
+        // through the backtrack's compensating paths.
+        let mut strings = Vec::new();
+        all_strings(Vec::new(), 4, &mut strings);
+        for xs in &strings {
+            for ys in &strings {
+                let pairs = lcs_pairs(xs, ys);
+                assert_eq!(pairs.len(), reference_lcs(xs, ys), "LCS({xs:?}, {ys:?})");
+                for (i, j) in &pairs {
+                    assert_eq!(xs.get(*i), ys.get(*j), "LCS({xs:?}, {ys:?})");
+                }
+                for window in pairs.windows(2) {
+                    if let [(i1, j1), (i2, j2)] = window {
+                        assert!(i1 < i2 && j1 < j2, "LCS({xs:?}, {ys:?}) crosses: {pairs:?}");
+                    }
+                }
+            }
+        }
+    }
+
     #[test]
     fn structural_eq_distinguishes_kind_label_and_shape() -> Result<(), Error> {
         // The collision guard in anchor() is unreachable through real