diff --git a/src/ccl/ccl_utils.rs b/src/ccl/ccl_utils.rs
index 765b602b..17538341 100644
--- a/src/ccl/ccl_utils.rs
+++ b/src/ccl/ccl_utils.rs
@@ -1287,13 +1287,22 @@ impl<C: PartialEq + Clone> PredMemo<C> {
                 }
                 None => {
                     let keepalive = Rc::clone(&refinement.predicate);
-                    let copy = (*refinement.predicate).clone();
+                    // Copy-on-write, not duplication: the rebuilt term is
+                    // installed *in place of* the original, so it is the same
+                    // logical node at a new allocation and keeps its ids.
+                    let copy = refinement.predicate.clone_preserving_ids();
                     let rev = store.revision;
                     (copy, keepalive, rev)
                 }
             }
         };
-        let reported = f(&mut pred);
+        // The rebuild runs id-preserving, covering the rewrite as well as the
+        // copy-on-write above (a substitution firing inside a predicate
+        // materializes its template here). Nothing records a predicate rewrite,
+        // so an id minted here is one no record explains; preserving is honest
+        // because the rebuilt term *replaces* the original everywhere this walk
+        // reaches.
+        let reported = crate::ccl::lineage::preserving_ids(|| f(&mut pred));
         let mut store = self.0.borrow_mut();
         let changed = reported || store.revision != before;
         let installed = if changed {
@@ -1329,8 +1338,10 @@ impl TermMemo {
     /// caller) still leaves the occurrence rebuilt and recorded.
     pub fn rebuild_always(&self, refinement: &mut Refinement, f: impl FnOnce(&mut Expr)) {
         let keepalive = Rc::clone(&refinement.predicate);
-        let mut pred = (*refinement.predicate).clone();
-        f(&mut pred);
+        // Copy-on-write; see `rebuild`.
+        let mut pred = refinement.predicate.clone_preserving_ids();
+        // Id-preserving; see `rebuild`.
+        crate::ccl::lineage::preserving_ids(|| f(&mut pred));
         let mut store = self.0.0.borrow_mut();
         let shared = store
             .entries
diff --git a/src/ccl/channelize.rs b/src/ccl/channelize.rs
index e57b766b..6a664063 100644
--- a/src/ccl/channelize.rs
+++ b/src/ccl/channelize.rs
@@ -267,7 +267,38 @@ fn try_extract_fanout_feed(body: &Expr, defer_name: &Name) -> Option<Vec<(Expr,
     any_feed.then_some(arms)
 }
 
-/// Attempt to apply the defer-returning lift to a `Let` binding.
+/// The defer-returning lift's output.
+struct DeferLift {
+    /// `let y = Defer in …` — the two defer scopes merged into one.
+    expr: Expr,
+    /// The inner defer binder, which the lift renamed to the outer name.
+    inner_name: Name,
+    /// The channel domain of the inner handle the lift replaced, when its type
+    /// records one.
+    inner_chan_dom: Option<(Name, crate::ccl::ChanLevel)>,
+}
+
+/// Whether `bound_expr` has the defer-returning lift's shape: any `ExprStmt`
+/// prefix, then `let x = Defer in body_x` with `body_x` defer-returning.
+///
+/// [`lift_defer`] consumes its input, so the shape is decided here first. A
+/// matcher that failed partway through would have to rebuild what it had already
+/// taken apart, or work on a copy.
+fn is_lift_shape(bound_expr: &Expr) -> bool {
+    let mut current = bound_expr;
+    while let TypedExprNode::ExprStmt { body, .. } = &current.node {
+        current = body;
+    }
+    matches!(
+        &current.node,
+        TypedExprNode::Let { binding, bound_expr: inner_be, body }
+            if matches!(inner_be.node, TypedExprNode::Defer)
+                && is_defer_returning(body, &binding.name)
+    )
+}
+
+/// Apply the defer-returning lift to a `Let` binding whose `bound_expr` has
+/// passed [`is_lift_shape`].
 ///
 /// Pattern: `let y = (let x = Defer in body_x) in body_y` where
 /// `body_x` is *defer-returning* (ends in `Var(x)` after walking
@@ -282,11 +313,10 @@ fn try_extract_fanout_feed(body: &Expr, defer_name: &Name) -> Option<Vec<(Expr,
 /// Also handles an optional `ExprStmt` prefix on `bound_expr`: the
 /// heads of any leading ExprStmts become a prefix that's prepended to
 /// the lifted body, with stale Feed/Define target names renamed to `y`.
-fn try_lift_defer(binding_name: &Name, bound_expr: &Expr, body: &Expr) -> Option<(Expr, Name)> {
+fn lift_defer(binding_name: &Name, bound_expr: Expr, body: &Expr) -> DeferLift {
     let mut prefix: Vec<Expr> = Vec::new();
-    let mut current = bound_expr.clone();
+    let mut current = bound_expr;
     loop {
-        let cur_id = current.node_id;
         match current.node {
             TypedExprNode::ExprStmt {
                 expr: head,
@@ -295,34 +325,39 @@ fn try_lift_defer(binding_name: &Name, bound_expr: &Expr, body: &Expr) -> Option
                 prefix.push(*head);
                 current = *tail;
             }
+            // Put the node back on the expression the match moved it out of; the
+            // spine ends here.
             node => {
-                current = TypedExpr {
-                    node,
-                    ty: current.ty,
-                    user_annotation: current.user_annotation,
-                    // TODO(preserve): hand-rolled preserve — fold into `Expr::preserve`.
-                    node_id: cur_id,
-                };
+                current.node = node;
                 break;
             }
         }
     }
-    let (inner_name, inner_handle_ty, inner_body_x) = match current.node {
-        TypedExprNode::Let {
-            binding: inner_binding,
-            bound_expr: inner_be,
-            body: inner_body,
-        } if matches!(inner_be.node, TypedExprNode::Defer)
-            && is_defer_returning(&inner_body, &inner_binding.name) =>
-        {
-            // Keep the inner defer's recorded handle type (`feed(ChanDom(F) ⇒
-            // V)`) — the lifted binding must carry it so cluster discovery
-            // keys the channel by the domain name consumer types reference,
-            // not by the term name. (`Hole` on an untyped tree, harmlessly.)
-            (inner_binding.name, inner_be.ty, *inner_body)
-        }
-        _ => return None,
+    let TypedExprNode::Let {
+        binding: inner_binding,
+        bound_expr: inner_be,
+        body: inner_body,
+    } = current.node
+    else {
+        unreachable!("`lift_defer` requires the `is_lift_shape` shape")
     };
+    debug_assert!(
+        matches!(inner_be.node, TypedExprNode::Defer)
+            && is_defer_returning(&inner_body, &inner_binding.name),
+        "`lift_defer` requires the spine to end in `let x = Defer in body_x` with a \
+         defer-returning `body_x` — check `is_lift_shape` first"
+    );
+    // Read the inner handle's channel domain off the binding this lift replaces:
+    // the entry the caller records has to key on the domain name consumer types
+    // carry, which for a specialization clone differs from the term binder name.
+    let inner_chan_dom =
+        handle_chan_dom(&inner_binding.ty).or_else(|| handle_chan_dom(&inner_be.ty));
+    // Keep the inner defer's recorded handle type (`feed(ChanDom(F) ⇒ V)`) — the
+    // lifted binding must carry it so cluster discovery keys the channel by the
+    // domain name consumer types reference, not by the term name. (`Hole` on an
+    // untyped tree, harmlessly.)
+    let (inner_name, inner_handle_ty, inner_body_x) =
+        (inner_binding.name, inner_be.ty, *inner_body);
 
     // `body_x[x → y]` — also renames Feed/Define targets named `x` to `y`.
     let inner_subst = desugar_rename(inner_body_x, &inner_name, binding_name);
@@ -370,7 +405,11 @@ fn try_lift_defer(binding_name: &Name, bound_expr: &Expr, body: &Expr) -> Option
     defer_node.ty = inner_handle_ty;
     let mut lifted = Expr::let_bind(binding_name, defer_node, spliced);
     lifted.ty = out_ty;
-    Some((lifted, inner_name))
+    DeferLift {
+        expr: lifted,
+        inner_name,
+        inner_chan_dom,
+    }
 }
 
 /// Return `true` if `expr` ends in `Var(name)` after walking through
@@ -577,30 +616,6 @@ fn handle_chan_dom(ty: &Type) -> Option<(Name, crate::ccl::ChanLevel)> {
     }
 }
 
-/// Locate the `let <term> = Defer` binding inside `expr` and read its handle's
-/// channel-domain name ([`handle_chan_dom`], off the binding slot or the
-/// `Defer` node itself). Used by the defer-returning lift to key its alias
-/// entry by the name consumer types carry.
-fn find_defer_chan_dom(expr: &Expr, term: &Name) -> Option<(Name, crate::ccl::ChanLevel)> {
-    if let TypedExprNode::Let {
-        binding,
-        bound_expr,
-        ..
-    } = &expr.node
-        && binding.name == *term
-        && matches!(bound_expr.node, TypedExprNode::Defer)
-    {
-        return handle_chan_dom(&binding.ty).or_else(|| handle_chan_dom(&bound_expr.ty));
-    }
-    let mut found = None;
-    expr.walk_children(|c| {
-        if found.is_none() {
-            found = find_defer_chan_dom(c, term);
-        }
-    });
-    found
-}
-
 /// the channel domain carried by an assembled channel's
 /// type — the domain of its constructed `Fun`, or, for an alias channel that
 /// is itself a defer read (`x <<= y` leaves `Var(y) : feed(…)`), the read's
@@ -744,7 +759,10 @@ fn erase_chan_domains(expr: &mut Expr, map: &mut HashMap<Name, Type>) {
         erase_chan_domains(bound_expr, map);
         erase_chan_domains(body, map);
         // §6.2 Let-closing on the substitution content (see fn docs).
-        let discharge = crate::ccl::subst::Subst::discharge(&binding.name, (**bound_expr).clone());
+        // A discharge template is not a tree node: it is cloned again at every
+        // read, and that read is where the sibling is minted.
+        let discharge =
+            crate::ccl::subst::Subst::discharge(&binding.name, bound_expr.clone_preserving_ids());
         for dom in map.values_mut() {
             *dom = discharge.apply_type(dom);
         }
@@ -1215,7 +1233,11 @@ fn desugar_inner(expr: Expr, ctx: &mut DesugarCtx) -> Result<Expr, DeferError> {
             // functions: `let y = f(arg)` where f's body is `let x =
             // Defer in x` inlines to `let y = (let x = Defer in x) in
             // body_y`, and the lift collapses the two scopes.
-            if let Some((lifted, inner_name)) = try_lift_defer(&binding.name, &bound_expr, &body) {
+            if is_lift_shape(&bound_expr) {
+                // Read before the lift consumes the binding.
+                let (outer, lvl) = handle_chan_dom(&binding.ty)
+                    .unwrap_or_else(|| (binding.name.clone(), crate::ccl::ChanLevel(0)));
+                let lift = lift_defer(&binding.name, *bound_expr, &body);
                 // The lift renames the inner defer binder to the outer name,
                 // but *consumer types outside the lifted subtree* may carry
                 // the inner handle's rigid `ChanDom`. Record the alias so the
@@ -1226,22 +1248,21 @@ fn desugar_inner(expr: Expr, ctx: &mut DesugarCtx) -> Result<Expr, DeferError> {
                 // is per-instantiation, freshened at `specialize_use`), and
                 // post-freshening the two scopes usually already share one
                 // name, in which case no entry is needed. Term names are the
-                // fallback for handles the walk cannot locate.
-                let inner_key = find_defer_chan_dom(&bound_expr, &inner_name)
+                // fallback for handles whose type records no domain.
+                let inner_key = lift
+                    .inner_chan_dom
                     .map(|(n, _)| n)
-                    .unwrap_or_else(|| inner_name.clone());
-                let (outer, lvl) = handle_chan_dom(&binding.ty)
-                    .unwrap_or_else(|| (binding.name.clone(), crate::ccl::ChanLevel(0)));
+                    .unwrap_or(lift.inner_name);
                 if inner_key != outer {
                     ctx.resolved_domains
                         .push((inner_key, Type::ChanDom(outer, lvl)));
                 }
-                return desugar(lifted, ctx);
+                return desugar(lift.expr, ctx);
             }
             // Let-of-defer-returning-let collapse: `let y = (let z =
             // E in Var(z)) in body_y` is equivalent to `let z = E in
             // body_y[y → z]`.  Surfaces a deeper `Defer` (inside E)
-            // so the outer try_lift_defer can fire on a subsequent
+            // so the outer defer lift can fire on a subsequent
             // pass.  Triggered by nested UDF inlines whose ANF
             // introduced an intermediate alias.
             if let TypedExprNode::Let {
@@ -1289,7 +1310,7 @@ fn desugar_inner(expr: Expr, ctx: &mut DesugarCtx) -> Result<Expr, DeferError> {
             // alias handle must never reach here; a survivor would silently
             // mis-route `Feed(y, …)` to the wrong handle. Assert that loudly in
             // debug rather than re-implementing the collapse. (The defer-*returning*
-            // lifts above — `try_lift_defer` / the collapse — survive `inline`
+            // lifts above — `lift_defer` / the collapse — survive `inline`
             // because their bound-expr is a `let`, not a bare `Var`.)
             #[cfg(debug_assertions)]
             {
@@ -2120,7 +2141,9 @@ fn extract_for_defer_impl(
                     let mut fvs = HashSet::new();
                     collect_free_vars(feed, &mut fvs);
                     if fvs.contains(&binding.name) {
-                        let placeholder = Expr::new(TypedExprNode::Lit(Lit::Unit));
+                        // A `mem::take` slot, overwritten below: minting for it
+                        // would log a birth for a node no tree ever holds.
+                        let placeholder = Expr::throwaway(TypedExprNode::Lit(Lit::Unit));
                         let original = std::mem::replace(feed, placeholder);
                         // stamp the wrap at construction —
                         // the let's type is its body's, closed over the binder
@@ -2725,7 +2748,7 @@ mod tests {
 
     /// The lifted-prefix spine is typed, not `Hole`.
     ///
-    /// `try_lift_defer` rebuilds the prefix onto the lifted body with
+    /// [`lift_defer`] rebuilds the prefix onto the lifted body with
     /// `Expr::expr_stmt`, which carries the body's type — an `ExprStmt`'s type
     /// *is* its body's. That constructor used to leave `Type::Hole` here, and
     /// `Hole` is [`has_type_residue`], so an escaping one is exactly what
@@ -2749,9 +2772,9 @@ mod tests {
         let bound_expr = Expr::expr_stmt(Expr::feed("x", lit(1)), inner);
         let body = var("y").with_ty(int.clone());
 
-        let (lifted, inner_name) =
-            try_lift_defer(&Name::raw("y"), &bound_expr, &body).expect("the lift shape matches");
-        assert_eq!(inner_name, Name::raw("x"));
+        assert!(is_lift_shape(&bound_expr), "the fixture has the lift shape");
+        let lift = lift_defer(&Name::raw("y"), bound_expr, &body);
+        assert_eq!(lift.inner_name, Name::raw("x"));
 
         // Every `ExprStmt` on the spine carries a type. Checking for the absence
         // of `Hole` rather than for equality with `int` keeps this honest if the
@@ -2766,7 +2789,7 @@ mod tests {
             }
             e.walk_children(assert_spine_typed);
         }
-        assert_spine_typed(&lifted);
+        assert_spine_typed(&lift.expr);
     }
 
     #[test]
diff --git a/src/ccl/context.rs b/src/ccl/context.rs
index f32d1b5f..9326874d 100644
--- a/src/ccl/context.rs
+++ b/src/ccl/context.rs
@@ -576,16 +576,40 @@ impl CompiledProgram {
     }
 }
 
-/// Every main-tree node id reachable in `expr` (the `walk_children` node set,
-/// refinement-predicate interiors excluded — the domain the lineage steps and
-/// the pane projections reason about).
+/// Every node id reachable in `expr`: the `walk_children` node set plus the
+/// interiors of every refinement predicate riding a type slot — the id domain the
+/// lineage steps and the pane projections must explain.
+///
+/// Deliberately wider than `assert_unique_node_ids`, which walks children only.
+/// Explanation and uniqueness are two questions with two answers; see
+/// `design/provenance.md`, "Walking the ids".
 pub(crate) fn collect_tree_ids(expr: &Expr) -> std::collections::HashSet<NodeId> {
-    fn go(e: &Expr, acc: &mut std::collections::HashSet<NodeId>) {
+    use crate::ccl::TypedExprNode;
+    use crate::ccl::ty::Type;
+
+    fn from_ty(t: &Type, acc: &mut std::collections::HashSet<NodeId>) {
+        if let Type::Refinement(_, r) = t {
+            from_expr(&r.predicate, acc);
+        }
+        t.walk_children(|c| from_ty(c, acc));
+    }
+
+    fn from_expr(e: &Expr, acc: &mut std::collections::HashSet<NodeId>) {
         acc.insert(e.node_id());
-        e.walk_children(|c| go(c, acc));
+        from_ty(&e.ty, acc);
+        if let Some(ann) = &e.user_annotation {
+            from_ty(ann, acc);
+        }
+        // A `Cast`'s target is a type slot `walk_children` skips, and it is where
+        // lowering parks the predicate it just built.
+        if let TypedExprNode::Cast { target, .. } = &e.node {
+            from_ty(target, acc);
+        }
+        e.walk_children(|c| from_expr(c, acc));
     }
+
     let mut acc = std::collections::HashSet::new();
-    go(expr, &mut acc);
+    from_expr(expr, &mut acc);
     acc
 }
 
@@ -788,7 +812,12 @@ pub fn compile_program(
     // `infer` mutates `expr` in place. This is the source-shaped, pre-mono,
     // still-hole-typed tree. Its ids resolve against the `lowering_projection`
     // (the pre-mono originals). See `CompiledProgram::pre_inference_ir`.
-    let pre_inference_ir = expr.clone();
+    // A pane snapshot: the same nodes as the live tree, observed at a point in
+    // time, so it preserves ids. A freshening clone would hand the boundary a
+    // structurally identical program sharing no identity with the one it is meant
+    // to snapshot, and these ids must resolve against the `lowering_projection`,
+    // which is keyed by the originals.
+    let pre_inference_ir = expr.clone_preserving_ids();
 
     // Register every source (pre-registered + discovered during lowering) with
     // inference and operator-conversion now that the full source set is known.
@@ -883,9 +912,11 @@ pub fn compile_program(
     // not run). `ast` (`join_planned`) is the *wrong* tree for a source
     // view — `lambda_elim`/`planning` re-mint ids and produce execution shape.
     // See `CompiledProgram::post_inference_ir`.
-    let post_inference_ir = expr.clone();
+    // A pane snapshot; see `pre_inference_ir`.
+    let post_inference_ir = expr.clone_preserving_ids();
 
     expr = inline::inline_capability_lambdas(expr);
+    assert_unique_node_ids(&expr, "post-inline");
     debug!("UDFs inlined CCL:\n{}", symbolic(&expr));
     check_pre_desugar(&expr).map_err(|errs| {
         if errs
@@ -939,6 +970,7 @@ pub fn compile_program(
         .map_err(|msg| vec![CompileError::Unsupported(msg)])?;
     expr = transact_phase::run(expr, &txn_mut_vars)
         .map_err(|msg| vec![CompileError::Unsupported(msg)])?;
+    assert_unique_node_ids(&expr, "post-transact");
     debug!("Transact phase CCL:\n{}", symbolic(&expr));
     check_pre_desugar(&expr).expect("transact phase produced an inconsistent tree");
 
@@ -951,6 +983,7 @@ pub fn compile_program(
     // The tree still carries Defer/Feed here, so the walls are the relaxed
     // pre-desugar check.
     let phase_out = mut_elim::run(expr);
+    assert_unique_node_ids(&phase_out, "post-letrec-run");
     debug!("Letrec phase CCL:\n{}", symbolic(&phase_out));
     check_pre_desugar(&phase_out).expect("letrec phase produced an inconsistent tree");
 
@@ -965,6 +998,7 @@ pub fn compile_program(
     // channel domains by substitution; the strict `typecheck` below is the
     // release-visible enforcement.
     let mut desugared = channelize::run(phase_out).errs()?;
+    assert_unique_node_ids(&desugared, "post-desugar");
     debug!("Channelized:\n{}", symbolic(&desugared));
     typecheck(&desugared).expect("channelize produced an ill-typed tree");
 
@@ -972,7 +1006,8 @@ pub fn compile_program(
     // post-inference desugar order this snapshot is *downstream* of
     // `post_inference_ir` (post-inline/transact/letrec/channelize); see the doc
     // comment on `post_desugar_ir`.
-    let post_desugar_ir = desugared.clone();
+    // A pane snapshot; see `pre_inference_ir`.
+    let post_desugar_ir = desugared.clone_preserving_ids();
 
     // Fed-out mutable variable reads: rewrite a read-only reply that reads a mutable variable out of
     // its block into an outer-indexed as-of join (an as-of read at the reading
@@ -983,9 +1018,11 @@ pub fn compile_program(
     // `transact_phase::rewrite_as_of_reads`.
     transact_phase::rewrite_as_of_reads(&mut desugared)
         .map_err(|msg| vec![CompileError::Unsupported(msg)])?;
+    assert_unique_node_ids(&desugared, "post-as-of-read");
     typecheck(&desugared).expect("as-of-read rewrite produced an ill-typed tree");
 
     let lambda_elim = lambda_elim::run(desugared).errs()?;
+    assert_unique_node_ids(&lambda_elim, "post-lambda-elim");
     debug!("λ-eliminated CCL:\n{}", symbolic(&lambda_elim));
     debug!("λ-eliminated typed CCL:\n{}", symbolic_typed(&lambda_elim));
 
@@ -1006,6 +1043,7 @@ pub fn compile_program(
     typecheck(&recognized).expect("letrec recognition produced an ill-typed tree");
 
     let join_planned = planning::run(recognized);
+    assert_unique_node_ids(&join_planned, "post-planning");
     debug!(
         "Join-planned CCL:\n{} : {}",
         symbolic(&join_planned),
diff --git a/src/ccl/design/provenance.md b/src/ccl/design/provenance.md
index 1b695a2f..6fce36ba 100644
--- a/src/ccl/design/provenance.md
+++ b/src/ccl/design/provenance.md
@@ -6,6 +6,11 @@ at lowering, monomorphization cloning subtrees, inline fanning UDF bodies out,
 channelize rewriting defers, lambda-elim synthesizing combinators, planning
 fusing clauses).
 
+A **pane** is a snapshot of the AST at one point in compilation. `CompiledProgram` retains three —
+`pre_inference_ir`, `post_inference_ir`, `post_desugar_ir` — and the inspector renders each in one
+UI pane, which is where the name comes from. **Below** a pane means later in the pipeline, on a more
+lowered tree; it is not tree depth and not a layering.
+
 **Status markers.** The substrate — the identity primitives, the lineage model,
 the recorder, and the always-on lowering projection — is in tree. Everything a
 **Planned** marker introduces is designed but not yet built: the passes' adoption
@@ -13,63 +18,146 @@ of the recorder, the pane-boundary folds, and the inspector's consumption of
 them. A reader on `main` can tell the two apart by the marker alone; unmarked
 prose describes code you can go read.
 
-> The design of record — the full decision log, the collapse algorithm, the
-> recorder mechanism, and the adoption sequencing — is the lineage-redesign doc
-> under projects/program-inspector in the internal vault. This file summarizes
-> the shipped shape; where the two disagree, that doc wins.
-
-## The two identity primitives (`src/ccl/provenance.rs`)
-
-- **`NodeId`** — a `Copy` newtype giving each IR expression node a stable,
-  never-reused identity (its own atomic counter, distinct from `Uid`). It rides
-  inline on `TypedExpr`, whose hand-written `PartialEq` **skips it**: provenance
-  is metadata, not part of a node's value, so two structurally-equal nodes stay
-  equal even with distinct ids — which the passes' structural-equality checks
-  depend on. (Nodes are never hashed by value: `TypedExpr` has no `Hash` impl.
-  `NodeId` itself is `Hash`/`Ord`, as a map key.) `NodeId::PLACEHOLDER` is the reserved sentinel for
-  `Default`/`mem::take` throwaways (ignored by the recorder; `assert_unique_node_ids`
-  backstops that it never persists into a checked tree).
-- **`Pass`** — the compiler stage that produced/rewrote a node (`Lower`,
-  `Uniquify`, `Inline`, `Desugar`, `Transact`, `Letrec`, `Mono`, `LambdaElim`,
-  `Planning`). It lives in the lineage *data* (each step's `via`), never in a
-  type.
-
-### The id domain
-
-**The main tree, and nothing else.** A `NodeId` lives on the `walk_children`
-node-set. A `Type` carries no identity — the only `NodeId`s reachable *through* a
-type are the `TypedExpr`s inside a `Refinement.predicate`, and those are outside
-the domain: duplication does not freshen them, and no walk that matters
-enumerates them. `assert_unique_node_ids` excludes predicates deliberately (a
-predicate-inclusive walk would false-fire on inline's blind spot); the fold's
-leak classes and every `SourceProjection` enumerate from `collect_tree_ids`; the
-remaining predicate-interior readers key on `PredicateId` (transient pointer
-identity) or `Name`. So predicate-interior ids are *carried*, never *checked*, and
-a duplicated subtree's predicate interior may alias its source's ids. Freshening
-them would be write-only, and it splits predicate `Rc` sharing — planning's
-compile memo is `Rc`-keyed, so a split predicate is compiled once per copy. The
-rule cuts the other way too, and usefully: because predicate-interior ids are
-unread, a duplication path is free to *share* a predicate `Rc` with its source
-rather than rebuild one, with no identity consequence to weigh (see
-`design/type-inference.md`, "Sharing is an invariant, not an optimization
-detail").
-
-`uniquify::collect_node_ids` is the one predicate-inclusive walk, and is not a
-counterexample: it is a debug tripwire on uniquify itself, asserting **multiset
-preservation** over the nodes `Uniquifier::expr` visits — uniquify *rebuilds*
-predicate terms through a `PredMemo`, which is exactly where ids could be dropped
-or re-minted. It checks preservation, not uniqueness, and deliberately does not
-dedup by `PredicateId`.
-
-The cost, accepted: an inference error blamed on a predicate-interior node
-resolves to no span (the guard of `[x for x in xs if x > "a"]` reports without a
-caret) because the id is not in the lowering projection. Fixing that means
-seeding predicate-position nodes into the fold as live roots and making
-`output_ids` predicate-inclusive — deferred; see the lineage-redesign doc's
-decisions 16-17. Sharing ids with the main tree is *not* a fix: lowering already
-shares a few incidentally (`pred_sources = gen_sources.clone()`), but the nodes
-actually blamed for guard errors are minted fresh in predicate position and have
-no main-tree twin.
+> This file is the reference for the shipped shape and wins on what the code
+> does. The decision log behind it — the rejected alternatives, the measurements,
+> and the adoption sequencing — is the `lineage-design` note under
+> projects/program-inspector in the internal vault.
+
+## Node identity (`src/ccl/provenance.rs`)
+
+**`NodeId`** is a `Copy` newtype giving each IR expression node an identity: stable, never reused,
+and off its own atomic counter. It rides inline on `TypedExpr`. Lineage and source attribution are
+both keyed by it, which is what lets an inference error on a node minted three passes ago resolve to
+the source span the user wrote. It is distinct from `Uid` because `Uid` identifies binders and a
+`NodeId` identifies expression nodes.
+
+A node is **live** when it is reachable from the expression tree a pass hands on — the node set
+`walk_children` enumerates, called the **main tree** throughout this doc. A refinement predicate is
+a term hanging off a *type* slot, so its nodes are reachable from the tree without being in it; the
+distinction is what the two walks below split on.
+
+Four properties define a `NodeId`.
+
+- **It is not part of a node's value.** `TypedExpr`'s hand-written `PartialEq` skips `node_id`, so
+  two structurally-equal nodes compare equal with distinct ids, which the passes'
+  structural-equality checks depend on. Nodes are never hashed by value: `TypedExpr` has no `Hash`
+  impl. `NodeId` itself is `Hash`/`Ord`, as a map key.
+- **Two live nodes never share one.** This is what makes an id an identity rather than a label. Two
+  nodes at one id collapse to a single entry in every `NodeId`-keyed walk, and give the
+  `SourceProjection` — the `NodeId → SourceAttribution` map the lineage fold produces
+  ([The collapse](#the-collapse)) — one attribution for two nodes.
+- **Construction and copying both mint.** `Expr::new` mints, and `Clone` mints for every node it
+  copies. A call site duplicating a subtree gets distinct identities without asking for them, so no
+  site has to work out which of its copies is the survivor — reaching a shared id takes writing one
+  through a named primitive ([Duplication](#duplication)).
+- **Uniqueness is asserted on the main tree only.** `assert_unique_node_ids` walks children and
+  stops there, so predicate interiors are outside the uniqueness walk.
+
+`NodeId::PLACEHOLDER` is the reserved sentinel for `Default`/`mem::take` throwaways. The recorder —
+the ambient session that logs every mint and copy ([The recorder](#the-recorder)) — ignores it, and
+`assert_unique_node_ids` backstops that it never persists into a checked tree.
+
+### Maintaining uniqueness
+
+`Clone` freshens: it mints a new `NodeId` for every node it copies and reports each `(origin,
+fresh)` pair through `on_copy`, the recorder's copy hook. The alternative is a call site that
+decides — keep the id here, freshen there — and a site that decides wrong puts two nodes on one id,
+which surfaces at a boundary assert far from the site, if at all. Freshening removes the decision
+rather than answering it.
+
+`assert_unique_node_ids` enforces uniqueness at every pass boundary in `compile_program`:
+post-lowering, -inline, -transact, -letrec-run, -desugar, -as-of-read, -lambda-elim, -planning,
+gated on `cfg!(any(debug_assertions, test))`. The walk is `O(nodes)` per boundary and compiles out
+of a release build, along with the leak checks (`assert_leaks_clean` is gated the same way, so
+nothing enforces either property in release). The lineage fold that produces the release-critical
+projection — [The collapse](#the-collapse) — stays always-on. A boundary check states a property of
+the tree rather than of the pass that produced it, so reordering the passes leaves the checks where
+they are and still bounds every pass between two of them. A clean run is therefore evidence about
+the boundaries, not about any individual pass.
+
+### Walking the ids
+
+Three walks answer three questions.
+
+| Walk | Question | Domain |
+|---|---|---|
+| `assert_unique_node_ids` | may two live nodes share an id? | children |
+| `collect_tree_ids` | which ids must the lineage fold account for? | children, plus refinement predicates |
+| `uniquify::collect_node_ids` | did a `PredMemo` rebuild drop or re-mint an id? | the same, as a multiset |
+
+`collect_tree_ids` reaches a predicate through a type slot, a `user_annotation`, or a `Cast` target.
+It is the operative definition of what the fold must explain: the leak classes and every
+`SourceProjection` enumerate from it, so a node it returns is a node the fold explains or reports as
+a leak. A refinement predicate is program text the user wrote — `[x for x in xs if x > k]` puts `x >
+k` in one — so it earns the same attribution as any other node. Lowering sweeps a finished predicate
+through `LoweringContext::tag_predicate`, which is what makes a guard error resolve to a caret.
+
+That sweep is the predicate domain's **entry** crossing, and the only crossing that is recorded. A
+predicate being rewritten (uniquify and inference rebuild them through a `PredMemo`) and a predicate
+being raised back into the main tree (planning) both still mint under no recording. No boundary
+check reads the ids they mint: the uniqueness walk stops at children, and the leak checks run only
+at the lowering boundary, upstream of both crossings.
+
+`uniquify::collect_node_ids` checks multiset preservation across uniquify's own `PredMemo` rebuilds,
+which is where ids could be dropped or re-minted.
+
+`Rc` sharing is load-bearing and constrains how recording may be done. One predicate term rides many
+type slots as a shared `Rc`, and planning's compile memo is `Rc`-keyed, so splitting the sharing
+compiles one predicate once per occurrence. Recording is therefore idempotent per id rather than per
+slot the id is reached through: `lowering_predicate_leaf` skips an id already recorded, which also
+stops a sweep replacing precise attribution with a coarse label. For the same reason a duplication
+path may share a predicate `Rc` with its source rather than rebuild one (see
+`design/type-inference.md`, "Sharing is an invariant, not an optimization detail").
+
+### Duplication
+
+Three primitives, chosen by what the copy denotes.
+
+- **`clone`** — the copy is a *sibling*: same value, distinct identity, `annot(p) = annot(o)`. The
+  default. Every re-minted node fires `on_copy`, so a freshen is captured as `Op::Copy`, the
+  lineage step whose outputs mirror an origin's history
+  ([The lineage model](#the-lineage-model-srcccllineagers)). Capture is live the moment a session is
+  installed and a no-op before that; no call site needs to know which.
+- **`clone_preserving_ids`** — the copy *is the same node*, so it keeps its ids. Sound because the
+  copy is never reachable from a tree beside its source, and narrow: a `Subst` discharge template,
+  which is not a tree node and is copied again at every read; a throwaway the normal path discards,
+  such as a rollback copy or a scratch tree; and a test comparing trees across a pass. Not a way to
+  silence a **leak**, the fold's report of a node whose history it cannot account for
+  ([The collapse](#the-collapse)): an `Unexplained` or a `CopyOfUnknown` means a copy was made with
+  no step open, or against an origin the log never recorded, which is a recording gap whose fix is
+  to record the copy.
+- **a copy at the occurrence's id** — the root takes an id the tree already holds and the interior
+  freshens: substitution, and the one copy that shares an id. The replacement for a `Var(𝑥)`
+  occurrence denotes what the occurrence denoted, the value of 𝑥 at that position, so attribution
+  there is the occurrence's; N reads give N subtrees under N ids the tree already holds. One site,
+  `Subst`'s compound-replacement arm in `as_expr_preserving`, which carries the alternative it is
+  chosen over: recording the copy against the occurrence instead of sharing its id resolves to the
+  same entry, at a death per occurrence and an ordering constraint on the record.
+
+**Freshen at placement, not at construction.** Most passes build intermediate structures — guard
+vectors, path conjunctions, per-branch environments — whose entries are aliased and then copied into
+the output. Placement is where a copy's multiplicity is known; freshening earlier assumes an answer,
+and the three outcomes carry different costs.
+
+- **Moved** into the output: no cost. The output node holds the fresh id, and its parent is the
+  original.
+- **Copied again** into the output: a defect the *lineage* fold catches, not the uniqueness walk.
+  The intermediate copy is stranded, so the placed copy's `Op::Copy` names an origin no node holds,
+  walking `parents` for a span dead-ends, and the fold reports `Leak::CopyOfUnknown`. Freshening the
+  substitution engine's `Subst`-resident templates produces exactly this.
+- **Dropped**: one spent id and one row no query reaches. No check reports it — both leak checks
+  enumerate from the tree, there is no produced-side check (below), and a node absent from the tree
+  is outside `assert_unique_node_ids`. Construction is the only constraint: `new` mints and records,
+  `preserve` carries.
+
+**A term crossing out of the predicate domain must not land aliased ids.** The uniqueness walk does
+not reach predicate interiors, so a pass lifting one into the main tree owes a freshen at the point
+of entry — `planning::iterate`'s `fn_of_bare_predicate` lift does exactly that. A lift that
+*rebuilds* the term is already safe: `planning::groupby`'s key extraction goes through
+`lambda_elim::run`, which re-mints every node. The requirement is that nothing aliased arrives;
+rebuilding is one mechanism that satisfies it. `groupby_recognition_lifts_the_key_without_aliasing`
+pins the property at the group-by site, so an elim that started preserving ids fails there rather
+than at a boundary. The `iterate` lift has no such test.
 
 ## The lineage model (`src/ccl/lineage.rs`)
 
@@ -81,6 +169,10 @@ a pass runs it appends `RewriteStep`s to a `LineageLog`:
 - `Op::Copy { origin, produced }` — outputs mirror `origin`'s lineage (freshened
   duplicates); silent on the origin's own fate.
 
+**`Pass`** names the compiler stage that produced or rewrote a node (`Lower`, `Uniquify`, `Inline`,
+`Desugar`, `Transact`, `Letrec`, `Mono`, `LambdaElim`, `Planning`). It lives in the lineage data, as
+each step's `via`, and never in a type.
+
 Each step *separately* carries a `blame` set (the upstream ids the outputs
 attribute to — **not** the same as `consumed`), a `nature` (the trinary fidelity
 axis `Source` / `Expansion` / `Machinery`), and a stable `label`. `consumed`
@@ -139,14 +231,11 @@ Transients (born + consumed within the phase) compose away. A two-sided leak
 audit (`Leak`) guarantees no node silently loses its history: an output with no
 lineage (`Unexplained`) and an input that vanished unconsumed (`Dropped`).
 
-Both checks enumerate from the **tree**. There is deliberately no third check on
-the *produced* side — "every id a step claims to produce is held by some node" —
-because it is not decidable against the node set the fold works over: lowering
-tags the nodes inside a refinement predicate, but that set is `collect_tree_ids`,
-the `walk_children` domain, which excludes predicate interiors, so every
-predicate id would read as a violation.
+Both checks enumerate from the **tree**. There is no third check on the *produced*
+side — "every id a step claims to produce is held by some node" — because
+legitimate shapes violate it.
 
-Two legitimate shapes would read as violations too. Uncurrying `def f(x, y)`
+Uncurrying `def f(x, y)`
 builds one `__arg_tuple_0.0` projection template and substitutes a freshened copy
 of it at each `x`; every copy's root carries that occurrence's own id, so the
 template's own root id is tagged and then held by no node. The read-your-writes
@@ -157,7 +246,7 @@ cannot see. Saying it explicitly means emitting the discard the model already
 has, `Transform { consumed: [id], produced: [] }`, which neither site does today.
 
 Construction closes the gap the check would have watched: a node is built either
-by `TypedExpr::new` (mint, recorded) or `TypedExpr::preserve` (carry an existing
+by `Expr::new` (mint, recorded) or `Expr::preserve` (carry an existing
 id, nothing recorded), so an id cannot be minted and then discarded.
 
 The fold is in tree; **planned** is its use at the inspector's two pane
@@ -213,11 +302,11 @@ boundaries, which needs the pass logs above.
   consumption shows which distinction is load-bearing. Treat both axes as
   unstable until then.
 
-  At the lowering→pipeline handoff (before uniquify/inference, so the release
+  At the lowering→pipeline handoff (before uniquify and inference, so the release
   `InferError` read timing is unchanged) `collapse_lowering` folds the log
   **once** into the always-on **lowering projection** (`NodeId →
-  SourceAttribution`, covering every `walk_children` node — refinement-predicate
-  interiors stay outside). This is the degenerate lowering case of `collapse`
+  SourceAttribution`, covering every id `collect_tree_ids` enumerates, refinement
+  predicates included). This is the degenerate lowering case of `collapse`
   (shared `RootTracker` core): no input pane (roots start empty, leaves are pure
   insertions attributed from their literal anchor), no `LineageMap` output, no
   upstream attr (a `Copy` mirrors its origin's already-folded entry). `Pass::Lower`
diff --git a/src/ccl/expr.rs b/src/ccl/expr.rs
index 43bdd69a..08d6ee6d 100644
--- a/src/ccl/expr.rs
+++ b/src/ccl/expr.rs
@@ -705,7 +705,7 @@ impl TypedExprNode {
 /// deliberately ignores `node_id`. Provenance is metadata, not part of a node's
 /// value, so two structurally-equal nodes must compare equal even with distinct
 /// ids.
-#[derive(Debug, Clone)]
+#[derive(Debug)]
 pub struct TypedExpr {
     /// The inferred type of this expression.
     ///
@@ -723,10 +723,9 @@ pub struct TypedExpr {
     /// (see [`crate::ccl::provenance`]). Excluded from [`PartialEq`] because
     /// provenance is metadata, not part of the node's value.
     ///
-    /// `Clone` copies `node_id`, so a cloned node *shares* its source's id;
-    /// freshening a clone's id is a deliberate later step, done where it
-    /// matters (monomorphization calls [`freshen_node_id`](Self::freshen_node_id)
-    /// or [`freshen_node_ids_deep`](Self::freshen_node_ids_deep) explicitly).
+    /// **`Clone` freshens** (see the [`Clone`] impl below), so reaching a
+    /// duplicated id takes writing one deliberately, through
+    /// [`preserve`](Self::preserve).
     ///
     /// # What is forbidden is a mint, not a write
     ///
@@ -752,6 +751,56 @@ pub struct TypedExpr {
 /// Type alias for backward compatibility. `Expr` is now [`TypedExpr`].
 pub type Expr = TypedExpr;
 
+/// Hand-written so that **a clone is a sibling, not the same node**: every node
+/// it copies gets a freshly-minted [`NodeId`], and every `(origin, fresh)` pair
+/// is reported to the ambient lineage recorder via
+/// [`on_copy`](crate::ccl::lineage::on_copy).
+///
+/// A derived `Clone` would copy `node_id`, making every duplication site decide
+/// whether to keep the id or freshen it. Freshening here removes the decision;
+/// `src/ccl/design/provenance.md`, "Node identity (`src/ccl/provenance.rs`)" has
+/// what a wrong decision costs.
+///
+/// **The named id-sharing paths.** Sharing an id takes writing one through
+/// [`TypedExpr::preserve`] (one node at an id already in hand),
+/// [`TypedExpr::clone_preserving_ids`] (a subtree at its source's ids), the
+/// [`preserving_ids`](crate::ccl::lineage::preserving_ids) scope that backs it —
+/// called directly by `PredMemo`'s rebuilds in `crate::ccl::ccl_utils` — the
+/// `*_preserving` constructors
+/// ([`expr_stmt_preserving`](TypedExpr::expr_stmt_preserving),
+/// [`let_in_preserving`](TypedExpr::let_in_preserving)), which are `preserve` in
+/// convenience form, or the one literal in [`crate::ccl::subst`]'s
+/// `as_expr_preserving`, where a substituted occurrence's id lands on the
+/// replacement's root.
+///
+/// The freshen is deep by construction: `node.clone()` clones the children, and
+/// each child is a `TypedExpr` reaching this same impl.
+///
+/// **Type slots are not freshened, and that is the rule, not an omission.** A
+/// [`Type`] carries no identity: the only [`NodeId`]s reachable through one are
+/// the `TypedExpr`s inside a `Refinement.predicate`, which is an
+/// `Rc<TypedExpr>` — so `ty.clone()` bumps a refcount and reaches this impl not
+/// at all. That is load-bearing twice over: predicate interiors are outside the
+/// *uniqueness* domain (`assert_unique_node_ids` walks children only), and
+/// planning's compile memo is keyed on `Rc` identity, so splitting the sharing
+/// would compile one predicate once per copy.
+///
+/// **`NodeId::PLACEHOLDER` is not preserved.** A [`throwaway`](TypedExpr::throwaway)
+/// node is built to be rendered into a panic message, never cloned into a tree;
+/// cloning one mints a real id, and `on_copy` drops the pair because its origin
+/// is the sentinel. Nothing is recorded and nothing reaches a checked tree.
+impl Clone for TypedExpr {
+    fn clone(&self) -> Self {
+        let node_id = crate::ccl::lineage::copy_id(self.node_id);
+        TypedExpr {
+            ty: self.ty.clone(),
+            node: self.node.clone(),
+            user_annotation: self.user_annotation.clone(),
+            node_id,
+        }
+    }
+}
+
 /// Hand-written to **exclude `node_id`** from equality.
 ///
 /// `node_id` is provenance metadata, not part of a node's value: two nodes that
@@ -767,26 +816,6 @@ impl PartialEq for TypedExpr {
     }
 }
 
-/// Shared deep-freshen walk over an expression's node-set: re-mints this node's
-/// id (which fires the ambient `on_copy` recorder hook) then descends into its
-/// children. Backs [`TypedExpr::freshen_node_ids_deep`]; the interior variant
-/// calls it per child, skipping the root's own re-mint.
-///
-/// **Type slots are not walked, and that is the rule, not an omission.** A
-/// [`Type`] carries no identity: the only [`NodeId`]s reachable through one are
-/// the [`TypedExpr`]s inside a `Refinement.predicate`, and those are outside the
-/// id domain — `assert_unique_node_ids` excludes predicates deliberately, and the
-/// lineage fold's leak classes and `SourceProjection` both enumerate from
-/// `collect_tree_ids` (the `walk_children` domain), so a predicate-interior id is
-/// carried but never checked. Freshening them was write-only work whose only
-/// observable effect was splitting predicate `Rc` sharing — planning's compile
-/// memo is keyed on `Rc` identity, so each split predicate is compiled once per
-/// copy. See `design/provenance.md`, "The id domain".
-fn freshen_from_expr(e: &mut TypedExpr) {
-    e.freshen_node_id();
-    e.walk_children_mut(freshen_from_expr);
-}
-
 impl TypedExpr {
     /// Construct a new [`TypedExpr`] with a [`Type::Hole`] placeholder and no user annotation.
     ///
@@ -819,7 +848,7 @@ impl TypedExpr {
     /// These are the only two ways to build a node, and the recorder sees exactly
     /// the difference: `new` mints and records a birth, `preserve` does neither.
     ///
-    /// # Two shapes build a node at an existing id; only one of them is this
+    /// # Three shapes build a node at an existing id; only one of them is this
     ///
     /// **Reaching into another node for its id** — `node_id: src.node_id`, where
     /// `src` is some *other* node — is this constructor's shape, and the one where
@@ -838,6 +867,11 @@ impl TypedExpr {
     /// assertion far away. Roughly three dozen such rebuilds live in
     /// `transact_phase`, `inline`, and `channelize`; converting them would trade a
     /// compile-time guarantee for a runtime one, once per site.
+    ///
+    /// **A copy at an id the tree already holds** — a subtree cloned, its root
+    /// taking a caller-supplied id — is neither, and is one site:
+    /// [`crate::ccl::subst`]'s `as_expr_preserving`, a literal for the same
+    /// field-check reason.
     pub(crate) fn preserve(node_id: NodeId, node: TypedExprNode) -> Self {
         TypedExpr {
             node,
@@ -863,72 +897,53 @@ impl TypedExpr {
         self.node_id
     }
 
-    /// Move an **already-cloned** node onto `node_id`, consuming and returning it
-    /// — the root-carry step of a compound substitution.
-    ///
-    /// This is the one legitimate write to `node_id` outside a constructor, and it
-    /// is named so it reads as deliberate rather than as a stray assignment. It is
-    /// sound for the same reason a preserving struct literal is: a clone mints
-    /// nothing, so overwriting its root id records no birth and strands none. The
-    /// id it drops is the clone's copied one, which no recorded step ever claimed.
-    ///
-    /// Not a way to *set* an arbitrary id on a freshly-minted node — that is the
-    /// phantom [`preserve`](Self::preserve) exists to prevent. The caller must
-    /// already hold a clone, and `node_id` must be an id some occurrence carries.
-    pub(crate) fn re_root(mut self, node_id: NodeId) -> Self {
-        self.node_id = node_id;
-        self
-    }
-
-    /// Re-mint this node's [`NodeId`], returning `(old, new)`. A cloned subtree
-    /// shares the original's ids; freshening makes them unique again.
-    ///
-    /// Deliberately fresh-only — there is no `set_node_id(arbitrary)`. Ids are
-    /// minted at construction; the one legitimate later mutation is re-minting
-    /// a clone's copied id.
-    pub(crate) fn freshen_node_id(&mut self) -> (NodeId, NodeId) {
-        let old = self.node_id;
-        let new = NodeId::fresh();
-        self.node_id = new;
-        // Every duplication path funnels through here — the direct callers and
-        // `freshen_node_ids_deep`'s per-node walk alike — so a single `on_copy`
-        // hook reports the (old, new) pair to any open lineage step.
-        crate::ccl::lineage::on_copy(old, new);
-        (old, new)
-    }
-
-    /// Deep-freshen every [`NodeId`] in this expression's node-set — the
-    /// `walk_children` domain, which is the whole id domain (type slots carry no
-    /// identity; see [`freshen_from_expr`]). Each re-minted node fires the ambient
-    /// `on_copy` recorder hook (via
-    /// [`freshen_node_id`](Self::freshen_node_id)), so an open lineage step
-    /// captures the copies.
-    ///
-    /// This is the single deep-freshen walk shared by monomorphization's clone
-    /// freshening and the transact/letrec phases' `subst_env` copies. Do not
-    /// hand-roll a second walk over this node-set.
-    ///
-    /// Not to be confused with [`crate::ccl::uniquify`]'s `collect_node_ids`,
-    /// which *is* predicate-inclusive: it is a debug tripwire asserting uniquify
-    /// preserves every id as a **multiset** across its own predicate rebuilds, a
-    /// different property over a deliberately different domain.
-    pub(crate) fn freshen_node_ids_deep(&mut self) {
-        freshen_from_expr(self);
-    }
-
-    /// Deep-freshen the **interior** of this node — every descendant — while
-    /// leaving the node's *own* [`NodeId`] untouched.
-    ///
-    /// This is the root-carry primitive: the
-    /// substitution engine's compound-replacement arm carries the occurrence's
-    /// id onto the replacement *root* (a preserve inheriting the occurrence's
-    /// span/attribution) and freshens only the interior, which lands as ambient
-    /// `Copy`s mirroring the template. Every re-minted interior node fires the
-    /// `on_copy` hook (via [`freshen_node_id`](Self::freshen_node_id)), so an
-    /// open lineage step captures them.
-    pub(crate) fn freshen_interior_node_ids(&mut self) {
-        // The root's own id is preserved; only its children are freshened.
-        self.walk_children_mut(freshen_from_expr);
+    /// A deep copy at the **same identities** — the opt-out from the freshening
+    /// [`Clone`], and the subtree analogue of [`preserve`](Self::preserve).
+    ///
+    /// Discouraged, and narrow: three shapes call it. Anywhere else a copy that
+    /// duplicates ids is a bug an id-uniqueness assert will find later, and the fix
+    /// is to **record** the freshened copy rather than to suppress the freshen —
+    /// including when the symptom is a `Leak::Unexplained` or a
+    /// `Leak::CopyOfUnknown`, which mean a copy was made with no step open or
+    /// against an unrecorded origin. Freshening everywhere and recording it costs
+    /// no compile time and no meaningful memory, so the fix is at the copy site.
+    /// See the vault's `freshening-clone-report`.
+    ///
+    /// # 1. A `Subst` discharge template
+    ///
+    /// A [`Subst`](crate::ccl::subst::Subst) discharge payload is never a tree
+    /// node. `Mapping::as_expr` clones it afresh at every read, and that read is
+    /// where each sibling is minted, so copying the template itself must mint
+    /// nothing. Every site of this shape is either the argument to
+    /// `Subst::discharge` or `Mapping`'s own `Clone` propagating one.
+    ///
+    /// # 2. A throwaway copy
+    ///
+    /// A copy the normal path *discards*, kept only so a failure or a later
+    /// comparison has something to look at: lowering's per-statement rollback copy
+    /// of the accumulated continuation (`lower_stmts_recovering`) and the
+    /// post-inference type check's scratch tree (`infer::check::check`).
+    /// Freshening them would mint whole trees for values nothing reads —
+    /// quadratic in both cases; each site carries a `TODO` saying so, and the fix
+    /// at both is to stop needing the copy at all.
+    ///
+    /// A copy that *reaches the output* is not this shape, even when the source is
+    /// dropped on the way: the output copy is a sibling and freshens.
+    ///
+    /// # 3. A test comparing trees across a pass
+    ///
+    /// A test that runs a pass over a copy and compares against the original
+    /// needs the two to be the same nodes, or it is not testing the pass. See
+    /// `uniquify`'s idempotence and id-stability tests.
+    ///
+    /// # Why this is sound
+    ///
+    /// In no shape are the source and the copy both reachable from one tree, so
+    /// nothing ever observes two live nodes at one identity. A template is not a
+    /// tree node; a throwaway sits outside the tree the pipeline goes on rewriting.
+    pub(crate) fn clone_preserving_ids(&self) -> Self {
+        let _preserving = crate::ccl::lineage::preserve_ids();
+        self.clone()
     }
 
     /// Set the inferred type on this expression, consuming and returning it.
diff --git a/src/ccl/infer/check.rs b/src/ccl/infer/check.rs
index e294185a..f4b5a09f 100644
--- a/src/ccl/infer/check.rs
+++ b/src/ccl/infer/check.rs
@@ -238,7 +238,10 @@ impl Typing for CheckCtx {
         // predicates — then return the (owned) body type unchanged rather than
         // cloning `bound_expr` for a no-op discharge.
         if crate::ccl::subst::type_free_vars(&body_ty).contains(name) {
-            crate::ccl::subst::Subst::discharge(name, bound_expr.clone()).apply_type(&body_ty)
+            // A discharge template is not a tree node: it is cloned again at
+            // every read, and that read is where the sibling is minted.
+            crate::ccl::subst::Subst::discharge(name, bound_expr.clone_preserving_ids())
+                .apply_type(&body_ty)
         } else {
             body_ty
         }
@@ -339,7 +342,9 @@ impl Typing for CheckCtx {
             Type::Fun { name: Some(b), .. }
                 if crate::ccl::subst::type_free_vars(&codomain).contains(b) =>
             {
-                crate::ccl::subst::Subst::discharge(b, argument.clone()).apply_type(&codomain)
+                // A discharge template; see the `Let` rule above.
+                crate::ccl::subst::Subst::discharge(b, argument.clone_preserving_ids())
+                    .apply_type(&codomain)
             }
             _ => codomain,
         };
@@ -521,12 +526,25 @@ fn check_node_rule(expr: &mut Expr, ctx: &mut CheckCtx) -> Result<Type, LocatedI
 /// Check reads the recorded types and discards the clone, so callers keep their
 /// `&Expr`. Returns every discovered error.
 ///
+/// The scratch copy **preserves ids**: it is never installed anywhere, so
+/// nothing can observe two nodes at one identity, and the blame ids the rules
+/// record name the caller's real nodes rather than scratch ones nobody can
+/// resolve.
+///
 /// Cost note: the full-tree clone makes each call O(tree). The hot caller is
 /// `simplify`'s `debug_typecheck` (one call per *fired* rewrite rule), which
 /// is compiled out of release builds; the remaining callers (`typecheck`,
 /// post-planning validation in `context.rs`) run once per pipeline stage.
+///
+/// **TODO(scratch-copy): ripe for refactoring — this is quadratic.** One tree
+/// copy per fired rule is O(tree x rules) over a debug compile, for a value that
+/// is read and dropped. The clone exists only because the shared per-node rules
+/// take `&mut Expr` for inference's in-place type writes, while Check needs
+/// nothing but reads. Splitting the rules' slot access — a `&mut` writer in
+/// Infer mode, a reader in Check mode — removes the copy entirely rather than
+/// making it cheaper.
 pub fn check(expr: &Expr) -> Result<(), Vec<InferError>> {
-    let mut cloned = expr.clone();
+    let mut cloned = expr.clone_preserving_ids();
     let mut ctx = CheckCtx::new(cloned.node_id());
     // Most rules *accumulate* into `ctx.errors` (see `require_sub`) so the walk keeps
     // going and reports everything it can. But a few propagate instead —
diff --git a/src/ccl/infer/solve.rs b/src/ccl/infer/solve.rs
index 9d1be044..3f3743c6 100644
--- a/src/ccl/infer/solve.rs
+++ b/src/ccl/infer/solve.rs
@@ -1683,22 +1683,6 @@ fn coalesce_type_predicates(ty: &mut Type, level: Level, ctx: &mut CoalesceCtx)
 // the use's own instantiation resolution, where refinements are excluded and the
 // reason is on `ReadPurpose::Instantiation`. Debug builds only; free in release.
 
-/// Mint a fresh [`NodeId`](crate::ccl::provenance::NodeId) for every node in a
-/// monomorphization clone.
-///
-/// Walks the main expression tree — the `walk_children` domain, which is the
-/// whole `NodeId` domain. Type slots are *not* walked: a `Type` carries no
-/// identity, and the predicate `Rc<TypedExpr>`s reachable through one are outside
-/// the id domain, so a specialization's predicate-embedded ids may alias the
-/// definition's. Nothing checks or reads them (see `ccl/design/provenance.md`,
-/// "The id domain"), and freshening them would split the predicate `Rc` sharing
-/// planning's compile memo depends on.
-fn freshen_clone_node_ids(expr: &mut Expr) {
-    // The deep walk lives on `TypedExpr::freshen_node_ids_deep`; each re-mint
-    // fires the ambient `on_copy` hook, captured by the open Mono Copy step.
-    expr.freshen_node_ids_deep();
-}
-
 /// Specialize a use of a generalized binding (frame at `frame_idx` in the
 /// walk's scope) to its instantiation, then rewrite the use to reference the
 /// specialization and stamp the specialization's resolved type on it.
@@ -1797,6 +1781,18 @@ pub(super) fn specialize_use(use_expr: &mut Expr, frame_idx: usize, ctx: &mut Co
     }
     let base_name = frame.name.clone();
     let cutoff = frame.cutoff;
+    // A freshened, independently-identified copy of the definition: `Clone`
+    // mints a new `NodeId` for every node, so N specializations cannot collide on
+    // one id. The clone itself covers the `walk_children` domain only: a predicate
+    // rides its type slot behind an `Rc` that `Type`'s `Clone` shares.
+    // `freshen_expr_type_slots` below re-mints those interiors separately, through
+    // `freshen_refinement_predicate`.
+    //
+    // TODO(mono-record): nothing captures these copies. `on_copy` records only
+    // into an open step, and no recorder spans inference. Whichever change adds
+    // one must open the step **before** this clone, because the clone is what
+    // fires `on_copy`: a step entered after it watches every pair fall on the
+    // floor and leaves the whole specialization `Unexplained`.
     let mut clone = frame.def.clone();
     // A monomorphization name carrying the source binding as provenance and a
     // globally-fresh uid for identity — so it can neither capture nor be
@@ -1822,16 +1818,6 @@ pub(super) fn specialize_use(use_expr: &mut Expr, frame_idx: usize, ctx: &mut Co
     seed_chan_dom_pairings(&resolved, &clone.ty, cutoff, &mut fresh.chan_doms);
     freshen_expr_type_slots(&mut clone, cutoff, FreshenLevel::Preserve, &mut fresh);
 
-    // `Clone` copies `node_id`, so every node in this clone currently shares
-    // the original definition's id — N specializations would collide on one id,
-    // breaking any post-inference index keyed by `NodeId`. Mint a fresh id for
-    // every cloned node. This is a dedicated walk scoped to monomorphization
-    // (not folded into the shared `freshen_expr_type_slots`, which also runs on
-    // refinement-predicate copies outside any mono context). It covers the
-    // `walk_children` domain only — predicate-embedded ids, reachable through
-    // type slots, are outside the id domain and stay aliased.
-    freshen_clone_node_ids(&mut clone);
-
     // Pin the clone to the use's live instantiation type, two-way. Inward,
     // this drives the use site's accumulated bounds into the clone's
     // freshened variables (what makes the clone *this* use's specialization);
diff --git a/src/ccl/infer/solver/scheme.rs b/src/ccl/infer/solver/scheme.rs
index 75ac77d9..41fa8a68 100644
--- a/src/ccl/infer/solver/scheme.rs
+++ b/src/ccl/infer/solver/scheme.rs
@@ -408,8 +408,8 @@ fn freshen_watches(
 /// freshen its type slots through `cache`, and install a fresh `Rc`. See
 /// [`freshen_above`]'s `Refinement` arm.
 ///
-/// **This does not preserve predicate `Rc` sharing, and unlike the rebuilding
-/// passes it threads no [`PredMemo`](crate::ccl::ccl_utils::PredMemo).** The
+/// This does not preserve predicate `Rc` sharing, and unlike the rebuilding
+/// passes it threads no [`PredMemo`](crate::ccl::ccl_utils::PredMemo). The
 /// `Rc::new` is unconditional, so N type slots of one clone that shared an `Rc`
 /// going in come out with N distinct `Rc`s, and planning — whose compile memo is
 /// `Rc`-keyed — compiles each separately. Known and not currently fixed: the
@@ -420,10 +420,11 @@ fn freshen_watches(
 /// exception, scoped and unfixed: generic instantiation", for the numbers and
 /// the decision.
 ///
-/// Note the freshened copy's predicate interior carries the *origin's*
-/// [`NodeId`](crate::ccl::provenance::NodeId)s: predicate interiors are outside
-/// the id domain (`ccl/design/provenance.md`), so nothing reads or checks them and
-/// a sharing fix here has no identity consequence.
+/// A sharing fix here has to keep one id-set per term: reusing one rebuilt `Rc`
+/// across the slots that shared an `Rc` going in is one term riding many slots,
+/// and returning the origin `Rc` when the freshen is vacuous is the same.
+/// Producing two *distinct* terms with equal ids is what nothing may do, and
+/// nothing yet checks.
 fn freshen_refinement_predicate(
     lim: Level,
     r: &Refinement,
diff --git a/src/ccl/inline.rs b/src/ccl/inline.rs
index 59bec718..7e27d52f 100644
--- a/src/ccl/inline.rs
+++ b/src/ccl/inline.rs
@@ -192,7 +192,7 @@ fn is_mut_written(name: &Name, expr: &Expr) -> bool {
 /// docs), so it *does* encounter `Defer`/`Feed`/`Define` nodes; beta-reduction
 /// routes them through the defer-aware [`crate::ccl::subst::Subst`] engine,
 /// which renames a fed-to handle when a defer-mediating UDF is inlined. The
-/// defer-returning lift itself lives in `channelize::try_lift_defer`.
+/// defer-returning lift itself lives in `channelize::lift_defer`.
 fn inline_impl(expr: Expr) -> Expr {
     // Carry `node_id` through every rebuild: reconstructing a node with
     // inlined children is a Preserve (the same node, same identity), so the
@@ -270,10 +270,10 @@ fn inline_impl(expr: Expr) -> Expr {
         // ANF defer-returning Compose source: when the first element of a Compose
         // (i.e. the for-loop iteration source) is itself a defer-returning
         // expression, wrap it in a fresh `let __for_src_N = source` binding so
-        // that `try_lift_defer` can physically rename its inner defer handle,
+        // that `lift_defer` can physically rename its inner defer handle,
         // preventing two same-named `__result` defers from coexisting in
         // `channelize`. Re-running `inline_impl` on the wrapping `Let`
-        // triggers `try_lift_defer` on the new binding.
+        // triggers the defer lift on the new binding.
         TypedExprNode::Compose(terms) => {
             TypedExprNode::Compose(terms.into_iter().map(inline_impl).collect())
         }
diff --git a/src/ccl/lambda_elim.rs b/src/ccl/lambda_elim.rs
index a22c1525..31a229b9 100644
--- a/src/ccl/lambda_elim.rs
+++ b/src/ccl/lambda_elim.rs
@@ -362,7 +362,10 @@ fn build_value_case_cform(
     let mut arm_domains: Vec<Type> = Vec::new();
     let mut default_body: Option<Expr> = None;
 
-    for b in branches {
+    // `final_or_default`'s default is the *last* branch's body, the one branch
+    // whose body reaches the output twice; the rest move whole into their arms.
+    let last = branches.len().saturating_sub(1);
+    for (i, b) in branches.into_iter().enumerate() {
         let guard = elim_lambdas(ctx, b.guard)?;
         let body = elim_lambdas(ctx, b.body)?;
         // First-match gate π̂ᵢ, lifted to a constant-in-element predicate
@@ -380,14 +383,16 @@ fn build_value_case_cform(
         // gate (a leading `if True`) leaves the driver unrefined (always fires).
         let refined_dom = refine_with(driver_dom.clone(), &gate_fn);
         arm_domains.push(refined_dom.clone());
+        if i == last {
+            default_body = Some(body.clone());
+        }
         // const(eᵢ) : {UIntRange(1) | π̂ᵢ} ⤇ V — lift the value over the gated driver.
         let arm = apply_primitive(
-            body.clone(),
+            body,
             Builtin::Const,
             Type::data_fun(refined_dom, result_ty.clone()),
         );
         arms.push(arm);
-        default_body = Some(body);
     }
 
     // A one-branch value `Case` denotes just that branch's value.
diff --git a/src/ccl/lineage.rs b/src/ccl/lineage.rs
index ae905c25..9c2e73e1 100644
--- a/src/ccl/lineage.rs
+++ b/src/ccl/lineage.rs
@@ -188,9 +188,11 @@ pub(crate) type LineageLog = Vec<RewriteStep>;
 /// itself hold). Attached-literal vs resolved-through-state are different
 /// semantics, not two instances of one thing — and thread-local statics cannot
 /// be generic, so a blame-domain generic would erase to the same at the
-/// recorder boundary anyway. There is deliberately no NodeId-blame field:
-/// root-carry eliminated its only prospective user; add one when a site
-/// demands it.
+/// recorder boundary anyway. There is no NodeId-blame field: the one site that
+/// would name an upstream id — a substitution, whose replacement takes the
+/// replaced occurrence's attribution — carries the occurrence's identity instead
+/// (`crate::ccl::subst`'s `as_expr_preserving`), so there is no id left to
+/// resolve. Add one when a site demands it.
 #[derive(Clone, Debug, PartialEq, Eq)]
 pub(crate) struct LoweringStep {
     /// The identity relation this step performs. For lowering: a leaf mint is a
@@ -808,11 +810,25 @@ thread_local! {
 /// `on_mint`/`on_copy` push NodeIds regardless (they are
 /// blame-domain-agnostic); a frame's flush matches this to emit the right step
 /// type, and the always-on lowering leaves ([`lowering_leaf`]) append here too.
+/// The lowering log, plus the set of [`NodeId`]s it has already explained.
+///
+/// The set exists for one caller: [`lowering_predicate_leaf`], which sweeps a
+/// finished refinement predicate and must **not** re-record a node that already
+/// carries precise attribution from its own lowering. The fold is
+/// last-write-wins (`attr.insert(p, out_attr)`), so a blanket sweep would
+/// silently replace a node's real span and label with the coarse predicate one —
+/// a loss no leak class can see, because the node stays explained either way.
+#[derive(Default)]
+struct LoweringRecord {
+    log: LoweringLog,
+    recorded: HashSet<NodeId>,
+}
+
 enum ActiveLog {
     /// A pass boundary's log (inspector-only sessions).
     Pass(LineageLog),
     /// Lowering's log (the always-on session, all builds).
-    Lowering(LoweringLog),
+    Lowering(LoweringRecord),
 }
 
 /// An in-flight step accumulating the ids born and copied within its dynamic
@@ -887,7 +903,7 @@ impl OpenStep {
     /// [`lowering_leaf`], so a lowering frame carries no consumed ids and no
     /// births — only the captured per-origin copies flush here, as `Copy`
     /// [`LoweringStep`]s mirroring their origins' folded entries (empty anchor).
-    fn flush_into_lowering(self, log: &mut LoweringLog) {
+    fn flush_into_lowering(self, rec: &mut LoweringRecord) {
         let OpenStep {
             label,
             nature,
@@ -901,7 +917,8 @@ impl OpenStep {
              append via lowering_leaf, frames capture only copies",
         );
         for (origin, produced) in group_copies(&copies) {
-            log.push(LoweringStep {
+            rec.recorded.extend(produced.iter().copied());
+            rec.log.push(LoweringStep {
                 op: Op::Copy { origin, produced },
                 anchor: Vec::new(),
                 nature,
@@ -917,10 +934,47 @@ impl OpenStep {
 /// route through. A no-op when no lowering session is installed (the lower
 /// submodules' unit tests, which only inspect the tree shape) or when a pass
 /// session is active (defensive: lowering leaves belong only to a lowering log).
+/// Record one node of a **refinement predicate**, unless it is already
+/// explained.
+///
+/// Lowering builds a predicate out of ordinary sub-expressions that were lowered
+/// — and therefore recorded — in the main tree, then mints and copies extra
+/// nodes to assemble them (`ccl_utils::refined_data_fun` is where the result is
+/// sealed into a `Refinement`). Those assembly nodes live only in a type slot,
+/// outside the `walk_children` domain, so nothing recorded them.
+///
+/// The skip is the whole point. A node the main-tree walk already explained has
+/// a precise span and label; re-recording it here would replace both with this
+/// sweep's coarse ones, because the fold is last-write-wins. Measured on the
+/// pipeline corpus: 318 nodes would be clobbered without it, and no leak class
+/// would report anything, since a clobbered node is still explained.
+pub(crate) fn lowering_predicate_leaf(id: NodeId, span: Span, nature: Nature, label: RewriteLabel) {
+    if id == NodeId::PLACEHOLDER {
+        return;
+    }
+    ACTIVE_LOG.with(|slot| {
+        if let Some(ActiveLog::Lowering(rec)) = slot.borrow_mut().as_mut() {
+            if !rec.recorded.insert(id) {
+                return;
+            }
+            rec.log.push(LoweringStep {
+                op: Op::Transform {
+                    consumed: Vec::new(),
+                    produced: vec![id],
+                },
+                anchor: vec![span],
+                nature,
+                label,
+            });
+        }
+    });
+}
+
 pub(crate) fn lowering_leaf(id: NodeId, span: Span, nature: Nature, label: RewriteLabel) {
     ACTIVE_LOG.with(|slot| {
-        if let Some(ActiveLog::Lowering(log)) = slot.borrow_mut().as_mut() {
-            log.push(LoweringStep {
+        if let Some(ActiveLog::Lowering(rec)) = slot.borrow_mut().as_mut() {
+            rec.recorded.insert(id);
+            rec.log.push(LoweringStep {
                 op: Op::Transform {
                     consumed: Vec::new(),
                     produced: vec![id],
@@ -1025,7 +1079,7 @@ impl Drop for StepGuard {
         // The log kind routes the flush to the matching step type.
         ACTIVE_LOG.with(|slot| match slot.borrow_mut().as_mut() {
             Some(ActiveLog::Pass(log)) => frame.flush_into(log),
-            Some(ActiveLog::Lowering(log)) => frame.flush_into_lowering(log),
+            Some(ActiveLog::Lowering(rec)) => frame.flush_into_lowering(rec),
             None => {}
         });
     }
@@ -1048,6 +1102,87 @@ pub(crate) fn on_mint(id: NodeId) {
     });
 }
 
+thread_local! {
+    /// Depth counter for [`preserve_ids`]: non-zero means a clone in progress is
+    /// a **re-allocation of the same node**, not a duplication, so it must carry
+    /// the origin's id rather than mint one.
+    ///
+    /// A counter rather than a flag because the scopes nest — a preserving copy
+    /// of a tree recurses through `Clone` for every child.
+    static PRESERVING_IDS: std::cell::Cell<usize> = const { std::cell::Cell::new(0) };
+}
+
+/// Guard returned by [`preserve_ids`]. Dropping it re-enables freshening.
+pub(crate) struct PreservingIds;
+
+impl Drop for PreservingIds {
+    fn drop(&mut self) {
+        PRESERVING_IDS.with(|c| c.set(c.get() - 1));
+    }
+}
+
+/// Open a scope in which [`TypedExpr`](crate::ccl::expr::TypedExpr)'s `Clone`
+/// **preserves** ids instead of freshening them.
+///
+/// Reach for this through
+/// [`TypedExpr::clone_preserving_ids`](crate::ccl::expr::TypedExpr::clone_preserving_ids),
+/// never directly: the scope must cover the clone and nothing else, and a
+/// genuine duplication performed inside one would silently produce a
+/// duplicate id.
+#[must_use]
+pub(crate) fn preserve_ids() -> PreservingIds {
+    PRESERVING_IDS.with(|c| c.set(c.get() + 1));
+    PreservingIds
+}
+
+/// Run `f` with id-preserving clones — a scope over a whole *rewrite region*,
+/// not over a copy.
+///
+/// # TODO(predicate-domain): this is slated for removal. Do not add callers.
+///
+/// **There is exactly one legitimate user: [`PredMemo`]'s predicate rebuild**
+/// (two call sites). Everything else that needs a preserving copy has one —
+/// [`TypedExpr::clone_preserving_ids`] — and should use it. A new caller here is
+/// almost certainly reaching for the wrong tool: this scope silences the
+/// freshening for *every* clone on the thread until `f` returns, including
+/// genuine duplications a callee performs, so it can manufacture duplicate ids
+/// in a way the per-copy method cannot.
+///
+/// It exists because what must not mint inside a predicate rebuild is not a copy
+/// but an arbitrary caller-supplied rewrite: `f` does not clone the predicate, it
+/// mints *into* it (a substitution materializing a template, a rule building a
+/// conjunction). Nothing records a predicate rewrite, so a node minted there is
+/// one no record explains, and a `Copy` rowed against it folds as
+/// [`Leak::CopyOfUnknown`]. `clone_preserving_ids` covers one copy;
+/// only a scope covers a region.
+///
+/// Preserving is honest here because the rebuilt term *replaces* the original
+/// everywhere the walk reaches — which holds only because `uniquify` walks the
+/// whole tree. It is a **scope cut**, not a design: the predicate domain needs
+/// recording, and this function should go when that lands. See the vault's
+/// `predicate-lineage-report` and `design/provenance.md`, "Walking the ids".
+///
+/// [`PredMemo`]: crate::ccl::ccl_utils::PredMemo
+/// [`TypedExpr::clone_preserving_ids`]: crate::ccl::expr::TypedExpr::clone_preserving_ids
+pub(crate) fn preserving_ids<R>(f: impl FnOnce() -> R) -> R {
+    let _guard = preserve_ids();
+    f()
+}
+
+/// The id a clone of `origin` should carry, and the one place that decides.
+///
+/// Freshens by default — a clone is a sibling — reporting the pair through
+/// [`on_copy`]. Inside a [`preserve_ids`] scope it returns `origin` unchanged
+/// and records nothing, because no new node came into being.
+pub(crate) fn copy_id(origin: NodeId) -> NodeId {
+    if PRESERVING_IDS.with(std::cell::Cell::get) > 0 {
+        return origin;
+    }
+    let fresh = NodeId::fresh();
+    on_copy(origin, fresh);
+    fresh
+}
+
 /// A hook called from the freshen helpers for every `(origin, fresh)`
 /// duplication. Pushes the pair into the innermost open step's copies, or does
 /// nothing when no step is open. Guards the [`PLACEHOLDER`] sentinel on both
@@ -1096,7 +1231,7 @@ impl RecorderSession {
     /// installed for the whole of lowering in every build. Its leaf entries
     /// ([`lowering_leaf`]) and copy-frame flushes route to a [`LoweringLog`].
     pub(crate) fn lowering() -> Self {
-        Self::install(ActiveLog::Lowering(Vec::new()))
+        Self::install(ActiveLog::Lowering(LoweringRecord::default()))
     }
 
     fn install(log: ActiveLog) -> Self {
@@ -1129,7 +1264,7 @@ impl RecorderSession {
     /// Drain and return the recorded **lowering** log, ending the session.
     pub(crate) fn into_lowering_log(self) -> LoweringLog {
         ACTIVE_LOG.with(|slot| match slot.borrow_mut().take() {
-            Some(ActiveLog::Lowering(log)) => log,
+            Some(ActiveLog::Lowering(rec)) => rec.log,
             other => {
                 debug_assert!(
                     other.is_none(),
@@ -1172,6 +1307,77 @@ mod tests {
         items.into_iter().collect()
     }
 
+    /// The predicate sweep must not overwrite attribution a node already has.
+    ///
+    /// This is the one property of `lowering_predicate_leaf` that **no leak class
+    /// can see**: the fold is last-write-wins, so a node re-recorded by the sweep
+    /// is still perfectly *explained* — it has just silently swapped its real
+    /// span and label for the sweep's coarse ones. Measured on the pipeline
+    /// corpus, a blanket sweep clobbers 318 nodes and every gate stays green.
+    #[test]
+    fn the_predicate_sweep_skips_already_recorded_nodes() {
+        let [recorded, fresh] = ids::<2>();
+        let session = RecorderSession::lowering();
+        // A node lowered in the main tree: precise span, precise label.
+        lowering_leaf(recorded, span(10, 20), Nature::Source, "lower.precise");
+        // The sweep runs over a predicate containing both that node and one
+        // minted while assembling the predicate.
+        lowering_predicate_leaf(recorded, span(0, 99), Nature::Machinery, "lower.sweep");
+        lowering_predicate_leaf(fresh, span(0, 99), Nature::Machinery, "lower.sweep");
+        let log = session.into_lowering_log();
+
+        assert_eq!(log.len(), 2, "the already-recorded node is not re-recorded");
+        let for_recorded: Vec<_> = log
+            .iter()
+            .filter(
+                |s| matches!(&s.op, Op::Transform { produced, .. } if produced == &vec![recorded]),
+            )
+            .collect();
+        assert_eq!(
+            for_recorded.len(),
+            1,
+            "exactly one entry for the lowered node"
+        );
+        assert_eq!(
+            for_recorded[0].label, "lower.precise",
+            "its own label survives"
+        );
+        assert_eq!(
+            for_recorded[0].anchor,
+            vec![span(10, 20)],
+            "its own span survives"
+        );
+
+        let for_fresh: Vec<_> = log
+            .iter()
+            .filter(|s| matches!(&s.op, Op::Transform { produced, .. } if produced == &vec![fresh]))
+            .collect();
+        assert_eq!(
+            for_fresh.len(),
+            1,
+            "the assembly node is explained by the sweep"
+        );
+        assert_eq!(for_fresh[0].label, "lower.sweep");
+    }
+
+    /// A second sweep over the same predicate adds nothing — the skip is keyed on
+    /// the id, not on which sweep recorded it, so overlapping predicates (one
+    /// term riding several type slots) cannot double-record.
+    #[test]
+    fn the_predicate_sweep_is_idempotent() {
+        let [n] = ids::<1>();
+        let session = RecorderSession::lowering();
+        lowering_predicate_leaf(n, span(1, 2), Nature::Machinery, "lower.sweep");
+        lowering_predicate_leaf(n, span(3, 4), Nature::Machinery, "lower.sweep");
+        let log = session.into_lowering_log();
+        assert_eq!(
+            log.len(),
+            1,
+            "one entry per node however many sweeps reach it"
+        );
+        assert_eq!(log[0].anchor, vec![span(1, 2)], "the first sweep wins");
+    }
+
     fn transform(consumed: Vec<NodeId>, produced: Vec<NodeId>, blame: Vec<NodeId>) -> RewriteStep {
         RewriteStep {
             op: Op::Transform { consumed, produced },
@@ -1638,12 +1844,11 @@ mod tests {
     }
 
     #[test]
-    fn lowering_root_carry_preserve_inherits_its_leaf_attribution() {
-        // Root-carry: the substituted compound root carries the
-        // occurrence's own id (a preserve). In the log that is just the
-        // occurrence's leaf entry — no copy for the root — and its interior
-        // children are copies of the template. The root keeps its own (Source)
-        // attribution; the interior mirrors the template (Machinery).
+    fn lowering_substituted_root_inherits_its_occurrences_leaf_attribution() {
+        // A substituted root carries the occurrence's own id, so the log holds no
+        // step for it — just the occurrence's leaf entry — while its interior
+        // children are copies of the replacement template. The root keeps its own
+        // (Source) attribution; the interior mirrors the template (Machinery).
         let [occurrence, tmpl_child, occ_child] = ids();
         let log = vec![
             // The param-use occurrence, imaged Source at its mint.
@@ -1665,7 +1870,7 @@ mod tests {
         assert_eq!(
             root_attr.rewritten.nature,
             Nature::Source,
-            "the carried root preserves the occurrence's own Source attribution"
+            "the carried root keeps the occurrence's own Source attribution"
         );
         assert_eq!(root_attr.spans, vec![span(10, 11)]);
         assert_eq!(
@@ -1697,9 +1902,9 @@ mod tests {
 
     // ---- the recorder ------------------------------------------------------
     //
-    // These exercise the construction hooks through *real* `Expr` construction
-    // (`Expr::new`/`Expr::lit`/`Expr::tuple` + `freshen_node_ids_deep`), not
-    // hand-built steps, so the hook wiring in `expr.rs` is under test too.
+    // These exercise the hooks through *real* `Expr` construction (`Expr::lit`,
+    // `Expr::tuple`) and the freshening `Clone`, not hand-built steps, so the hook
+    // wiring in `expr.rs` is under test too.
 
     use crate::ccl::Lit;
     use crate::ccl::expr::Expr;
@@ -1764,26 +1969,33 @@ mod tests {
 
     #[test]
     fn deep_freshen_in_a_step_yields_per_origin_copies() {
-        // Build a 3-node tree (tuple + two lits) OUTSIDE any step, clone it
-        // (Clone shares ids), then deep-freshen the clone inside a copy-only
-        // frame — one that consumes nothing and mints nothing, so its whole
-        // output is the freshen pairs the `on_copy` hook captures.
-        let tree = Expr::tuple(vec![Expr::lit(Lit::Int(1)), Expr::lit(Lit::Int(2))]);
-        let mut clone = tree.clone();
-        let old_root = clone.node_id();
-        // The pre-freshen node ids (the clone still shares the original's) are
-        // the origins each per-node `Copy` should record.
-        let old_ids: HashSet<NodeId> = std::iter::once(old_root)
-            .chain(clone.child_exprs().iter().map(|c| c.node_id()))
+        // Build a 3-node tree (tuple + two lits) OUTSIDE any step, then clone it
+        // inside a copy-only frame — one that consumes nothing and mints nothing
+        // of its own, so its whole output is the freshen pairs `Clone` reports
+        // through the `on_copy` hook.
+        let source = Expr::tuple(vec![Expr::lit(Lit::Int(1)), Expr::lit(Lit::Int(2))]);
+        // The source's node ids are the origins each per-node `Copy` should record.
+        let old_ids: HashSet<NodeId> = std::iter::once(source.node_id())
+            .chain(source.child_exprs().iter().map(|c| c.node_id()))
             .collect();
 
         let session = RecorderSession::new();
-        {
+        let clone = {
             let _g = copy_frame("dup");
-            clone.freshen_node_ids_deep();
-        }
+            source.clone()
+        };
         let log = session.into_log();
 
+        // The clone is a distinct 3-node tree sharing no id with its source.
+        let fresh_ids: HashSet<NodeId> = std::iter::once(clone.node_id())
+            .chain(clone.child_exprs().iter().map(|c| c.node_id()))
+            .collect();
+        assert_eq!(fresh_ids.len(), 3);
+        assert!(
+            fresh_ids.is_disjoint(&old_ids),
+            "a clone shares no id with its source"
+        );
+
         // Three nodes freshened: three per-origin Copy steps, one produced each,
         // one Copy per pre-freshen origin id.
         assert_eq!(log.len(), 3, "one Copy step per freshened origin");
@@ -1808,13 +2020,12 @@ mod tests {
         // A Transform frame opened purely to capture a deep freshen (no consumed
         // ids, no births) emits only its per-origin Copy steps — never an empty
         // `Transform { consumed: [], produced: [] }`.
-        let tree = Expr::tuple(vec![Expr::lit(Lit::Int(1)), Expr::lit(Lit::Int(2))]);
-        let mut clone = tree.clone();
+        let source = Expr::tuple(vec![Expr::lit(Lit::Int(1)), Expr::lit(Lit::Int(2))]);
 
         let session = RecorderSession::new();
         {
             let _g = step("wrap.freshen", vec![], vec![], Nature::Machinery);
-            clone.freshen_node_ids_deep();
+            let _clone = source.clone();
         }
         let log = session.into_log();
         assert_eq!(log.len(), 3, "only the three per-origin Copy steps");
@@ -1827,10 +2038,10 @@ mod tests {
     #[test]
     fn no_step_open_records_nothing() {
         let session = RecorderSession::new();
-        // Construction and freshening with an empty stack capture nowhere.
+        // Construction and cloning with an empty stack capture nowhere.
         let _e = Expr::lit(Lit::Int(1));
-        let mut x = Expr::lit(Lit::Int(2));
-        x.freshen_node_id();
+        let x = Expr::lit(Lit::Int(2));
+        let _copy = x.clone();
         let log = session.into_log();
         assert!(log.is_empty(), "empty stack ⇒ nothing recorded: {log:?}");
     }
@@ -1982,11 +2193,9 @@ mod tests {
             let template = Expr::lit(Lit::Int(0));
             t = template.node_id();
             // Copy it twice — one freshened clone per read site.
-            let mut r1 = template.clone();
-            r1.freshen_node_id();
+            let r1 = template.clone();
             c1 = r1.node_id();
-            let mut r2 = template.clone();
-            r2.freshen_node_id();
+            let r2 = template.clone();
             c2 = r2.node_id();
         }
         let log = session.into_log();
diff --git a/src/ccl/lower/comprehension.rs b/src/ccl/lower/comprehension.rs
index da98ee81..9b866813 100644
--- a/src/ccl/lower/comprehension.rs
+++ b/src/ccl/lower/comprehension.rs
@@ -183,7 +183,6 @@ pub(super) fn lower_list_comp(
             source,
             &gen_iter_vars[0],
             &body,
-            &mut false,
             comp.element.span,
             ctx,
         ));
@@ -321,6 +320,7 @@ pub(super) fn lower_list_comp(
             element_span,
             lc,
         );
+        ctx.tag_predicate(&pred_expr, element_span, "lower.comp_filter_pred");
         let target_ty = refined_data_fun(Type::Hole, pred_expr, Type::Hole);
         Ok(ctx.tag_machinery(make_cast(unrefined_lambda, target_ty), element_span, lc))
     } else {
@@ -340,34 +340,25 @@ pub(super) fn lower_list_comp(
     }
 }
 
+/// Hand out a tree copy of `origin` for one arm of a fan-out. Every arm is a
+/// sibling, including the first: a fan-out places the same subtree under several
+/// arms and no arm is privileged. The copy-frame records each copy as a `Copy` of
+/// the origin, so every arm's attribution mirrors the original's.
+fn fan_out_copy(origin: &Expr, label: &'static str) -> Expr {
+    use crate::ccl::lineage::copy_frame;
+    let _frame = copy_frame(label);
+    origin.clone()
+}
+
 /// Float a value-`Case` *source* out of a single-generator comprehension:
 /// `[e for x in Case{gᵢ→srcᵢ}]` ⟹ `Case{gᵢ → [e for x in srcᵢ]}`. Sound because
 /// the guards do not reference the comprehension variable `x`. Recurses so a
 /// nested conditional source flattens per arm; a concrete (non-`Case`) source
 /// builds the ordinary map chain `λ __idx → __idx ▷ src ▷ (λ x → body)`.
-/// Hand out a tree copy of `origin` for one arm of a fan-out, **keep-first**: the
-/// first copy keeps the original's `NodeId`s and every later one is deep-freshened
-/// inside a lowering copy-frame, so its re-mints land as `Copy` steps mirroring the
-/// original's attribution. A fan-out places the same subtree under several arms and
-/// two main-tree nodes may not share an id — see `src/ccl/design/provenance.md`,
-/// "The id domain". (The same keep-first shape as the chained-comparison operand
-/// freshen in `lower::exprs`.)
-fn fan_out_copy(origin: &Expr, used: &mut bool, label: &'static str) -> Expr {
-    let mut copy = origin.clone();
-    if *used {
-        use crate::ccl::lineage::copy_frame;
-        let _frame = copy_frame(label);
-        copy.freshen_node_ids_deep();
-    }
-    *used = true;
-    copy
-}
-
 fn float_comp_source_case(
     source: Expr,
     iter_var: &str,
     body: &Expr,
-    body_used: &mut bool,
     span: Span,
     ctx: &mut LoweringContext,
 ) -> Expr {
@@ -386,7 +377,7 @@ fn float_comp_source_case(
                 pattern: b.pattern,
                 guard: b.guard,
                 // The arm body *is* this arm's source collection; float into it.
-                body: float_comp_source_case(b.body, iter_var, body, body_used, span, ctx),
+                body: float_comp_source_case(b.body, iter_var, body, span, ctx),
             })
             .collect();
         // The rebuilt `Case` is the floated encoding of the rule, not an image of
@@ -409,7 +400,7 @@ fn float_comp_source_case(
     // a conditional source join as collections rather than colliding as
     // capabilities whose index domains would meet — and saying it on the node
     // lowering mints is what keeps it from being decided by whoever consumes it.
-    let body = fan_out_copy(body, body_used, "lower.comp_source_case_body");
+    let body = fan_out_copy(body, "lower.comp_source_case_body");
     let cs = "lower.comp_source_case";
     let elem_map = ctx.tag_machinery(Expr::lambda(iter_var, Type::Hole, body), span, cs);
     ctx.tag_machinery(
@@ -443,9 +434,6 @@ fn fan_out_element_case(
     // `true → Case{…}`) into one flat partition, so each arm is a plain value.
     let branches = flatten_trailing_value_case(branches);
     let mut prior_guards: Vec<Expr> = Vec::new();
-    // The source subtree is placed once per arm in the element map and once more in
-    // that arm's gate, so every use after the first must be a freshened copy.
-    let mut source_used = false;
     let arms: Vec<Expr> = branches
         .into_iter()
         .map(|b| {
@@ -456,7 +444,7 @@ fn fan_out_element_case(
             // own images, recorded when they were lowered.
             let ec = "lower.comp_elem_case";
             let idx_var = ctx.tag_machinery(Expr::var(Name::raw(outer_var)), span, ec);
-            let arm_src = fan_out_copy(&source, &mut source_used, "lower.comp_elem_case_source");
+            let arm_src = fan_out_copy(&source, "lower.comp_elem_case_source");
             let read = ctx.tag_machinery(Expr::apply(idx_var, arm_src), span, ec);
             let arm_body = ctx.tag_machinery(Expr::lambda(iter_var, Type::Hole, b.body), span, ec);
             let applied = ctx.tag_machinery(Expr::apply(read, arm_body), span, ec);
@@ -475,13 +463,15 @@ fn fan_out_element_case(
             let gate_on_source = Expr::apply(
                 Expr::apply(
                     Expr::var(Name::elem()),
-                    fan_out_copy(&source, &mut source_used, "lower.comp_elem_case_source"),
+                    fan_out_copy(&source, "lower.comp_elem_case_source"),
                 ),
                 Expr::lambda(iter_var, Type::Hole, gate),
             );
-            // `gate_on_source` rides the cast target's refinement predicate, so its
-            // interior is outside the NodeId domain — carried, never checked — and
-            // needs no tagging (`src/ccl/design/provenance.md`, "The id domain").
+            // `gate_on_source` rides the cast target's refinement predicate, so
+            // its interior is in the domain the fold must explain and nothing in
+            // the main-tree walk reaches it. Sweep it
+            // (`src/ccl/design/provenance.md`, "Walking the ids").
+            ctx.tag_predicate(&gate_on_source, span, "lower.comp_arm_gate_pred");
             let target = refined_data_fun(Type::Hole, gate_on_source, Type::Hole);
             ctx.tag_machinery(make_cast(elem_map, target), span, ec)
         })
diff --git a/src/ccl/lower/exprs.rs b/src/ccl/lower/exprs.rs
index c25a24e7..2dd53fee 100644
--- a/src/ccl/lower/exprs.rs
+++ b/src/ccl/lower/exprs.rs
@@ -87,7 +87,13 @@ pub(super) fn lower_call(
             let key_ty = ctx.fresh_shared_hole();
             // `bare_pred` (and the `collection` clone inside it) lives in the
             // cast target's refinement predicate — a type slot outside the
-            // `walk_children` domain — so its nodes are deliberately untagged.
+            // `walk_children` domain. It used to be left deliberately untagged
+            // for exactly that reason; it is now swept by `tag_predicate` below,
+            // because `collect_tree_ids` reaches refinement predicates and the
+            // lowering fold therefore has to explain them. The `collection`
+            // clone is the reason this matters more than it used to: `Clone`
+            // freshens, so that clone no longer aliases an already-tagged
+            // main-tree id.
             let bare_pred = Expr::binop(
                 Expr::apply(
                     Expr::apply(Expr::var(Name::elem()), collection.clone()),
@@ -114,6 +120,7 @@ pub(super) fn lower_call(
                 func.span,
                 gb,
             );
+            ctx.tag_predicate(&bare_pred, func.span, "lower.groupby_key_pred");
             let target_ty = refined_data_fun(Type::Hole, bare_pred, Type::Hole);
             let cast = ctx.tag_machinery(make_cast(unrefined_inner, target_ty), func.span, gb);
             // A group-by is a **data function** (a keyed collection): stamp its
@@ -456,11 +463,15 @@ pub(super) fn lower_compare(
     }
 
     // Build one BinOp per (op, adjacent-operand-pair). Each middle operand is
-    // shared by two pairs; a bare clone would put the same NodeIds in the tree
-    // twice. Keep-first: an operand's first tree use keeps its original ids
-    // (operand i+1 first appears as pair i's RIGHT side), and its second use
-    // (as pair i+1's LEFT side) is a deep-freshened copy whose folded
-    // attributions mirror the original's.
+    // placed in two pairs, and no placement is privileged, so every placement is a
+    // freshened copy taken inside a lowering copy-frame: each re-minted node lands
+    // as a `Copy` step mirroring the original operand's (Source) image, which is
+    // the attribution wanted for a duplicated operand.
+    let operand = |i: usize| {
+        use crate::ccl::lineage::copy_frame;
+        let _frame = copy_frame("lower.compare_operand");
+        operands[i].clone()
+    };
     let mut comparisons: Vec<Expr> = Vec::with_capacity(ops.len());
     for (i, op) in ops.iter().enumerate() {
         let kind = match op {
@@ -471,22 +482,8 @@ pub(super) fn lower_compare(
             CmpOp::Gt => CompareKind::Greater,
             CmpOp::GtE => CompareKind::GreaterOrEq,
         };
-        let lhs = if i == 0 {
-            // Operand 0's only use.
-            operands[0].clone()
-        } else {
-            // Operand i's second use (its first was pair i-1's right side). A
-            // bare clone would share NodeIds; freshen a copy inside a lowering
-            // copy-frame so each re-minted node lands as a `Copy` LoweringStep
-            // mirroring the original operand's (Source) image — exactly the
-            // attribution wanted for the duplicated operand.
-            use crate::ccl::lineage::copy_frame;
-            let mut copy = operands[i].clone();
-            let _frame = copy_frame("lower.compare_operand");
-            copy.freshen_node_ids_deep();
-            copy
-        };
-        let rhs = operands[i + 1].clone();
+        let lhs = operand(i);
+        let rhs = operand(i + 1);
         // Each pair comparison images its `<op>` in the chain, spanning its two
         // operands. It is *not* `Nature::Source` — a chained comparison is one of
         // the cost cases of the structural rule (see `tag_source`): only the
diff --git a/src/ccl/lower/functions.rs b/src/ccl/lower/functions.rs
index 20f4ba31..f8146712 100644
--- a/src/ccl/lower/functions.rs
+++ b/src/ccl/lower/functions.rs
@@ -184,18 +184,18 @@ pub(super) fn uncurry_params(
     let up = "lower.uncurry_proj";
     let body_with_subs = params.iter().enumerate().fold(body_expr, |acc, (i, arg)| {
         // The projection plumbing is manufactured per *occurrence*: the
-        // substitution deep-freshens the template's INTERIOR into every
-        // occurrence of the parameter (root-carry keeps each occurrence's own
-        // id/attribution — see `substitute_param_in_body`), so tag the template's
+        // substitution deep-freshens this template's INTERIOR into every
+        // occurrence of the parameter while each occurrence keeps its own
+        // id/attribution (see `substitute_param_in_body`), so tag the template's
         // three nodes as machinery leaves.
         //
         // The template itself never enters the tree. Its two interior ids reach
         // the tree as the freshened copies the frame below captures, so they are
-        // origins of live nodes; its ROOT does not — root-carry replaces it with
-        // each occurrence's own id — so that one id is tagged and then carried by
-        // nothing. Harmless in the product (the projection is filtered to the
-        // output tree, so the entry drops out), and the reason there is no
-        // produced-side leak class: see `design/provenance.md`, "The collapse".
+        // origins of live nodes; its ROOT does not — each occurrence's own id
+        // replaces it — so that one id is tagged and then carried by nothing.
+        // Harmless in the product (the projection is filtered to the output tree,
+        // so the entry drops out), and the reason there is no produced-side leak
+        // class: see `design/provenance.md`, "The collapse".
         let var = ctx.tag_machinery(Expr::var(&tuple_name), fn_span, up);
         let idx = ctx.tag_machinery(Expr::proj_index(i), fn_span, up);
         let proj = ctx.tag_machinery(Expr::apply(var, idx), fn_span, up);
@@ -408,12 +408,11 @@ in add"
     }
 
     /// Occurrence fidelity: in a multi-param `def` whose params occur more than
-    /// once, uncurry substitutes a fresh tuple-projection template into each
-    /// occurrence — and root-carry (see [`substitute_param_in_body`]) makes each
-    /// projection *root* preserve the occurrence's own id, so it inherits that
-    /// occurrence's own source span instead of the one `def` span shared by every
-    /// copy. The corpus otherwise has no multi-param `def`, so pin the span
-    /// fidelity here.
+    /// once, uncurry substitutes a tuple-projection template into each occurrence,
+    /// and each projection *root* keeps that occurrence's own id (see
+    /// [`substitute_param_in_body`]), so it inherits that occurrence's own source
+    /// span instead of the one `def` span every copy of the template shares. The
+    /// corpus otherwise has no multi-param `def`, so pin the span fidelity here.
     #[test]
     fn uncurry_projection_roots_carry_occurrence_spans() {
         use crate::ccl::TypedExprNode;
@@ -448,8 +447,8 @@ in add"
 
         // Collect the source span each uncurry-projection ROOT carries. A
         // projection node is `Apply { function: Proj(Index(_)) }` — its argument
-        // is the synthetic tuple var. Its own id is the occurrence's, carried by
-        // root-carry, so its projection entry is the occurrence's `Source` image.
+        // is the synthetic tuple var. Its own id is the occurrence's, so its
+        // projection entry is that occurrence's `Source` image.
         fn projection_spans(e: &Expr, proj: &SourceProjection, out: &mut Vec<Span>) {
             if let TypedExprNode::Apply { function, .. } = &e.node
                 && matches!(function.node, TypedExprNode::Proj(_))
diff --git a/src/ccl/lower/mod.rs b/src/ccl/lower/mod.rs
index 2d1d7015..3c2efc59 100644
--- a/src/ccl/lower/mod.rs
+++ b/src/ccl/lower/mod.rs
@@ -489,6 +489,34 @@ impl LoweringContext {
         expr
     }
 
+    /// Record every node of a finished **refinement predicate** that nothing
+    /// else has explained.
+    ///
+    /// A predicate is assembled from sub-expressions that were lowered — and so
+    /// recorded — in the main tree, plus the nodes minted and copied to join them
+    /// up. Sealed into a `Refinement` it lives in a *type slot*, outside the
+    /// `walk_children` domain, so those assembly nodes have no leaf of their own
+    /// and the widened `collect_tree_ids` would report them `Unexplained`.
+    ///
+    /// Call this on the predicate **immediately before** handing it to
+    /// `ccl_utils::refined_data_fun`, which is the single point a lowering
+    /// predicate is born. Nodes already recorded keep their own precise
+    /// attribution — see [`lowering_predicate_leaf`].
+    ///
+    /// [`lowering_predicate_leaf`]: crate::ccl::lineage::lowering_predicate_leaf
+    pub(super) fn tag_predicate(&mut self, pred: &Expr, span: Span, label: RewriteLabel) {
+        fn go(e: &Expr, span: Span, label: RewriteLabel) {
+            crate::ccl::lineage::lowering_predicate_leaf(
+                e.node_id(),
+                span,
+                Nature::Machinery,
+                label,
+            );
+            e.walk_children(|c| go(c, span, label));
+        }
+        go(pred, span, label);
+    }
+
     /// Mint a fresh `{prefix}_{id}` name from the monotonic synthetic-id
     /// counter, bumping it so every minted name is distinct within a lowering.
     /// The `fresh_*` methods below wrap this, each fixing its own `prefix`.
diff --git a/src/ccl/lower/stmts.rs b/src/ccl/lower/stmts.rs
index 06860d70..044f39c5 100644
--- a/src/ccl/lower/stmts.rs
+++ b/src/ccl/lower/stmts.rs
@@ -61,12 +61,24 @@ pub(super) fn lower_stmts_recovering(
     // we've built so far), so when one fails we need a snapshot to fall back
     // to. Cloning unconditionally is fine — lowering isn't a hot path and
     // errors are exceptional.
+    //
+    // The snapshot preserves ids, and must. It is a *rollback copy*, not a
+    // sibling: at most one of `acc` and `backup` ever reaches the tree.
+    //
+    // TODO(rollback-copy): ripe for refactoring — this is quadratic. The
+    // continuation grows with every statement and is copied whole for each one,
+    // so a clean compile of an n-statement program does O(n^2) node copies for a
+    // value the happy path drops. Preserving ids keeps it off the *id* ledger
+    // (a freshening clone would deep-mint all of it), but the copy itself
+    // remains. The fix is to stop needing a snapshot: have `lower_middle_stmt`
+    // borrow, or return the continuation back on the error path, so recovery
+    // costs nothing when nothing fails.
     let body = rest
         .iter()
         .enumerate()
         .rev()
         .fold(final_expr, |acc, (i, stmt)| {
-            let backup = acc.clone();
+            let backup = acc.clone_preserving_ids();
             match lower_middle_stmt(stmt, &rest[..i], acc, &outer_bindings, ctx, true) {
                 Ok(e) => e,
                 Err(e) => {
diff --git a/src/ccl/mut_elim.rs b/src/ccl/mut_elim.rs
index 68a65f7d..ee708abb 100644
--- a/src/ccl/mut_elim.rs
+++ b/src/ccl/mut_elim.rs
@@ -1119,11 +1119,10 @@ fn body_has_feed(expr: &Expr) -> bool {
 /// place. The result is the clean generator body (`Case { gᵢ → Feed; true → unit }`
 /// / a bare `Feed`) that `channelize`'s feed fan-out recognizes.
 fn strip_trailing_unit(expr: Expr) -> Expr {
-    // The rebuilt `Case` below is the *same* logical node with stripped branch
-    // bodies, so it carries its original `NodeId` — a pass that minted here would
-    // break the node's link to the source it came from
-    // (`src/ccl/design/provenance.md`, "The two identity primitives
-    // (`src/ccl/provenance.rs`)").
+    // The rebuilt `Case` below is the same logical node with stripped branch
+    // bodies, so it carries its original `NodeId`; a pass that minted here would
+    // break the node's link to the source it came from. See
+    // `src/ccl/design/provenance.md`, "Node identity (`src/ccl/provenance.rs`)".
     let node_id = expr.node_id();
     match expr.node {
         TypedExprNode::ExprStmt { expr: effect, body }
@@ -1589,7 +1588,7 @@ fn attach_feed_fields(decision: Expr, feeds: &[FeedSite]) -> Expr {
             let ty = new_body.ty.clone();
             // The same logical `Let` with its feed fields attached, so it keeps its
             // own id rather than minting a replacement.
-            let mut e = Expr::let_in(binding, *bound_expr, new_body).re_root(node_id);
+            let mut e = Expr::let_in_preserving(node_id, binding, *bound_expr, new_body);
             e.ty = ty;
             e
         }
diff --git a/src/ccl/planning/groupby.rs b/src/ccl/planning/groupby.rs
index 442ee09f..c2a5c46a 100644
--- a/src/ccl/planning/groupby.rs
+++ b/src/ccl/planning/groupby.rs
@@ -182,6 +182,13 @@ fn rewrite_groupby_source(head: &Expr) -> Option<Expr> {
 
     // Compile the pointful key function to a point-free morphism V ⇒ K, then
     // build `keys = c ≫ key : I ⇒ K` and `values = c : I ⇒ V`.
+    // This lifts a term out of a *type* — the refined domain's predicate — into
+    // the term tree. A predicate interior may already alias a live main-tree id
+    // (lowering shares a comprehension's source term between the generator and
+    // the guard), so a lift can land ids that are already in use. `lambda_elim::run`
+    // rebuilds the term, re-minting every node, which is what makes the crossing
+    // safe; `groupby_recognition_lifts_the_key_without_aliasing` pins the property
+    // rather than the mechanism.
     let key_pf = lambda_elim::run((**key_expr).clone()).ok()?;
     let value_idx_ty = (**idx_ty).clone();
     let keys =
@@ -218,6 +225,7 @@ fn side_extracts_element(e: &Expr) -> bool {
 mod tests {
     use super::super::test_helpers::*;
     use super::*;
+    use crate::ccl::context::assert_unique_node_ids;
 
     #[test]
     fn test_recognize_groupby_sites_on_var() {
@@ -226,4 +234,59 @@ mod tests {
         // Should remain unchanged
         assert!(matches!(expr.node, TypedExprNode::Var(ref v) if v.base() == "x"));
     }
+
+    /// `const(cast(c)) : (k) ⇒ ({i | i ▷ c ▷ key == k} ⇒ V)` composed with a
+    /// tail — the pointful group-by source the recognizer matches, with the key
+    /// morphism deliberately **shared** between the predicate and the tail.
+    ///
+    /// That sharing is not artificial: predicate interiors are outside the
+    /// checked id domain and lowering already aliases them into the main tree
+    /// (`pred_sources = gen_sources.clone()`), so a term lifted out of a
+    /// predicate can collide with a live original.
+    fn groupby_source_sharing_its_key(key: &Expr) -> Expr {
+        let idx = Type::UIntRange(4);
+        let int = int_ty();
+        let c = var("c").with_ty(fun_ty(idx.clone(), int.clone()));
+
+        // pred = (__elem ▷ c ▷ key) == k
+        let elem = Expr::var(Name::elem()).with_ty(idx.clone());
+        let elem_c = Expr::apply(elem, c.clone()).with_ty(int.clone());
+        let extract = Expr::apply(elem_c, key.clone()).with_ty(int.clone());
+        let pred = Expr::binop(
+            extract,
+            BinOpKind::Compare(CompareKind::Equals),
+            var("k").with_ty(int.clone()),
+        )
+        .with_ty(bool_ty());
+
+        let head_ty = fun_ty(
+            int.clone(),
+            fun_ty(refined_ty(idx.clone(), pred), int.clone()),
+        );
+        let cast = Expr::cast(c.clone(), fun_ty(idx, int)).with_ty(c.ty.clone());
+        let head = apply_builtin(cast, Builtin::Const, Type::Hole, head_ty.clone());
+        // The tail stands in for the live main-tree occurrence of the shared key.
+        Expr::compose(vec![head, key.clone()]).with_ty(head_ty)
+    }
+
+    /// Recognition lifts the key extraction out of a *type* and into the term
+    /// tree, and the lifted copy must not carry ids that are still live
+    /// elsewhere. Today `lambda_elim::run` provides that by rebuilding the term;
+    /// this pins the *property* rather than the mechanism, so an elim that
+    /// started preserving ids fails here instead of at a pane boundary.
+    #[test]
+    fn groupby_recognition_lifts_the_key_without_aliasing() {
+        let key = var("key").with_ty(fun_ty(int_ty(), int_ty()));
+        let mut expr = groupby_source_sharing_its_key(&key);
+        recognize_groupby_sites(&mut expr);
+
+        assert!(
+            !matches!(&expr.node, TypedExprNode::Compose(elts)
+                if matches!(&elts[0].node, TypedExprNode::Apply { function, .. }
+                    if is_builtin(function, Builtin::Const))),
+            "the recognizer must have rewritten the source: {}",
+            symbolic(&expr)
+        );
+        assert_unique_node_ids(&expr, "planning::groupby");
+    }
 }
diff --git a/src/ccl/planning/iterate.rs b/src/ccl/planning/iterate.rs
index dfead343..d7516365 100644
--- a/src/ccl/planning/iterate.rs
+++ b/src/ccl/planning/iterate.rs
@@ -407,7 +407,10 @@ pub(super) fn wrap_with_iterate(expr: &mut Expr) {
     let mut preds: Vec<Expr> = Vec::new();
     let mut current = &domain_ty;
     while let Type::Refinement(base, refinement) = current {
-        preds.push(fn_of_bare_predicate(base.as_ref(), &refinement.predicate));
+        // Lifting a predicate out of a *type* and into the term tree: a predicate
+        // interior may already alias a live main-tree id, and one predicate `Rc`
+        // reached from two iteration sites would land twice.
+        preds.push(fn_of_bare_predicate(base.as_ref(), &refinement.predicate).clone());
         current = base.as_ref();
     }
     preds.reverse();
diff --git a/src/ccl/simplify.rs b/src/ccl/simplify.rs
index 9d00f25d..0a40a9a9 100644
--- a/src/ccl/simplify.rs
+++ b/src/ccl/simplify.rs
@@ -957,8 +957,10 @@ fn try_zip_distribute_compose(expr: &mut Expr) -> bool {
             let g_ty = arm_ty(g);
             let h_ty = arm_ty(h);
 
-            let g_compose = Expr::compose(vec![left.clone(), g.clone()]).with_ty(g_ty);
-            let h_compose = Expr::compose(vec![left.clone(), h.clone()]).with_ty(h_ty);
+            // Distribution places `left` on both legs of the zip.
+            let h_left = left.clone();
+            let g_compose = Expr::compose(vec![left, g.clone()]).with_ty(g_ty);
+            let h_compose = Expr::compose(vec![h_left, h.clone()]).with_ty(h_ty);
             vec![zip_pair(g_compose, h_compose)]
         },
     )
@@ -1970,6 +1972,56 @@ mod tests {
         assert_eq!(simplified, expected);
     }
 
+    /// Zip distribute places the left operand on both legs, so the two
+    /// placements must not share one identity.
+    ///
+    /// Arms reading the *same* slot are what make the duplication observable:
+    /// with `⟨.0, .1⟩` the follow-on product-beta consumes one copy per leg and
+    /// the survivors are disjoint, which is why the pipeline boundaries stayed
+    /// green over a corpus that never produced this shape. `⟨.0, .0⟩` beta-
+    /// reduces to `⟨f0, f0⟩`, leaving both copies of `f0` live.
+    #[test]
+    fn zip_distribute_yields_unique_node_ids_when_both_arms_read_one_slot() {
+        let int_fun = fun_ty(int_ty(), int_ty());
+        let int_pair = Type::Tuple(vec![int_ty(), int_ty()]);
+
+        let f0 = var("f0").with_ty(int_fun.clone());
+        let f1 = var("f1").with_ty(int_fun.clone());
+        let zip1 = zip_pair(f0, f1);
+
+        // ⟨.0, .0⟩ — simplifying (projections), and not both `id`, so the rule
+        // fires; both arms select the *first* component.
+        let p0 = Expr::proj_index(0).with_ty(fun_ty(int_pair.clone(), int_ty()));
+        let p0_again = Expr::proj_index(0).with_ty(fun_ty(int_pair, int_ty()));
+        let zip2 = zip_pair(p0, p0_again);
+
+        let simplified = simplify(typed_compose2(zip1, zip2));
+        crate::ccl::context::assert_unique_node_ids(&simplified, "simplify::zip_distribute");
+    }
+
+    /// The same guarantee on the shape whose beta-reduction *does* split the two
+    /// copies — a regression here would mean the fix moved rather than removed
+    /// the duplication.
+    #[test]
+    fn zip_distribute_yields_unique_node_ids_with_composed_arms() {
+        let int_fun = fun_ty(int_ty(), int_ty());
+        let int_pair = Type::Tuple(vec![int_ty(), int_ty()]);
+
+        let zip1 = zip_pair(
+            var("f0").with_ty(int_fun.clone()),
+            var("f1").with_ty(int_fun.clone()),
+        );
+        let p0 = Expr::proj_index(0).with_ty(fun_ty(int_pair.clone(), int_ty()));
+        let p1 = Expr::proj_index(1).with_ty(fun_ty(int_pair, int_ty()));
+        let zip2 = zip_pair(
+            typed_compose2(p0, var("g").with_ty(int_fun.clone())),
+            typed_compose2(p1, var("h").with_ty(int_fun)),
+        );
+
+        let simplified = simplify(typed_compose2(zip1, zip2));
+        crate::ccl::context::assert_unique_node_ids(&simplified, "simplify::zip_distribute");
+    }
+
     /// Zip distribute in n-ary compose: a ≫ ⟨f0, f1⟩ ≫ ⟨.0, .1⟩ ≫ b
     /// where right zip has simplifying arms (both projections)
     #[test]
diff --git a/src/ccl/subst.rs b/src/ccl/subst.rs
index 1230700f..bb4830de 100644
--- a/src/ccl/subst.rs
+++ b/src/ccl/subst.rs
@@ -73,15 +73,58 @@ pub type Binder = Name;
 /// what lets [`Subst::invert`] and [`Subst::split_renames`] be exact by
 /// construction: inversion legality is type-enforced, and "the rename part"
 /// means precisely the entries constructed as correspondences.
-#[derive(Clone, Debug, PartialEq)]
+#[derive(Debug, PartialEq)]
 pub enum Mapping {
     /// `binder ↦ other binder` — a correspondence between frames. Invertible.
     Rename(Binder),
     /// `binder ↦ term` — plug a term in for the binder. No inverse.
     /// (Boxed: a term is much larger than a binder name.)
+    ///
+    /// **Considered and deferred: `Rc<TypedExpr>`.** The payload is a template,
+    /// never a tree node and cloned afresh at every read ([`Mapping::as_expr`]),
+    /// so sharing it is sound. The solver copies substitutions constantly
+    /// (`Bound::render_subst`, [`Subst::then`], `compact`, `constrain`): with a
+    /// `Box` each of those ~28 sites deep-copies the payload tree, with an `Rc`
+    /// they are refcount bumps.
+    ///
+    /// One trap if it is ever done: [`Subst::for_each_discharge_term_mut`] would
+    /// become `Rc::make_mut`, which copies out through `TypedExpr`'s freshening
+    /// `Clone`. `freshen_subst_payloads` clones the `Subst` while the source
+    /// `Bound` is still alive, so the payload is **always** shared at that point
+    /// and it would freshen every time. The fix is to stop mutating in place —
+    /// map to a new `Rc` per payload instead. See the vault's
+    /// `freshening-clone-report`.
     Discharge(Box<TypedExpr>),
 }
 
+/// Hand-written so that **copying a substitution does not duplicate its terms**
+/// — the one place `TypedExpr`'s freshening `Clone` is deliberately opted out
+/// of, and the reason it can be opted out of exactly here.
+///
+/// A `Discharge` payload is a **template**, not a tree node. It is cloned again
+/// at every read ([`Mapping::as_expr`] / [`as_expr_preserving`]), and *that*
+/// read is where the sibling gets minted, once per occurrence actually filled.
+/// So copying the map itself must mint nothing: the template is never in a tree,
+/// and no two nodes can end up sharing an id because of it.
+///
+/// Without this, every `Subst` copy inherits the freshening and re-mints its
+/// payloads. The solver copies substitutions constantly — `Bound::render_subst`,
+/// [`Subst::then`], `compact`, `constrain` — and a bound edge's payloads are **type-domain**
+/// terms whose ids no step ever produced, so each such copy records a `Copy`
+/// against an origin the log never saw and the pane fold reports it as
+/// [`Leak::CopyOfUnknown`](crate::ccl::lineage::Leak::CopyOfUnknown). Measured on
+/// `generator_pipeline`: 200 of them at the first pane boundary.
+///
+/// [`as_expr_preserving`]: Mapping::as_expr_preserving
+impl Clone for Mapping {
+    fn clone(&self) -> Self {
+        match self {
+            Mapping::Rename(b) => Mapping::Rename(b.clone()),
+            Mapping::Discharge(t) => Mapping::Discharge(Box::new(t.clone_preserving_ids())),
+        }
+    }
+}
+
 /// A substitution must never leave a **typed** occurrence holding an untyped
 /// replacement.
 ///
@@ -110,8 +153,10 @@ fn assert_preserves_typedness(replacement: &TypedExpr, occurrence_ty: &Type) {
 
 impl Mapping {
     /// The mapping's replacement as a term (a `Rename` materializes as a bare
-    /// variable reference). The replacement carries a **new** identity: a fresh
-    /// mint for a `Rename`, the discharged term's own ids for a `Discharge`.
+    /// variable reference). The replacement carries a **new** identity
+    /// throughout: a fresh mint for a `Rename`, and — since `Clone` freshens —
+    /// a wholly fresh node-set for a `Discharge`, rather than the template's own
+    /// ids duplicated into every occurrence it fills.
     fn as_expr(&self, occurrence_ty: &Type) -> TypedExpr {
         let out = match self {
             // α-renaming cannot change a term's type: the occurrence's type is a
@@ -127,22 +172,49 @@ impl Mapping {
         out
     }
 
-    /// [`as_expr`](Self::as_expr) at a **preserved** root identity: the
-    /// replacement root takes `node_id` — the occurrence's own id — so it
-    /// inherits the use-site's span and attribution.
+    /// [`as_expr`](Self::as_expr) at the **occurrence's own identity**: the
+    /// replacement's root takes `node_id`, so attribution at that position stays
+    /// the use site's rather than becoming the template's.
     ///
     /// A `Rename` is built directly at `node_id` rather than minted and then
     /// overwritten: a mint fires `on_mint`, and an id no node ends up carrying is
-    /// a phantom birth in the lineage log. A `Discharge` clones (which mints
-    /// nothing) and re-roots that clone
-    /// ([`re_root`](TypedExpr::re_root)) — the two shapes reach a preserved
-    /// identity by different routes, and neither mints.
+    /// a phantom birth in the lineage log.
+    ///
+    /// A `Discharge` is the crate's one copy that shares an id; the literal below
+    /// carries why.
     fn as_expr_preserving(&self, node_id: NodeId, occurrence_ty: &Type) -> TypedExpr {
         let out = match self {
             // See [`as_expr`]: the rename keeps the occurrence's type.
             Mapping::Rename(to) => TypedExpr::preserve(node_id, TypedExprNode::Var(to.clone()))
                 .with_ty(occurrence_ty.clone()),
-            Mapping::Discharge(t) => (**t).clone().re_root(node_id),
+            // The root takes the occurrence's id, the interior freshens
+            // (`node.clone()` reaches each child's own `Clone`): N occurrences give
+            // N subtrees under N ids the tree already holds. The id is what
+            // attribution resolves through, and a lowered parameter use is the case
+            // that shows it — uncurry substitutes a machine-made tuple projection
+            // into every use of `a` in `def add(a, b): a + a + b`, so a freshened
+            // root resolves through that template, whose span is the whole `def`
+            // and whose nature is machinery, and all three uses report the header
+            // instead of their own columns.
+            //
+            // A literal rather than `preserve(node_id, …).with_ty(…)`: the
+            // exhaustive field check is what keeps `user_annotation` from being
+            // silently dropped.
+            //
+            // TODO(subst-lineage): the edge encoding reproduces this entry, span
+            // and nature alike — freshen the root and record the copy against the
+            // occurrence instead of the template. It costs a death per occurrence,
+            // and the record has to land in the enclosing frame, since a nested one
+            // flushes first (guards drop LIFO) and would order these edges ahead of
+            // the copy that introduced the template they read. Revisit when the
+            // pane-level table lands and the two become distinguishable from
+            // outside this function.
+            Mapping::Discharge(t) => TypedExpr {
+                ty: t.ty.clone(),
+                node: t.node.clone(),
+                user_annotation: t.user_annotation.clone(),
+                node_id,
+            },
         };
         assert_preserves_typedness(&out, occurrence_ty);
         out
@@ -650,22 +722,6 @@ impl Subst {
             // construction.
             let occurrence_ty = e.ty.clone();
             *e = repl.as_expr_preserving(e.node_id, &occurrence_ty);
-            if !matches!(e.node, TypedExprNode::Var(_)) {
-                // Compound replacement: `as_expr_preserving` bare-`clone()`s the
-                // whole subtree, sharing the source's NodeIds. Freshen only the
-                // INTERIOR (the children) — the root keeps the carried id. Each
-                // interior re-mint fires the ambient `on_copy` lineage hook into
-                // any open step. Type slots are out of the id domain, so the
-                // predicate `Rc`s the clone shares with its source stay shared.
-                //
-                // Freshening the root as well would work, but it re-mints an id
-                // the carry immediately overwrites, so the step records a `Copy`
-                // whose produced id no node ends up holding. The node survives
-                // either way — only its recorded identity would be one the tree
-                // never keeps — so this is about not logging an operation that is
-                // undone a line later, and about spending one fewer id.
-                e.freshen_interior_node_ids();
-            }
             return;
         }
         // *Every* type slot the node carries, not just `ty` and the annotation: a
diff --git a/src/ccl/transact_phase.rs b/src/ccl/transact_phase.rs
index b9f08197..4004062b 100644
--- a/src/ccl/transact_phase.rs
+++ b/src/ccl/transact_phase.rs
@@ -165,11 +165,13 @@ fn drop_dead_as_of_reads(e: &mut Expr) {
         binding,
         bound_expr,
         body,
-    } = &e.node
+    } = &mut e.node
         && as_of_read_source(bound_expr).is_some()
         && !is_free_in_value(&binding.name, body)
     {
-        *e = (**body).clone();
+        // The body takes the dropped `let`'s position: a move, not a duplication.
+        let body = std::mem::take(&mut **body);
+        *e = body;
         drop_dead_as_of_reads(e);
         return;
     }
@@ -2335,6 +2337,9 @@ fn subst_env(e: &Expr, env: &HashMap<Name, Expr>) -> Expr {
     if let TypedExprNode::Var(n) = &e.node
         && let Some(rep) = env.get(n)
     {
+        // Root-carry: the replacement denotes what the `Var` denoted — the value
+        // of `n` *here* — so the read site keeps its own id, and with it its
+        // span/attribution. N reads give N distinct roots.
         return rep.clone();
     }
     let mut out = e.clone();
@@ -2350,7 +2355,10 @@ fn collect_key_inits(expr: &Expr, keys: &[Name], out: &mut HashMap<Name, Expr>)
         && keys.contains(&binding.name)
         && !out.contains_key(&binding.name)
     {
-        out.insert(binding.name.clone(), (**init).clone());
+        // A stash, not a duplication: the `let` that held this init is dropped
+        // rather than kept alongside, so preserving its ids is what makes the
+        // later placements copies **of the original**.
+        out.insert(binding.name.clone(), init.clone_preserving_ids());
     }
     expr.walk_children(|c| collect_key_inits(c, keys, out));
 }
@@ -2718,7 +2726,7 @@ fn plan_store(
         let v = value_ty(k);
         let reg_k = hist[k].clone();
         let t = Name::fresh("__t");
-        let init = key_init.get(k).cloned().expect("key init present");
+        let init = key_init.get(k).expect("key init present").clone();
         // The `get_prev_txn` history slot — the design's denotation: the
         // `⧺`-merged **per-key commit views** of every site writing this key
         // ("multiple writer sites for one variable merge their commit
diff --git a/src/ccl/uniquify.rs b/src/ccl/uniquify.rs
index 4a647301..9abfb988 100644
--- a/src/ccl/uniquify.rs
+++ b/src/ccl/uniquify.rs
@@ -344,9 +344,9 @@ impl Uniquifier {
 /// result order-independent so the before/after comparison checks set identity
 /// with 1:1 multiplicity, not traversal order.
 ///
-/// This domain is deliberately **broader than the `NodeId` domain** (the
-/// `walk_children` node-set — see `design/provenance.md`, "The id domain"): the
-/// property checked here is not uniqueness but *preservation*, and predicate
+/// This domain is **broader than the uniqueness walk**'s `walk_children` node-set
+/// (see `design/provenance.md`, "Walking the ids"): the
+/// property checked here is not uniqueness but preservation, and predicate
 /// interiors are in scope precisely because uniquify rebuilds those terms through
 /// a [`PredMemo`], which is where a rebuild could drop or re-mint an id. Do not
 /// narrow it to match the freshen walks — they are checking different things.
@@ -608,7 +608,8 @@ mod tests {
     #[test]
     fn idempotent_on_minted_trees() {
         let expr = pipeline_front("k = 1\n[x for x in [1, 2, 3] if x > k]\n");
-        let again = run(expr.clone());
+        // The second run must see the same nodes, not a freshened copy of them.
+        let again = run(expr.clone_preserving_ids());
         assert_eq!(expr, again, "uniquify must be idempotent");
     }
 
diff --git a/tests/compilation_pipeline/feeds_cases.rs b/tests/compilation_pipeline/feeds_cases.rs
index e41078e6..9025389c 100644
--- a/tests/compilation_pipeline/feeds_cases.rs
+++ b/tests/compilation_pipeline/feeds_cases.rs
@@ -22,6 +22,18 @@ r#"x = defer()
 for i in [1,2,3]:
   x << i
 x"#, make_int_list(&[1, 2, 3]))]
+// Two feeds inside one read-only `with begin():` block: the letrec phase's
+// feed-only path emits one `Feed` per feed, each mapping the same loop source, so
+// the source lands at two live positions and must be freshened per placement — a
+// bare clone trips the `post-letrec-run` id-uniqueness boundary.
+#[case::two_feeds_in_readonly_txn_loop(
+r#"x = defer()
+y = defer()
+for i in [1,2,3]:
+  with begin():
+    x << i
+    y << i
+x"#, make_int_list(&[1, 2, 3]))]
 // Filter-feed inside a defer: `if cond: d << v` in a loop lowers to a
 // refined-source channel whose domain carries the bare predicate
 // `__elem ▷ source ▷ (λ p → guard)` (the same element form a filtered
diff --git a/tests/compilation_pipeline/generators_udf_poly.rs b/tests/compilation_pipeline/generators_udf_poly.rs
index 20d7bdd2..1fa23bdb 100644
--- a/tests/compilation_pipeline/generators_udf_poly.rs
+++ b/tests/compilation_pipeline/generators_udf_poly.rs
@@ -99,7 +99,7 @@ fn test_polymorphic_udf_calls_differing_only_in_a_literal(
 // Same generator, but its result is *bound* to a variable before use
 // (`y = doubles(...)` then `y`) rather than called inline. `inline` expands
 // the call to `let y = (let __result = defer in … __result) in y`, and
-// `channelize::try_lift_defer` lifts the inner result-defer scope out so the
+// `channelize::lift_defer` lifts the inner result-defer scope out so the
 // feeds land on `y`. The inline form above never reaches that path, so this
 // case is its regression guard.
 #[case(
@@ -111,7 +111,7 @@ fn test_polymorphic_udf_calls_differing_only_in_a_literal(
 // becomes `let y = (let z = <doubles inlined> in z) in y` — the inner
 // bound-expr contains a defer but is not itself `Defer`, so
 // `channelize`'s defer-returning-let *collapse* fires (surfacing the inner
-// defer for a subsequent `try_lift_defer`). Regression guard for that path.
+// defer for a subsequent `lift_defer`). Regression guard for that path.
 #[case(
     "def doubles(xs):\n    for x in xs:\n        yield x * 2\ndef wrap(xs):\n    z = doubles(xs)\n    z\ny = wrap([1, 2, 3])\ny",
     make_int_list(&[2, 4, 6])