The four conditions are set-membership statements over node maps, and
a relabel is the one edit that changes no membership: a merge that
ignored a rename — of code or a comment — passed the checker, both as
an external judge of other tools and in the pipeline self-check. A
fifth condition compares labels wherever the routes commute: a branch
that relabeled a node must see its label in M (missed relabel), M
must keep O's label when neither branch relabeled it (extra relabel),
and a branch's inserted nodes must arrive with labels verbatim —
otherwise the merge holds a label nobody wrote.

Nodes whose routes disagree are skipped rather than judged: that
disagreement is condition 3's extra deletion, and comparing labels
across unrelated twins (duplicated content splits i1 and i2 across
copies) would misfire.

Assisted-by: Claude Fable 5 via Claude Code

diff --git a/docs/notes/2026-07-14-mergiraf-comparison.md b/docs/notes/2026-07-14-mergiraf-comparison.md
index e649958..96f2063 100644
--- a/docs/notes/2026-07-14-mergiraf-comparison.md
+++ b/docs/notes/2026-07-14-mergiraf-comparison.md
@@ -310,10 +310,15 @@ between the pre- and post-comment builds is
 *silent* comment-dropping merge; the remaining BAD-MERGE is
 `conflicting_method_signatures`, the known signature-composition gap.
 
-Sweeping also surfaced a checker limitation worth its own follow-up:
-`d3j check` cannot see a *dropped relabel* (comment or code — a merge
-that ignores A's rename of `a` to `b` passes). The four universality
-conditions are set-membership statements over node maps; none of them
-compares labels along the routes. The merge pipeline itself conflicts
-correctly via relabel-relabel, but `check` as an external judge of
-other tools' merges is blind to this class.
+Sweeping also surfaced a checker limitation, fixed the same day: `d3j
+check` could not see a *dropped relabel* (comment or code — a merge
+that ignored A's rename of `a` to `b` passed). The four universality
+conditions were set-membership statements over node maps; none of
+them compared labels along the routes. A fifth condition now judges
+labels wherever the routes commute: a branch that relabeled a node
+must see its label in M (missed relabel), M must keep O's label when
+neither branch relabeled (extra relabel), and a branch's inserted
+nodes must arrive with their labels verbatim. The merge pipeline
+already conflicted correctly via relabel-relabel; this closes the
+gap for `check` as an external judge and tightens the pipeline's own
+self-check.
diff --git a/src/bin/d3j/commands/check.rs b/src/bin/d3j/commands/check.rs
index e7d8244..5426057 100644
--- a/src/bin/d3j/commands/check.rs
+++ b/src/bin/d3j/commands/check.rs
@@ -55,16 +55,28 @@ fn witness<'t>(
     violation: &Violation,
 ) -> (&'t Tree, Range<usize>) {
     match violation {
-        Violation::ExtraInsertion { span, .. } => (m, span.clone()),
+        Violation::ExtraInsertion { span, .. } | Violation::ExtraRelabel { span, .. } => {
+            (m, span.clone())
+        }
         Violation::MissedInsertion {
             branch: Branch::A,
             span,
             ..
+        }
+        | Violation::MissedRelabel {
+            branch: Branch::A,
+            span,
+            ..
         } => (a, span.clone()),
         Violation::MissedInsertion {
             branch: Branch::B,
             span,
             ..
+        }
+        | Violation::MissedRelabel {
+            branch: Branch::B,
+            span,
+            ..
         } => (b, span.clone()),
         Violation::ExtraDeletion { span, .. } | Violation::MissedDeletion { span, .. } => {
             (o, span.clone())
diff --git a/src/check.rs b/src/check.rs
index 09fb643..1fb5432 100644
--- a/src/check.rs
+++ b/src/check.rs
@@ -3,8 +3,10 @@
 //! lands, nothing else does.
 //!
 //! Fidelity is bounded by diff quality (the paper carries the same
-//! caveat): the four conditions are set-membership statements over the
-//! diffs f: O→A, g: O→B, i1: A→M, i2: B→M.
+//! caveat): conditions 1–4 are set-membership statements over the
+//! diffs f: O→A, g: O→B, i1: A→M, i2: B→M; condition 5 additionally
+//! compares labels along the routes, since a merge that drops or
+//! invents a relabel is invisible to membership alone.
 
 use std::ops::Range;
 
@@ -37,6 +39,18 @@ pub enum Violation {
 
     #[error("missed deletion: a branch deleted the node at {span:?} but the merge kept it")]
     MissedDeletion { node: NodeId, span: Range<usize> },
+
+    #[error(
+        "missed relabel: branch {branch:?} relabeled the node at {span:?} but the merge kept a different label"
+    )]
+    MissedRelabel {
+        branch: Branch,
+        node: NodeId,
+        span: Range<usize>,
+    },
+
+    #[error("extra relabel: the merge node at {span:?} holds a label neither branch wrote")]
+    ExtraRelabel { node: NodeId, span: Range<usize> },
 }
 
 /// The checker's verdict on one (O, A, B, M) quadruple.
@@ -55,7 +69,7 @@ impl Report {
     }
 }
 
-/// Checks M against the four universality conditions.
+/// Checks M against the five universality conditions.
 pub fn check(o: &Tree, a: &Tree, b: &Tree, m: &Tree) -> Report {
     let f = diff(o, a);
     let g = diff(o, b);
@@ -119,14 +133,91 @@ pub fn check(o: &Tree, a: &Tree, b: &Tree, m: &Tree) -> Report {
         }
     }
 
+    // 5. Relabels land exactly once. Conditions 1–4 are membership
+    //    statements over node maps and never compare labels, so a
+    //    merge that ignored a rename — or invented one — would pass
+    //    them. For every O node reaching M through both routes: a
+    //    branch that relabeled it must see its label in M, and when
+    //    neither branch relabeled it, M must keep O's label.
+    for node in o.nodes() {
+        let (Some(in_a), Some(in_b)) = (f.image(node), g.image(node)) else {
+            continue;
+        };
+        // Broken or disagreeing routes are condition 3's extra
+        // deletion; labels are only judged where the routes commute.
+        let (Some(via_a), Some(via_b)) = (i1.image(in_a), i2.image(in_b)) else {
+            continue;
+        };
+        if via_a != via_b {
+            continue;
+        }
+        let merged = m.label(via_a);
+        let original = o.label(node);
+        let relabeled_a = a.label(in_a) != original;
+        let relabeled_b = b.label(in_b) != original;
+        if relabeled_a && merged != a.label(in_a) {
+            violations.push(Violation::MissedRelabel {
+                branch: Branch::A,
+                node: in_a,
+                span: a.span(in_a),
+            });
+        }
+        if relabeled_b && merged != b.label(in_b) {
+            violations.push(Violation::MissedRelabel {
+                branch: Branch::B,
+                node: in_b,
+                span: b.span(in_b),
+            });
+        }
+        if !relabeled_a && !relabeled_b && merged != original {
+            violations.push(Violation::ExtraRelabel {
+                node: via_a,
+                span: m.span(via_a),
+            });
+        }
+    }
+
+    //    The same for insertions: a branch's inserted node that
+    //    reaches M must arrive with its label intact — otherwise the
+    //    merge holds a label nobody wrote.
+    altered_insertions(a, &f, &i1, m, &mut violations);
+    altered_insertions(b, &g, &i2, m, &mut violations);
+
     Report {
         parsable: true,
         violations,
     }
 }
 
+/// Condition 5 for one branch's insertions: an inserted node's image
+/// in M must carry the inserted label verbatim.
+fn altered_insertions(
+    branch_tree: &Tree,
+    from_o: &Matching,
+    to_m: &Matching,
+    m: &Tree,
+    violations: &mut Vec<Violation>,
+) {
+    for node in branch_tree.nodes() {
+        if from_o.preimage(node).is_some() {
+            continue;
+        }
+        let Some(in_m) = to_m.image(node) else {
+            continue; // Condition 2's missed insertion, not a relabel.
+        };
+        if m.label(in_m) != branch_tree.label(node) {
+            violations.push(Violation::ExtraRelabel {
+                node: in_m,
+                span: m.span(in_m),
+            });
+        }
+    }
+}
+
 /// Anonymous tokens under a commutative parent are fungible
-/// separators, exempt from all four conditions. A cross-branch union
+/// separators, exempt from the membership conditions (the label
+/// condition is vacuous for them — anonymous nodes carry no label).
+/// A cross-branch union
 /// merge makes their attribution ambiguous — both branches' commas
 /// legitimately claim the same merged comma, orphaning its twin — and
 /// the parse itself (verified before the conditions run) already pins
@@ -276,6 +367,149 @@ mod tests {
         Ok(())
     }
 
+    #[test]
+    fn a_dropped_relabel_is_flagged() -> Result<(), Error> {
+        // A renames 1 to 2; a merge that keeps 1 used to pass — the
+        // membership conditions never compare labels.
+        let report = check_json("[1]", "[2]", "[1]", "[1]")?;
+        assert!(report.violations.iter().any(|v| matches!(
+            v,
+            Violation::MissedRelabel {
+                branch: Branch::A,
+                ..
+            }
+        )));
+        // The witness is A's new label.
+        let a = parse_json("[2]")?;
+        assert!(report.violations.iter().any(|v| match v {
+            Violation::MissedRelabel { span, .. } => a.source_slice(span.clone()) == Some("2"),
+            _ => false,
+        }));
+        // The merge that lands the rename passes.
+        let report = check_json("[1]", "[2]", "[1]", "[2]")?;
+        assert!(report.is_correct());
+        Ok(())
+    }
+
+    #[test]
+    fn a_dropped_relabel_is_flagged_for_branch_b() -> Result<(), Error> {
+        let report = check_json("[1]", "[1]", "[2]", "[1]")?;
+        assert!(report.violations.iter().any(|v| matches!(
+            v,
+            Violation::MissedRelabel {
+                branch: Branch::B,
+                ..
+            }
+        )));
+        Ok(())
+    }
+
+    #[test]
+    fn a_dropped_comment_edit_is_flagged() -> Result<(), Error> {
+        // The comment-nodes probe: A rewrites a comment, the candidate
+        // merge keeps the old text.
+        let lang = Lang::by_name("rust").ok_or(Error::UnknownLanguage {
+            path: "rust".into(),
+        })?;
+        let o = Tree::parse("// old\nfn f() {}", lang)?;
+        let a = Tree::parse("// new\nfn f() {}", lang)?;
+        let b = Tree::parse("// old\nfn f() {}", lang)?;
+        let m = Tree::parse("// old\nfn f() {}", lang)?;
+        let report = check(&o, &a, &b, &m);
+        assert!(report.violations.iter().any(|v| matches!(
+            v,
+            Violation::MissedRelabel {
+                branch: Branch::A,
+                ..
+            }
+        )));
+        Ok(())
+    }
+
+    #[test]
+    fn an_invented_relabel_is_flagged() -> Result<(), Error> {
+        // Nobody renamed 1, but the merge holds 9: condition 1 passes
+        // (the 9 has a preimage via the relabel matching), so only a
+        // label comparison catches it.
+        let report = check_json("[1]", "[1]", "[1]", "[9]")?;
+        assert!(!report.violations.is_empty());
+        let m = parse_json("[9]")?;
+        assert!(report.violations.iter().any(|v| match v {
+            Violation::ExtraRelabel { span, .. } => m.source_slice(span.clone()) == Some("9"),
+            _ => false,
+        }));
+        Ok(())
+    }
+
+    #[test]
+    fn an_altered_insertion_is_flagged() -> Result<(), Error> {
+        // A inserted 2; the merge holds 3 where the insertion landed —
+        // a label nobody wrote, on a node with no O preimage.
+        let report = check_json("[1]", "[1, 2]", "[1]", "[1, 3]")?;
+        assert!(
+            report
+                .violations
+                .iter()
+                .any(|v| matches!(v, Violation::ExtraRelabel { .. })),
+            "{:?}",
+            report.violations
+        );
+        // The faithful merge passes.
+        let report = check_json("[1]", "[1, 2]", "[1]", "[1, 2]")?;
+        assert!(report.is_correct());
+        Ok(())
+    }
+
+    #[test]
+    fn concurrent_distinct_relabels_flag_whichever_side_lost() -> Result<(), Error> {
+        // A and B rename 1 differently; no M satisfies both, so the
+        // checker must reject either resolution.
+        let report = check_json("[1]", "[2]", "[3]", "[2]")?;
+        assert!(report.violations.iter().any(|v| matches!(
+            v,
+            Violation::MissedRelabel {
+                branch: Branch::B,
+                ..
+            }
+        )));
+        let report = check_json("[1]", "[2]", "[3]", "[3]")?;
+        assert!(report.violations.iter().any(|v| matches!(
+            v,
+            Violation::MissedRelabel {
+                branch: Branch::A,
+                ..
+            }
+        )));
+        // The identical rename made twice passes with the new label.
+        let report = check_json("[1]", "[2]", "[2]", "[2]")?;
+        assert!(report.is_correct());
+        Ok(())
+    }
+
+    #[test]
+    fn routes_that_disagree_are_not_judged_for_labels() -> Result<(), Error> {
+        // O's 8 reaches M through both routes, but they land on
+        // different twins: i1 pairs A's 8 with the first (greedy LCS),
+        // while B's 0 anchors uniquely and drags i2's 8 to the third
+        // element. Condition 3 owns that disagreement (extra
+        // deletion); condition 5 must skip the node rather than
+        // compare labels across unrelated twins.
+        let report = check_json("[8]", "[8]", "[0, 8]", "[8, 0, 8]")?;
+        assert!(
+            report
+                .violations
+                .iter()
+                .any(|v| matches!(v, Violation::ExtraDeletion { .. })),
+            "{:?}",
+            report.violations
+        );
+        assert!(report.violations.iter().all(|v| !matches!(
+            v,
+            Violation::MissedRelabel { .. } | Violation::ExtraRelabel { .. }
+        )));
+        Ok(())
+    }
+
     #[test]
     fn a_universal_merge_passes() -> Result<(), Error> {
         // The paper's Figures 2/3: disjoint edits, including B's 2→6
diff --git a/src/merge.rs b/src/merge.rs
index 3e69d21..2d63f0e 100644
--- a/src/merge.rs
+++ b/src/merge.rs
@@ -172,14 +172,26 @@ fn merge_to_text_with(
                         branch: crate::check::Branch::A,
                         span,
                         ..
+                    }
+                    | Violation::MissedRelabel {
+                        branch: crate::check::Branch::A,
+                        span,
+                        ..
                     } => (None, Some(span.clone()), None),
                     Violation::MissedInsertion {
                         branch: crate::check::Branch::B,
                         span,
                         ..
+                    }
+                    | Violation::MissedRelabel {
+                        branch: crate::check::Branch::B,
+                        span,
+                        ..
                     } => (None, None, Some(span.clone())),
                     // The witness lives in M, which has no span slot.
-                    Violation::ExtraInsertion { .. } => (None, None, None),
+                    Violation::ExtraInsertion { .. } | Violation::ExtraRelabel { .. } => {
+                        (None, None, None)
+                    }
                 };
                 Conflict {
                     span_o,