diff --git a/differential/corpus/programs/projection_cut.mm2 b/differential/corpus/programs/projection_cut.mm2
new file mode 100644
index 00000000..eb4bc1f2
--- /dev/null
+++ b/differential/corpus/programs/projection_cut.mm2
@@ -0,0 +1,52 @@
+;; @expect
+;; @steps  20
+;; @desc   Variables no template reads: the engines may answer them with one witness instead of
+;; @desc   enumerating their domain, but only where that cannot change the answer set. Each block
+;; @desc   below is a shape the projection cut must get right; the expected space pins all of them.
+
+;; --- 1. A trailing don't-care with fan-out. `$_` is mentioned once and no template reads it, so
+;; every value past the first re-derives `(out1 a)`. One row per `r`, whatever the fan-out.
+(r a)
+(r b)
+(s a p)
+(s a q)
+(s a t)
+(s b t)
+(exec 0 (, (r $x) (s $x $_)) (, (out1 $x)))
+
+;; --- 2. Schematic data. A don't-care may witness a term that itself contains variables; the
+;; answer must not depend on which witness the engine happened to reach first.
+(sv k plain)
+(sv k (f $z))
+(sv k (g $w $v))
+(exec 1 (, (sv $y $_) ) (, (out2 $y)))
+
+;; --- 3. A don't-care that is NOT trailing. `$m` decides which `(gg $m $n)` subtrie `$n` is drawn
+;; from, so pinning it would drop answers rather than duplicates: every `$n` must survive.
+(gg p 1)
+(gg p 2)
+(gg q 3)
+(exec 2 (, (gg $m $n)) (, (out3 $n)))
+
+;; --- 4. The same, one level down: the don't-care sits inside a compound, still not trailing.
+(hh (kk p 1))
+(hh (kk p 2))
+(hh (kk q 3))
+(exec 3 (, (hh (kk $mm $nn))) (, (out4 $nn)))
+
+;; --- 5. A repeated variable no template reads is a JOIN variable, not a don't-care: it still has
+;; to intersect, so `(out5 ...)` holds only the values `jl` and `jr` agree on.
+(jl 1)
+(jl 2)
+(jl 3)
+(jr 2)
+(jr 3)
+(jr 4)
+(je 2)
+(exec 4 (, (jl $p) (jr $p) (je $q)) (, (out5 $q)))
+
+;; --- 6. An O-form whose pattern carries a don't-care guard. The guard must keep gating: the
+;; counter decrements once per step while `(wanted t)` exists, and stops when it no longer does.
+(wanted t)
+(counter (S (S (Z))))
+(exec 5 (, (exec 5 $a $b) (wanted $c) (counter (S $d))) (O (+ (exec 5 $a $b)) (+ (counter $d)) (- (counter (S $d)))))
diff --git a/differential/corpus/programs/projection_cut_aliased.mm2 b/differential/corpus/programs/projection_cut_aliased.mm2
new file mode 100644
index 00000000..4f041ac6
--- /dev/null
+++ b/differential/corpus/programs/projection_cut_aliased.mm2
@@ -0,0 +1,53 @@
+;; @expect
+;; @steps  30
+;; @desc   Data-side aliasing: facts whose own variable ties the don't-care column to a column a
+;; @desc   template reads. The query-side rule (mentioned once, unread, trailing) says nothing
+;; @desc   about the DATA sharing a variable across those columns, so each shape is pinned here.
+;; @desc
+;; @desc   Why it is sound: a bare fresh singleton is an unconstrained position, so whichever
+;; @desc   stored subterm it meets, the binding is read by nothing and constrains nothing else.
+;; @desc   What could still discriminate is a LATER query position drawing from the subtrie the
+;; @desc   choice selected -- and the trailing condition is exactly what excludes that. The
+;; @desc   discriminating information in these shapes lives in the repeated column, which is a
+;; @desc   trie PREFIX of the don't-care column, so it is enumerated before the cut applies.
+
+;; 1. the tail aliases the first column; the facts differ at the REPEATED column, so `$a` must
+;;    still iterate over both A and B
+(f1 $x A $x)
+(f1 $x B $x)
+(exec (0 1) (, (f1 $a $a $_)) (, (o1 $a)))
+
+;; 2. the facts differ at the DON'T-CARE column instead, and `$a` stays free
+(f2 $x $x A)
+(f2 $x $x B)
+(exec (0 2) (, (f2 $a $a $_)) (, (o2 $a)))
+
+;; 3. the don't-care column mixes a back-reference with a ground term
+(f3 $x $x $x)
+(f3 $x $x A)
+(exec (0 3) (, (f3 $a $a $_)) (, (o3 $a)))
+
+;; 4. the read variable is pinned by the FIRST column, with an alias in the tail
+(f4 A $x $x)
+(f4 B $x $x)
+(exec (0 4) (, (f4 $a $a $_)) (, (o4 $a)))
+
+;; 5. two trailing don't-cares, both aliased to the read variable
+(f5 $x A $x $x)
+(f5 $x B $x $x)
+(exec (0 5) (, (f5 $a $a $_ $_2)) (, (o5 $a)))
+
+;; 6. the don't-care sits in the MIDDLE, so it is not cuttable at all
+(f6 $x A $x)
+(f6 $x B $x)
+(exec (0 6) (, (f6 $c $_ $c)) (, (o6 $c)))
+
+;; 7. the don't-care's subterm carries structure over the shared variable
+(f7 $x $x (g $x))
+(f7 $x $x (h $x))
+(exec (0 7) (, (f7 $a $a $_)) (, (o7 $a)))
+
+;; 8. a read variable pinned only via the repeated column, with the tail aliasing it
+(f8 $x $x A $x)
+(f8 $x $x B $x)
+(exec (0 8) (, (f8 $a $a $b $_)) (, (o8 $a $b)))
diff --git a/differential/corpus/programs/transform_decomposition.mm2 b/differential/corpus/programs/transform_decomposition.mm2
new file mode 100644
index 00000000..bcc71ea1
--- /dev/null
+++ b/differential/corpus/programs/transform_decomposition.mm2
@@ -0,0 +1,70 @@
+;; @expect
+;; @steps  40
+;; @desc   Decomposition lowerings, each computed BOTH ways so the expected space pins the
+;; @desc   staged form equal to the naive one: a 6-cycle split into two bags, a 4-clique staged
+;; @desc   through triangles, and the wiki Reachability-P2 crafting join reduced per ingredient
+;; @desc   side. A divergence in any of them changes this program's space.
+
+;; ---------------------------------------------------------------- 6-cycle, ghw 2 < rho* 3
+(e a b)
+(e b c)
+(e c d)
+(e d f)
+(e f g)
+(e g a)
+(e a c)
+(e c f)
+(e f a)
+(exec (0 0) (, (e $a $b) (e $b $c) (e $c $d) (e $d $f) (e $f $g) (e $g $a)) (, (cycN $a)))
+;; two bags of three edges; the first is materialised as its PROJECTED endpoints, which is what
+;; shares the suffix across every binding of the discarded middle variables
+(exec (1 0) (, (e $a $b) (e $b $c) (e $c $d)) (, (p3 $a $d)))
+(exec (1 1) (, (p3 $a $d) (e $d $f) (e $f $g) (e $g $a)) (, (cycS $a)))
+
+;; ---------------------------------------------------------------- 4-clique
+(edge n0 n1)
+(edge n0 n2)
+(edge n0 n3)
+(edge n1 n2)
+(edge n1 n3)
+(edge n2 n3)
+(edge n1 n4)
+(edge n2 n4)
+(exec (2 0) (, (edge $x0 $x1) (edge $x0 $x2) (edge $x0 $x3)
+                (edge $x1 $x2) (edge $x1 $x3) (edge $x2 $x3))
+            (, (c4N $x0 $x1 $x2 $x3)))
+;; staged through the triangle bag. Every variable is named by the template, so nothing is
+;; projected away and leapfrog has nothing to share -- kept as the contrast to the 6-cycle.
+(exec (3 0) (, (edge $x0 $x1) (edge $x0 $x2) (edge $x1 $x2)) (, (tri $x0 $x1 $x2)))
+(exec (3 1) (, (tri $x0 $x1 $x2) (edge $x0 $x3) (edge $x1 $x3) (edge $x2 $x3))
+            (, (c4S $x0 $x1 $x2 $x3)))
+
+;; ---------------------------------------------------------------- crafting (wiki P2 exec (1 3))
+(recipe r0 (numIngredients 2))
+(recipe r0 (result (id itemA)))
+(recipe r0 (pattern 0 sx0))
+(recipe r0 (pattern 1 sy0))
+(recipe r0 (key (sx0 wood)))
+(recipe r0 (key (sx0 stone)))
+(recipe r0 (key (sy0 coal)))
+(recipe r1 (numIngredients 2))
+(recipe r1 (result (id itemB)))
+(recipe r1 (pattern 0 sx1))
+(recipe r1 (pattern 1 sy1))
+(recipe r1 (key (sx1 gold)))
+(recipe r1 (key (sy1 missing)))
+(inventory wood)
+(inventory stone)
+(inventory coal)
+(inventory gold)
+(exec (4 0) (, (recipe $p (numIngredients 2)) (recipe $p (result (id $n)))
+                (recipe $p (pattern 0 $x)) (recipe $p (key ($x $xi)))
+                (recipe $p (pattern 1 $y)) (recipe $p (key ($y $yi)))
+                (inventory $xi) (inventory $yi))
+            (, (craftN $n)))
+;; each ingredient side is satisfiable independently given the recipe, and everything but the
+;; product name is projected away: reduce each side to a witness on $p, then combine
+(exec (5 0) (, (recipe $p (pattern 0 $x)) (recipe $p (key ($x $xi))) (inventory $xi)) (, (ok0 $p)))
+(exec (5 1) (, (recipe $p (pattern 1 $y)) (recipe $p (key ($y $yi))) (inventory $yi)) (, (ok1 $p)))
+(exec (5 2) (, (recipe $p (numIngredients 2)) (ok0 $p) (ok1 $p) (recipe $p (result (id $n))))
+            (, (craftS $n)))
diff --git a/differential/corpus/programs/transform_process_calculus.mm2 b/differential/corpus/programs/transform_process_calculus.mm2
new file mode 100644
index 00000000..87f676dc
--- /dev/null
+++ b/differential/corpus/programs/transform_process_calculus.mm2
@@ -0,0 +1,66 @@
+;; @expect
+;; @steps  60
+;; @desc   The process calculus lowered three ways over the same soup, so the expected space pins
+;; @desc   all three to the same final message: monotone naive, delta on the message side, and
+;; @desc   consuming (the reagents are retired). The naive rule never removes, so it re-derives
+;; @desc   every past communication on every round -- quadratic in the cascade length.
+
+;; a cascade: each receiver forwards to the next channel
+(pN (? c0 p0 (! c1 p1)))
+(pN (? c1 p1 (! c2 p2)))
+(pN (? c2 p2 (! c3 p3)))
+(pN (? c3 p3 (! r0 q0)))
+(pN (? r0 q0 (? r1 q1 (! deep ok))))
+(pN (? r1 q1 (! early seen)))
+(pN (! r1 q1))
+(pN (! c0 p0))
+(pD (? c0 p0 (! c1 p1)))
+(pD (? c1 p1 (! c2 p2)))
+(pD (? c2 p2 (! c3 p3)))
+(pD (? c3 p3 (! r0 q0)))
+(pD (? r0 q0 (? r1 q1 (! deep ok))))
+(pD (? r1 q1 (! early seen)))
+(pD (! r1 q1))
+(pD (! c0 p0))
+(dD (? c0 p0 (! c1 p1)))
+(dD (? c1 p1 (! c2 p2)))
+(dD (? c2 p2 (! c3 p3)))
+(dD (? c3 p3 (! r0 q0)))
+(dD (? r0 q0 (? r1 q1 (! deep ok))))
+(dD (? r1 q1 (! early seen)))
+(dD (! r1 q1))
+(dD (! c0 p0))
+(pC (? c0 p0 (! c1 p1)))
+(pC (? c1 p1 (! c2 p2)))
+(pC (? c2 p2 (! c3 p3)))
+(pC (? c3 p3 (! r0 q0)))
+(pC (? r0 q0 (? r1 q1 (! deep ok))))
+(pC (? r1 q1 (! early seen)))
+(pC (! r1 q1))
+(pC (! c0 p0))
+(fN (S (S (S (S (S (S Z)))))))
+(fD (S (S (S (S (S (S Z)))))))
+(fC (S (S (S (S (S (S Z)))))))
+
+;; (a) monotone: nothing retired, so round k re-derives all k-1 earlier communications
+(exec (1 Z) (, (exec (1 $l) $p $t) (fN (S $k)) (pN (? $c $pl $b)) (pN (! $c $pl)))
+            (O (+ (exec (1 (S $l)) $p $t)) (+ (pN $b)) (+ (fN $k)) (- (fN (S $k)))))
+
+;; (b) SYMMETRIC delta. A self-join over one relation needs both arms: new receivers against
+;; every message, and every receiver against new messages. With only the second, a communication
+;; that derives a RECEIVER never reacts with a message already in the soup -- which is what the
+;; (? r0 ..) pair above is here to catch.
+((armD 0) (, (dD (? $c $pl $b)) (pD (! $c $pl)))
+          (O (+ (pD $b)) (+ (dD $b)) (- (dD (? $c $pl $b)))))
+((armD 1) (, (pD (? $c $pl $b)) (dD (! $c $pl)))
+          (O (+ (pD $b)) (+ (dD $b)) (- (dD (! $c $pl)))))
+(exec (2 (IC 0 1 (S (S (S (S (S (S (S (S (S (S Z))))))))))))
+      (, (exec (2 (IC $x $y (S $c))) $sp $st) ((armD $x) $p $t))
+      (, (exec (2 (IC $y $x $c)) $sp $st) (exec (2 (R $x)) $p $t)))
+
+;; (c) consuming: the reagents are retired, so no intermediate is ever kept and the
+;; re-derivation is removed at its source rather than filtered afterwards
+(exec (3 Z) (, (exec (3 $l) $p $t) (fC (S $k)) (pC (? $c $pl $b)) (pC (! $c $pl)))
+            (O (+ (exec (3 (S $l)) $p $t)) (+ (pC $b))
+               (- (pC (? $c $pl $b))) (- (pC (! $c $pl)))
+               (+ (fC $k)) (- (fC (S $k)))))
diff --git a/differential/corpus/programs/transform_staging.mm2 b/differential/corpus/programs/transform_staging.mm2
new file mode 100644
index 00000000..d56468d7
--- /dev/null
+++ b/differential/corpus/programs/transform_staging.mm2
@@ -0,0 +1,65 @@
+;; @expect
+;; @steps  60
+;; @desc   The two source-level transforms, each computed BOTH ways in one program so the
+;; @desc   expected space pins them equal: a chain query naively and Yannakakis-staged, and a
+;; @desc   transitive closure naively and semi-naively. If a staging ever stops agreeing with the
+;; @desc   form it replaces, this program's space changes.
+
+;; ---------------------------------------------------------------- the chain query R-S-T
+(R a p)
+(R b p)
+(R c q)
+(R d r)
+(S p u)
+(S p v)
+(S q u)
+(S r dead)
+(T u m)
+(T v n)
+
+;; naive: one join over all three relations
+(exec (0 0) (, (R $x $y) (S $y $z) (T $z $w)) (, (outN $x $w)))
+
+;; Yannakakis-staged: project, semi-join bottom-up, semi-join top-down, then join the reduced
+;; relations. Every projection is `(, (Rel $key $_))` -- the shape the projection cut answers
+;; with one witness per key -- which is why the reduced relations are emitted KEY-FIRST: a
+;; projection off a key-last relation would be `(, (Rel $_ $key))`, where the don't-care is not
+;; trailing and must keep enumerating.
+(exec (1 0) (, (T $z $_))            (, (Tz $z)))
+(exec (1 1) (, (S $y $z) (Tz $z))    (, (S1 $y $z)))
+(exec (1 2) (, (S1 $y $_))           (, (S1y $y)))
+(exec (1 3) (, (R $x $y) (S1y $y))   (, (R1 $y $x)))
+(exec (1 4) (, (R1 $y $_))           (, (R1y $y)))
+(exec (1 5) (, (S1 $y $z) (R1y $y))  (, (S2 $z $y)))
+(exec (1 6) (, (S2 $z $_))           (, (S2z $z)))
+(exec (1 7) (, (T $z $w) (S2z $z))   (, (T1 $z $w)))
+(exec (1 8) (, (R1 $y $x) (S2 $z $y) (T1 $z $w)) (, (outS $x $w)))
+
+;; ---------------------------------------------------------------- transitive closure
+(edge g0 g1)
+(edge g1 g2)
+(edge g2 g3)
+(edge g3 g4)
+
+;; NOTE on loc ordering: execs run in byte order of the whole atom, and a SYMBOL loc sorts
+;; above a COMPOUND one -- `(exec (2 0) ..)` would run AFTER `(exec (2 (1 Z)) ..)`, so the seed
+;; would fire after the loop and the loop would see an empty relation. Every loc here is the
+;; same shape so the intended order is the numeric one.
+;;
+;; Both loops carry Peano fuel. A self-reproducing exec has no termination condition of its own,
+;; so an unbounded one would monopolise every remaining step and the family after it would never
+;; run at all.
+(fuelN (S (S (S (S (S Z))))))
+(fuelD (S (S (S (S (S Z))))))
+
+;; naive: every iteration re-joins the WHOLE path relation with edge
+(exec (2 (0 0)) (, (edge $x $y)) (, (pathN $x $y)))
+(exec (2 (1 Z)) (, (exec (2 (1 $l)) $p $t) (fuelN (S $k)) (pathN $x $y) (edge $y $z))
+                (O (+ (exec (2 (1 (S $l))) $p $t)) (+ (pathN $x $z))
+                   (+ (fuelN $k)) (- (fuelN (S $k)))))
+
+;; semi-naive: every iteration joins only the frontier the previous one produced
+(exec (3 (0 0)) (, (edge $x $y)) (, (front Z $x $y) (pathD $x $y)))
+(exec (3 (1 Z)) (, (exec (3 (1 $l)) $p $t) (fuelD (S $k)) (front $l $x $y) (edge $y $z))
+                (O (+ (exec (3 (1 (S $l))) $p $t)) (+ (front (S $l) $x $z)) (+ (pathD $x $z))
+                   (+ (fuelD $k)) (- (fuelD (S $k)))))
diff --git a/differential/expected/programs/projection_cut.expected b/differential/expected/programs/projection_cut.expected
new file mode 100644
index 00000000..cc336bae
--- /dev/null
+++ b/differential/expected/programs/projection_cut.expected
@@ -0,0 +1,34 @@
+(r a)
+(r b)
+(hh (kk p 1))
+(hh (kk p 2))
+(hh (kk q 3))
+(je 2)
+(jl 1)
+(jl 2)
+(jl 3)
+(jr 2)
+(jr 3)
+(jr 4)
+(out1 a)
+(out1 b)
+(out2 k)
+(out3 1)
+(out3 2)
+(out3 3)
+(out4 1)
+(out4 2)
+(out4 3)
+(out5 2)
+(wanted t)
+(counter (Z))
+(s a p)
+(s a q)
+(s a t)
+(s b t)
+(gg p 1)
+(gg p 2)
+(gg q 3)
+(sv k (f $a))
+(sv k (g $a $b))
+(sv k plain)
diff --git a/differential/expected/programs/projection_cut_aliased.expected b/differential/expected/programs/projection_cut_aliased.expected
new file mode 100644
index 00000000..eefc83ea
--- /dev/null
+++ b/differential/expected/programs/projection_cut_aliased.expected
@@ -0,0 +1,28 @@
+(o1 A)
+(o1 B)
+(o2 $a)
+(o3 $a)
+(o4 A)
+(o4 B)
+(o5 A)
+(o5 B)
+(o6 $a)
+(o7 $a)
+(o8 $a A)
+(o8 $a B)
+(f1 $a A $a)
+(f1 $a B $a)
+(f2 $a $a A)
+(f2 $a $a B)
+(f3 $a $a $a)
+(f3 $a $a A)
+(f4 A $a $a)
+(f4 B $a $a)
+(f6 $a A $a)
+(f6 $a B $a)
+(f7 $a $a (g $a))
+(f7 $a $a (h $a))
+(f5 $a A $a $a)
+(f5 $a B $a $a)
+(f8 $a $a A $a)
+(f8 $a $a B $a)
diff --git a/differential/expected/programs/transform_decomposition.expected b/differential/expected/programs/transform_decomposition.expected
new file mode 100644
index 00000000..8cc7915d
--- /dev/null
+++ b/differential/expected/programs/transform_decomposition.expected
@@ -0,0 +1,79 @@
+(ok0 r0)
+(ok0 r1)
+(ok1 r0)
+(cycN a)
+(cycN b)
+(cycN c)
+(cycN d)
+(cycN f)
+(cycN g)
+(cycS a)
+(cycS b)
+(cycS c)
+(cycS d)
+(cycS f)
+(cycS g)
+(craftN itemA)
+(craftS itemA)
+(inventory coal)
+(inventory gold)
+(inventory wood)
+(inventory stone)
+(e a b)
+(e a c)
+(e b c)
+(e c d)
+(e c f)
+(e d f)
+(e f a)
+(e f g)
+(e g a)
+(p3 a a)
+(p3 a d)
+(p3 a f)
+(p3 a g)
+(p3 b a)
+(p3 b f)
+(p3 b g)
+(p3 c a)
+(p3 c b)
+(p3 c c)
+(p3 c g)
+(p3 d a)
+(p3 d b)
+(p3 d c)
+(p3 f b)
+(p3 f c)
+(p3 f d)
+(p3 f f)
+(p3 g c)
+(p3 g d)
+(p3 g f)
+(edge n0 n1)
+(edge n0 n2)
+(edge n0 n3)
+(edge n1 n2)
+(edge n1 n3)
+(edge n1 n4)
+(edge n2 n3)
+(edge n2 n4)
+(recipe r0 (key (sx0 wood)))
+(recipe r0 (key (sx0 stone)))
+(recipe r0 (key (sy0 coal)))
+(recipe r0 (result (id itemA)))
+(recipe r0 (numIngredients 2))
+(recipe r0 (pattern 0 sx0))
+(recipe r0 (pattern 1 sy0))
+(recipe r1 (key (sx1 gold)))
+(recipe r1 (key (sy1 missing)))
+(recipe r1 (result (id itemB)))
+(recipe r1 (numIngredients 2))
+(recipe r1 (pattern 0 sx1))
+(recipe r1 (pattern 1 sy1))
+(tri n0 n1 n2)
+(tri n0 n1 n3)
+(tri n0 n2 n3)
+(tri n1 n2 n3)
+(tri n1 n2 n4)
+(c4N n0 n1 n2 n3)
+(c4S n0 n1 n2 n3)
diff --git a/differential/expected/programs/transform_process_calculus.expected b/differential/expected/programs/transform_process_calculus.expected
new file mode 100644
index 00000000..ed49c5e4
--- /dev/null
+++ b/differential/expected/programs/transform_process_calculus.expected
@@ -0,0 +1,39 @@
+(dD (! deep ok))
+(dD (! early seen))
+(fC (S Z))
+(fD (S (S (S (S (S (S Z)))))))
+(fN Z)
+(pC (! early seen))
+(pC (? r1 q1 (! deep ok)))
+(pD (! c0 p0))
+(pD (! c1 p1))
+(pD (! c2 p2))
+(pD (! c3 p3))
+(pD (! r0 q0))
+(pD (! r1 q1))
+(pD (! deep ok))
+(pD (! early seen))
+(pD (? c0 p0 (! c1 p1)))
+(pD (? c1 p1 (! c2 p2)))
+(pD (? c2 p2 (! c3 p3)))
+(pD (? c3 p3 (! r0 q0)))
+(pD (? r0 q0 (? r1 q1 (! deep ok))))
+(pD (? r1 q1 (! deep ok)))
+(pD (? r1 q1 (! early seen)))
+(pN (! c0 p0))
+(pN (! c1 p1))
+(pN (! c2 p2))
+(pN (! c3 p3))
+(pN (! r0 q0))
+(pN (! r1 q1))
+(pN (! deep ok))
+(pN (! early seen))
+(pN (? c0 p0 (! c1 p1)))
+(pN (? c1 p1 (! c2 p2)))
+(pN (? c2 p2 (! c3 p3)))
+(pN (? c3 p3 (! r0 q0)))
+(pN (? r0 q0 (? r1 q1 (! deep ok))))
+(pN (? r1 q1 (! deep ok)))
+(pN (? r1 q1 (! early seen)))
+((armD 0) (, (dD (? $a $b $c)) (pD (! $a $b))) (O (+ (pD $c)) (+ (dD $c)) (- (dD (? $a $b $c)))))
+((armD 1) (, (pD (? $a $b $c)) (dD (! $a $b))) (O (+ (pD $c)) (+ (dD $c)) (- (dD (! $a $b)))))
diff --git a/differential/expected/programs/transform_staging.expected b/differential/expected/programs/transform_staging.expected
new file mode 100644
index 00000000..856e1ffd
--- /dev/null
+++ b/differential/expected/programs/transform_staging.expected
@@ -0,0 +1,75 @@
+(Tz u)
+(Tz v)
+(R1y p)
+(R1y q)
+(S1y p)
+(S1y q)
+(S2z u)
+(S2z v)
+(fuelD (S (S Z)))
+(fuelN Z)
+(R a p)
+(R b p)
+(R c q)
+(R d r)
+(S p u)
+(S p v)
+(S q u)
+(S r dead)
+(T u m)
+(T v n)
+(R1 p a)
+(R1 p b)
+(R1 q c)
+(S1 p u)
+(S1 p v)
+(S1 q u)
+(S2 u p)
+(S2 u q)
+(S2 v p)
+(T1 u m)
+(T1 v n)
+(edge g0 g1)
+(edge g1 g2)
+(edge g2 g3)
+(edge g3 g4)
+(outN a m)
+(outN a n)
+(outN b m)
+(outN b n)
+(outN c m)
+(outS a m)
+(outS a n)
+(outS b m)
+(outS b n)
+(outS c m)
+(pathD g0 g1)
+(pathD g0 g2)
+(pathD g0 g3)
+(pathD g0 g4)
+(pathD g1 g2)
+(pathD g1 g3)
+(pathD g1 g4)
+(pathD g2 g3)
+(pathD g2 g4)
+(pathD g3 g4)
+(pathN g0 g1)
+(pathN g0 g2)
+(pathN g0 g3)
+(pathN g0 g4)
+(pathN g1 g2)
+(pathN g1 g3)
+(pathN g1 g4)
+(pathN g2 g3)
+(pathN g2 g4)
+(pathN g3 g4)
+(front (S (S (S Z))) g0 g4)
+(front (S (S Z)) g0 g3)
+(front (S (S Z)) g1 g4)
+(front (S Z) g0 g2)
+(front (S Z) g1 g3)
+(front (S Z) g2 g4)
+(front Z g0 g1)
+(front Z g1 g2)
+(front Z g2 g3)
+(front Z g3 g4)
diff --git a/differential/projection_cut_fuzz.py b/differential/projection_cut_fuzz.py
new file mode 100755
index 00000000..e7caecbe
--- /dev/null
+++ b/differential/projection_cut_fuzz.py
@@ -0,0 +1,382 @@
+#!/usr/bin/env python3
+"""Random-query validator for the projection cut.
+
+Generates random conjunctive bodies, works out INDEPENDENTLY -- from the rule as stated, over the
+generated syntax tree, never from the engine's mask -- which variables the cut may answer with a
+single witness, predicts how much enumeration that removes, then runs the query on a stock build
+and on a `projection_cut` build and checks three things:
+
+  * the two builds agree on the answer space byte for byte,
+  * the answers equal a join computed here in Python, from the generated facts, and
+  * where a speed-up was predicted, a speed-up actually happened.
+
+The rule, restated so this file is a second opinion rather than an echo: a body variable may be
+answered with one witness iff (a) the body mentions it exactly once, (b) no template reads it, and
+(c) everything after it inside its own conjunct also satisfies (a) and (b) -- it lies in the
+conjunct's trailing run. Anything earlier in a conjunct decides which subtrie the later columns
+are drawn from, so pinning it would drop answers rather than duplicates.
+
+Three families:
+
+  direct     relations of ground tuples, including the named shape
+             `(, (R $x $_1 $y $_2 $_3) (Q $x $y))` -- `$_2 $_3` are cuttable, `$_1` is not,
+             because `$y` follows it.
+  schematic  the same shapes, but every don't-care value is a fuzzed QUERY EXPRESSION carrying
+             variables of its own, so the cut binds schematic terms rather than symbols.
+  meta       the space holds fuzzed queries as data -- `(f (R $x $_1 $y $_2 $_3))`,
+             `(g (Q $x $y))`, `(data ...)` -- and the body queries over them in the
+             `(, (f $f ...) (g $g ...) (data $f) (data $g))` shape.
+
+Usage:  projection_cut_fuzz.py --base BIN --cut BIN [--cases N] [--seed S]
+"""
+
+import argparse, itertools, os, random, re, subprocess, sys, tempfile
+
+TOOK = re.compile(r"took (\d+) ms")
+
+
+# ---------------------------------------------------------------------------- queries
+
+class Factor:
+    def __init__(self, rel, cols):
+        self.rel, self.cols = rel, cols
+
+    def text(self):
+        return "(%s %s)" % (self.rel, " ".join("$" + c for c in self.cols))
+
+
+class Query:
+    def __init__(self, factors, reads, family):
+        self.factors, self.reads, self.family = factors, reads, family
+
+    def body(self):
+        return "(, %s)" % " ".join(f.text() for f in self.factors)
+
+    def exec_atom(self):
+        return "(exec 0 %s (, (out %s)))" % (self.body(), " ".join("$" + v for v in self.reads))
+
+    def occurrences(self):
+        occ = {}
+        for f in self.factors:
+            for c in f.cols:
+                occ[c] = occ.get(c, 0) + 1
+        return occ
+
+    def cuttable(self):
+        """The rule applied to the syntax tree -- independent of the engine's byte-level mask."""
+        occ = self.occurrences()
+        solo = lambda v: occ[v] == 1 and v not in self.reads
+        cut = set()
+        for f in self.factors:
+            for c in reversed(f.cols):      # the conjunct's trailing run, and no further
+                if not solo(c):
+                    break
+                cut.add(c)
+        return cut
+
+
+def named_shape():
+    """The shape called out by name: jump the last two columns of R, but never `$_1`."""
+    return Query([Factor("R", ["x0", "d0", "x1", "d1", "d2"]), Factor("Q", ["x0", "x1"])],
+                 ["x0", "x1"], "direct")
+
+
+def gen_query(rng, family):
+    if family == "meta":
+        # `(, (f $f ...) (g $g ...) (data $f) (data $g))` -- the join variables bind whole
+        # query expressions; the don't-care tails are what the cut may answer.
+        fac = [Factor("f", ["f"] + ["d%d" % i for i in range(rng.choice([1, 1, 2]))])]
+        nd = len(fac[0].cols) - 1
+        fac.append(Factor("g", ["g"] + ["d%d" % (nd + i) for i in range(rng.choice([0, 1, 2]))]))
+        fac.append(Factor("data", ["f"]))
+        fac.append(Factor("data", ["g"]))
+        return Query(fac, ["f", "g"], "meta")
+
+    nkeys = rng.choice([1, 1, 2])
+    keys = ["x%d" % i for i in range(nkeys)]
+    factors, dc = [], 0
+    for fi in range(rng.choice([1, 2, 2, 3])):
+        cols = list(keys) if fi == 0 else [rng.choice(keys)]
+        if rng.random() < 0.4 and nkeys > 1:        # a don't-care BEFORE a key: never cuttable
+            cols = [cols[0], "d%d" % dc] + cols[1:]
+            dc += 1
+        for _ in range(rng.choice([1, 1, 2, 2, 3])):
+            cols.append("d%d" % dc)
+            dc += 1
+        factors.append(Factor("R%d" % fi, cols))
+    return Query(factors, keys, family)
+
+
+# ---------------------------------------------------------------------------- data
+
+def query_expr(j):
+    """A fuzzed query expression, used as a stored VALUE. Carries its own variables.
+
+    Every index yields a DISTINCT expression -- the shape rotates but the relation names carry
+    `j`. Duplicates would silently collapse in the trie, making the relation smaller than the
+    generator believes and the predicted ratio a fiction.
+    """
+    shapes = [
+        "(, (R%d $x $a $y $b $c) (Q%d $x $y))" % (j, j),
+        "(, (f%d $p) (g%d $q) (data $p) (data $q))" % (j, j),
+        "(P%d (= $l $r) $t%d)" % (j, j),
+        "(, (S%d $u $v) (T%d $v $w $z))" % (j, j),
+    ]
+    return shapes[j % len(shapes)]
+
+
+def gen_data(rng, q, nkey, fan):
+    """Facts for every factor. Returns (facts, per-relation sizes, per-variable domains)."""
+    keyvals = ["k%d" % i for i in range(nkey)]
+    if q.family == "meta":
+        keyvals = [query_expr(i) for i in range(nkey)]
+    dcvals = [("w%d" % j) if q.family == "direct" else query_expr(j) for j in range(fan)]
+
+    assert len(set(keyvals)) == len(keyvals), "key values must be distinct"
+    assert len(set(dcvals)) == len(dcvals), "don't-care values must be distinct"
+    facts, sizes, domains = [], {}, {}
+    for f in q.factors:
+        rows = []
+        doms = [keyvals if not c.startswith("d") else dcvals for c in f.cols]
+        # A full cross product would make a don't-care that PRECEDES a key independent of that
+        # key: pinning it would still leave every suffix value reachable, so an engine that
+        # wrongly cut a non-trailing variable would produce the right answers anyway and the
+        # fuzzer would never notice. Correlate them instead -- each value of a leading
+        # don't-care admits only a SLICE of the keys that follow it, so pinning it drops
+        # answers and the check fails.
+        lead_dc = [k for k, c in enumerate(f.cols)
+                   if c.startswith("d") and any(not c2.startswith("d") for c2 in f.cols[k + 1:])]
+        for combo in itertools.product(*doms):
+            if lead_dc:
+                drop = False
+                for k in lead_dc:
+                    slot = dcvals.index(combo[k])
+                    for k2 in range(k + 1, len(f.cols)):
+                        if not f.cols[k2].startswith("d"):
+                            # keep only the keys congruent to this don't-care's slot
+                            if keyvals.index(combo[k2]) % len(dcvals) != slot % len(dcvals):
+                                drop = True
+                if drop:
+                    continue
+            rows.append("(%s %s)" % (f.rel, " ".join(combo)))
+        facts.extend(rows)
+        key = f.rel + "/" + str(len(f.cols))
+        sizes[key] = (sizes.get(key, (0, 0, 0))[0] + len(rows),
+                      sum(1 for c in f.cols if not c.startswith("d")),
+                      sum(1 for c in f.cols if c.startswith("d")))
+        for c in f.cols:
+            domains[c] = keyvals if not c.startswith("d") else dcvals
+    return facts, sizes, domains, keyvals, dcvals
+
+
+def predicted_ratio(q, fan):
+    """Enumerated tuples over cut tuples: every don't-care contributes its fan-out unless cut."""
+    cut = q.cuttable()
+    base = after = 1
+    for f in q.factors:
+        for c in f.cols:
+            if c.startswith("d"):
+                base *= fan
+                after *= 1 if c in cut else fan
+    return base, after
+
+
+def python_join(q, domains):
+    """The answer set, computed here: project each factor onto the variables that outlive it
+    (read, or shared with another factor), dedup, then join. Sound because every projected-away
+    variable is a singleton, hence purely existential."""
+    occ = q.occurrences()
+    keep = lambda v: v in q.reads or occ[v] > 1
+    rel = None
+    for f in q.factors:
+        cols = [c for c in f.cols if keep(c)]
+        doms = [domains[c] for c in cols]
+        tuples = {tuple(t) for t in itertools.product(*doms)} if cols else {()}
+        if rel is None:
+            rel, relcols = tuples, cols
+            continue
+        shared = [c for c in cols if c in relcols]
+        li = [relcols.index(c) for c in shared]
+        ri = [cols.index(c) for c in shared]
+        newcols = relcols + [c for c in cols if c not in relcols]
+        add = [cols.index(c) for c in cols if c not in relcols]
+        out = set()
+        for a in rel:
+            for b in tuples:
+                if all(a[x] == b[y] for x, y in zip(li, ri)):
+                    out.add(a + tuple(b[i] for i in add))
+        rel, relcols = out, newcols
+    idx = [relcols.index(v) for v in q.reads]
+    return {tuple(t[i] for i in idx) for t in rel}
+
+
+# ---------------------------------------------------------------------------- running
+
+def run(binary, prog, out, reps, timeout):
+    """Best-of-`reps` query time and the resulting space, or (None, None) if it does not finish.
+
+    A timeout is data, not an error: the two engines differ by orders of magnitude on some of
+    these shapes, so the sizing ladder needs to be told when it has gone too far rather than
+    having the run die.
+    """
+    best, dump = None, None
+    for _ in range(reps):
+        # Clear the target first and insist the process succeeded: otherwise a crashed or
+        # timed-out run leaves the PREVIOUS run's space behind and the comparison silently
+        # passes on stale output.
+        if os.path.exists(out):
+            os.remove(out)
+        try:
+            r = subprocess.run([binary, "run", prog, "--steps", "2", out],
+                               capture_output=True, timeout=timeout)
+        except subprocess.TimeoutExpired:
+            return None, None
+        if r.returncode != 0 or not os.path.exists(out):
+            return None, None
+        m = TOOK.search(r.stdout.decode("utf-8", "replace"))
+        ms = int(m.group(1)) if m else -1
+        best = ms if best is None else min(best, ms)
+        with open(out, "rb") as fh:
+            dump = fh.read()
+    return best, dump
+
+
+def parse_answers(dump):
+    out = set()
+    for line in dump.decode("utf-8", "replace").split("\n"):
+        if line.startswith("(out "):
+            out.add(line[5:-1].strip())
+    return out
+
+
+def main():
+    ap = argparse.ArgumentParser()
+    ap.add_argument("--base", required=True)
+    ap.add_argument("--cut", required=True)
+    ap.add_argument("--cases", type=int, default=26)
+    ap.add_argument("--seed", type=int, default=1)
+    ap.add_argument("--reps", type=int, default=2)
+    ap.add_argument("--min-base-ms", type=int, default=20)
+    ap.add_argument("--max-facts", type=int, default=250000)
+    ap.add_argument("--keep", default=None)
+    ap.add_argument("--family", default=None, help="force one family")
+    ap.add_argument("--base-timeout", type=int, default=300, help="seconds before a size is too big")
+    ap.add_argument("--label", default="", help="engine label for the report header")
+    args = ap.parse_args()
+
+    rng = random.Random(args.seed)
+    tmp = args.keep or tempfile.mkdtemp(prefix="pcfuzz-")
+    os.makedirs(tmp, exist_ok=True)
+    families = ["direct", "schematic", "meta"]
+    accepted, attempts = [], 0
+
+    while len(accepted) < args.cases and attempts < args.cases * 60:
+        attempts += 1
+        if args.family:
+            q = gen_query(rng, args.family)
+        else:
+            q = named_shape() if not accepted else gen_query(rng, families[attempts % 3])
+        cut = q.cuttable()
+        if not cut:
+            continue                                   # report only where a jump is predicted
+
+        # Grow the data until the ENUMERATION is long enough to time honestly, measuring it at
+        # each step rather than predicting its cost: the two engines differ by orders of
+        # magnitude on the schematic and meta shapes, so a tuple-count model that sizes the
+        # leapfrog join sensibly can hand the ProductZipper a query it will not finish.
+        prog = os.path.join(tmp, "case%02d.mm2" % len(accepted))
+        chosen = None
+        for nkey, fan in [(4, 6), (6, 8), (8, 10), (10, 12), (12, 14), (14, 16), (16, 20), (20, 24)]:
+            facts, sizes, domains, keyvals, dcvals = gen_data(rng, q, nkey, fan)
+            if len(facts) > args.max_facts:
+                break
+            base_t, after_t = predicted_ratio(q, fan)
+            if base_t <= after_t:
+                break
+            with open(prog, "w") as fh:
+                fh.write("\n".join(facts) + "\n" + q.exec_atom() + "\n")
+            b_ms, b_dump = run(args.base, prog, prog + ".base.space", 1, args.base_timeout)
+            if b_ms is None:
+                break                                  # too big for this engine: keep the last
+            chosen = (facts, sizes, domains, nkey, fan, base_t, after_t, b_ms, b_dump)
+            if b_ms >= args.min_base_ms:
+                break
+        if chosen is None:
+            continue
+        facts, sizes, domains, nkey, fan, base_t, after_t, b_ms, b_dump = chosen
+        if b_ms < args.min_base_ms:
+            continue                                   # too fast to attribute a ratio to
+        # rewrite the chosen size, since the ladder may have moved past it
+        with open(prog, "w") as fh:
+            fh.write("\n".join(facts) + "\n" + q.exec_atom() + "\n")
+        if b_ms < 2000:
+            b_ms, b_dump = run(args.base, prog, prog + ".base.space", args.reps, args.base_timeout)
+        c_ms, c_dump = run(args.cut, prog, prog + ".cut.space", args.reps, args.base_timeout)
+        if c_ms is None:
+            print("  case %d: the cut build did not finish or exited nonzero" % len(accepted))
+            c_ms, c_dump = args.base_timeout * 1000, None
+
+        identical = (c_dump is not None and b_dump == c_dump)
+        # The independent join models an EQUALITY join, which is what the engine performs only
+        # when the joined values are ground. In the meta family the read variables bind whole
+        # query expressions, so the engine joins them by UNIFICATION and renames their variables
+        # on output; modelling that here would mean reimplementing the unifier. Those cases are
+        # held to stock-vs-cut byte-identity instead -- the stock engine IS the reference -- plus
+        # a non-empty answer space, so a silently empty result cannot pass.
+        modelled = any(not v.startswith("(") for v in [domains[r][0] for r in q.reads])
+        if modelled:
+            want = {" ".join(t) for t in python_join(q, domains)}
+            answers_ok = (parse_answers(b_dump) == want and parse_answers(c_dump) == want)
+            nans = len(want)
+        else:
+            nans = len(parse_answers(b_dump))
+            answers_ok = nans > 0
+        speedup = b_ms / max(c_ms, 0.5)
+        accepted.append(dict(q=q, sizes=sizes, nkey=nkey, fan=fan, facts=len(facts),
+                             pred=base_t / after_t, b_ms=b_ms, c_ms=c_ms, speedup=speedup,
+                             identical=identical, answers_ok=answers_ok, modelled=modelled,
+                             cut=sorted(cut), nans=nans))
+
+    ok = lambda c: c["identical"] and c["answers_ok"] and c["speedup"] >= 1.5
+    print("%sseed=%d  cases=%d  attempts=%d  programs in %s\n" % (("engine=%s  " % args.label) if args.label else "", args.seed, len(accepted), attempts, tmp))
+    hdr = "%-3s %-9s %-44s %8s %10s %8s %7s %9s %s" % (
+        "#", "family", "body", "facts", "predicted", "base ms", "cut ms", "speedup", "ok")
+    print(hdr); print("-" * len(hdr))
+    for i, c in enumerate(accepted):
+        b = c["q"].body()
+        b = b if len(b) <= 44 else b[:41] + "..."
+        print("%-3d %-9s %-44s %8d %9.0fx %8d %7d %8.1fx %s" %
+              (i, c["q"].family, b, c["facts"], c["pred"], c["b_ms"], c["c_ms"], c["speedup"],
+               "yes" if ok(c) else "NO"))
+    print("\nrelation sizes and the variables the cut answered with one witness:")
+    for i, c in enumerate(accepted):
+        rels = ", ".join("%s:%d facts(%d key,%d dc)" % (r.split("/")[0], v[0], v[1], v[2])
+                         for r, v in sorted(c["sizes"].items()))
+        print("  %-3d keyvals=%-3d fanout=%-3d answers=%-5d cut=%-16s %s" %
+              (i, c["nkey"], c["fan"], c["nans"], ",".join("$" + v for v in c["cut"]), rels))
+    short = len(accepted) < args.cases
+    if short:
+        print("\nSHORT RUN: asked for %d cases, accepted %d. A run that cannot build its cases "
+              "proves nothing, so this is a failure, not a pass." % (args.cases, len(accepted)))
+    bad = [c for c in accepted if not ok(c)]
+    print("\n%d/%d met the prediction | byte-identical: %d/%d | answer set correct: %d/%d" %
+          (len(accepted) - len(bad), len(accepted),
+           sum(1 for c in accepted if c["identical"]), len(accepted),
+           sum(1 for c in accepted if c["answers_ok"]), len(accepted)))
+    nm = [c for c in accepted if not c["modelled"]]
+    if nm:
+        print("(%d meta cases are checked by stock-vs-cut byte-identity and a non-empty answer "
+              "space, not by the equality-join model -- see the note in the source)" % len(nm))
+    if accepted:
+        sp = sorted(c["speedup"] for c in accepted)
+        print("speed-up: min %.1fx  median %.1fx  max %.1fx" % (sp[0], sp[len(sp) // 2], sp[-1]))
+    if bad:
+        print("\nFAILED:")
+        for c in bad:
+            print("  %s\n    identical=%s answers_ok=%s speedup=%.2fx predicted=%.0fx" %
+                  (c["q"].body(), c["identical"], c["answers_ok"], c["speedup"], c["pred"]))
+    return 1 if (bad or short) else 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())
diff --git a/examples/transforms/README.md b/examples/transforms/README.md
new file mode 100644
index 00000000..7e303bf6
--- /dev/null
+++ b/examples/transforms/README.md
@@ -0,0 +1,175 @@
+# Semi-join and incrementalization, as source-level MM2 transforms
+
+Both are rewrites of a program into more programs. Neither needs a change to the join. What the
+projection cut adds is that the *projections* a semi-join reduction is built out of stop costing
+a full pass over the relation.
+
+`generate.py OUTDIR` writes the six measured programs; every measurement below is the query-only
+time the CLI reports (`took N ms`), best of three, on the same machine.
+
+## 1. The projection is the shape the cut answers
+
+A semi-join `A ⋉ B` on variable `v` needs `π_v(B)` — in MM2, `(exec _ (, (B $v $_)) (, (Bv $v)))`.
+`$_` is mentioned once, no template reads it, and it is the conjunct's last column, so the cut
+answers it with one witness per key instead of enumerating every tuple.
+
+| program | leapfrog | ProductZipper |
+|---|---|---|
+| `proj_keyfirst.mm2` — `(, (S $y $_))` | **0 ms** | **0 ms** |
+| `proj_keylast.mm2` — `(, (S $_ $z))` | 22 ms | 26 ms |
+
+80000 tuples over 600 distinct keys. **This is the design rule the transform must follow: emit
+reduced relations KEY-FIRST.** With the key last the don't-care is not trailing, the cut correctly
+refuses it (pinning `$_` would decide which subtrie `$z` comes from), and the projection pays a
+full pass.
+
+## 2. Yannakakis staging
+
+`chain_naive.mm2` joins `(, (R $x $y) (S $y $z) (T $z $w))` directly. `chain_staged.mm2` projects,
+semi-joins bottom-up, semi-joins top-down, then joins the reduced relations — nine execs ordered
+by `loc`.
+
+| | leapfrog | ProductZipper |
+|---|---|---|
+| naive chain join | 166 ms | 811 ms |
+| Yannakakis staged | 154 ms | **276 ms** |
+
+**2.9× on the ProductZipper, ~1.07× on leapfrog.** On an *acyclic* body leapfrog intersects every
+participating factor at each variable, so it is already doing the reduction's work and little is
+left to remove. That is a property of acyclic bodies only -- see §5, where the same decomposition
+is worth 25x to leapfrog on a cyclic one.
+
+## 3. Incrementalization
+
+`tc_naive.mm2` re-joins the whole `path` relation with `edge` on every iteration.
+`tc_delta.mm2` joins only the frontier the previous iteration produced — the wiki's own
+generation-labelled idiom, which is semi-naive evaluation written by hand.
+
+| chain of 220 nodes, closure = 24090 pairs | leapfrog | ProductZipper |
+|---|---|---|
+| naive fixpoint | 19565 ms | 24381 ms |
+| semi-naive | **150 ms** | **208 ms** |
+| | **130×** | **117×** |
+
+Identical closures on both engines. This one needs no engine support at all: per-iteration work
+falls from `O(|path|)` to `O(|Δ|)`, and the two are quadratically apart on a chain.
+
+## 4. Composing them
+
+The two compose and stay correct, but an *inline* semi-join conjunct buys nothing:
+
+| 120 chain nodes × 12 dead-end leaves each | leapfrog | ProductZipper |
+|---|---|---|
+| semi-naive | 348 ms | 504 ms |
+| semi-naive + inline `(esrc $y)` guard | 350 ms | 519 ms |
+
+Both engines already intersect at the shared variable, so the extra conjunct re-derives a
+restriction they were performing anyway and costs a third factor to intersect. A reduction only
+pays when it is **materialised into an earlier stage**, removing tuples before a later and more
+expensive one — which is what §2 does and what §4 does not.
+
+## Two MM2 gotchas these programs ran into
+
+**Loc ordering.** Execs run in byte order of the whole atom, and a *symbol* loc sorts above a
+*compound* one: `(exec (2 0) ..)` runs AFTER `(exec (2 (1 Z)) ..)`. Mixing the two shapes inverts
+the intended staging — a seed written `(exec (2 0) ..)` fires after the loop that consumes it, so
+the loop sees an empty relation and dies silently.
+
+**Self-reproducing execs never stop.** A rule that re-adds itself has no termination condition of
+its own, so it monopolises every remaining step and any family ordered after it never runs. Bound
+it with Peano fuel consumed through an `O`-form `(+ (fuel $k)) (- (fuel (S $k)))`, as the
+Reachability-P2 tutorial does.
+
+`differential/corpus/programs/transform_staging.mm2` carries both transforms at a size the
+differential runs on every build, computing each one BOTH ways in a single program so its expected
+space pins the staged form equal to the form it replaces.
+
+## 5. Decomposition on a CYCLIC body — where leapfrog does gain
+
+`cyc_naive.mm2` asks for 6-cycles directly. `cyc_staged.mm2` splits the cycle into two bags of
+three edges — a generalized hypertree decomposition of width 2, against the query's fractional
+edge cover number of 3 — materialising the first bag as its projected endpoints.
+
+| 900 edges, 70 nodes | leapfrog | ProductZipper |
+|---|---|---|
+| naive 6-cycle join | 5951 ms | 11419 ms |
+| two bags, endpoints materialised | **237 ms** | **425 ms** |
+| | **25×** | **27×** |
+
+Identical answers. The mechanism is visible in the data: the graph holds 149611 three-paths but
+only 4900 distinct endpoint pairs, a 30.5x sharing factor, of which the staging realises 25x. A
+worst-case-optimal join re-derives the entire suffix for **every** binding of the variables the
+decomposition projects away; materialising the bag pays for the suffix once per distinct endpoint
+pair. So the earlier claim that leapfrog is already doing Yannakakis' work holds for acyclic
+bodies and does not generalise: on cyclic ones the decomposition is a large win for leapfrog too.
+
+## 6. Incrementalizing the process calculus
+
+The benchmark's communication rule is a self-join on the soup keyed by channel:
+`(, (petri (? $c $pl $b)) (petri (! $c $pl))) -> (petri $b)`. It is MONOTONE -- nothing is
+removed -- so every past communication is re-derived on every activation, and the cost of a
+cascade of length N is quadratic in N.
+
+`pc3_delta.mm2` joins only the messages the previous round produced, with promotion folded into
+the rule itself (a separate promotion exec would be starved: this family re-adds itself and sorts
+first, so it consumes all the fuel before the promoter ever runs).
+
+`pc3_consume.mm2` instead retires the reagents -- `(- (petri (? ...))) (- (petri (! ...)))` --
+which is the faithful reading of a communication and removes the re-derivation at its source
+rather than filtering it afterwards.
+
+| chain length | naive | delta | | consuming | |
+|---|---|---|---|---|---|
+| 200 | 250 ms | 37 ms | 6.8× | 27 ms | 9.3× |
+| 400 | 1391 ms | 129 ms | 10.8× | 87 ms | 16.0× |
+| 800 | 9452 ms | 479 ms | 19.7× | 313 ms | 30.2× |
+
+All three derive the final message. The ratio roughly doubles as the chain doubles, which is the
+signature of removing a quadratic: the uplift is not a constant and has no ceiling.
+
+Consuming beats the delta at every size and leaves a soup of ONE atom against 801, because the
+delta still keeps every intermediate and merely avoids re-joining it, while consuming never keeps
+one. Where the intermediates are not wanted, that is the transform to reach for.
+
+An earlier version of this section reported ~1.1x. That measurement ran 30 rounds of fuel over a
+4000-receiver chain -- under one percent of the cascade -- so the quadratic never developed and
+the number was an artifact of the harness, not a property of the transform. The shipped
+`process_calculus_bench` rule is monotone in exactly this way, so it is paying the same quadratic.
+
+## 7. Sweep over main.rs and the wiki
+
+Every MM2 program in `kernel/src/main.rs`, `kernel/resources/` and the wiki was inventoried for
+the two transforms. Applicability turns on three properties of a rule body: whether it is
+ITERATIVE (a self-reproducing exec, so incrementalization applies), whether it is CYCLIC and
+PROJECTS variables away (so a decomposition can share the suffix), and whether the relation being
+ENUMERATED is the one that grows.
+
+`bench_pairs.py DIR STEPS PREFIXES` measures every `X_naive.mm2` against its `X_<variant>.mm2`
+in DIR on both engines and checks the answer spaces agree.
+
+| example | taken from | transform | leapfrog | ProductZipper |
+|---|---|---|---|---|
+| `tc` | Reachability P1/P3 shape | incrementalization | **130×** | **117×** |
+| `cyc` | cyclic body, ghw 2 < ρ* 3 | GHD decomposition | **25.4×** | **27.1×** |
+| `craft` | wiki Reachability-P2 `exec (1 3)` | semi-join reduction | **8.5×** | **15.6×** |
+| `chain` | acyclic 3-relation join | Yannakakis staging | 1.07× | **2.9×** |
+| `lts` | taxi_lts / tile_puzzle / CTL shape | worklist delta | 1.8× | 1.8× |
+| `clq` | `bench_clique_no_unify` | triangle staging | 0.9× | **6.9×** |
+| `pc2` | `process_calculus_bench` | delta | 1.1× | — |
+
+What separates the top of that table from the bottom is projection, not cyclicity. `cyc` and
+`craft` both discard almost every body variable, so materialising a bag pays for the shared
+suffix once instead of once per discarded binding. `clq` is just as cyclic but names every
+variable in its template, so leapfrog has nothing to share and only the ProductZipper -- which
+has no per-level intersection at all -- gains. `lts` and `pc2` grow the relation the join
+PROBES rather than the one it ENUMERATES, so a delta barely helps; `tc` grows the enumerated one
+quadratically, which is the whole 130×.
+
+Programs that the sweep found and did NOT translate, with the reason: `bench_logic_query`,
+`bench_finite_domain`, `pattern_mining`, `bench_lr`, `grounding`, `string_convert` and the
+`Sources-and-Sinks` examples are single-shot and non-iterative with nothing projected away;
+`decision_tree_learning`, `hexlife` and `ip_sudoku` are driven by aggregating sinks, which the
+projection cut may not touch at all (see the sink note in space.rs); `bfc`, `ctl` and the
+backward-chaining family are iterative but their rules are generated per-step by meta-execs, so
+a delta rewrite has to be applied to the generator rather than the rule and is a larger change
+than this file demonstrates.
diff --git a/examples/transforms/bench_pairs.py b/examples/transforms/bench_pairs.py
new file mode 100755
index 00000000..74f7088c
--- /dev/null
+++ b/examples/transforms/bench_pairs.py
@@ -0,0 +1,60 @@
+#!/usr/bin/env python3
+"""Benchmark paired MM2 programs: for each X, run X_naive.mm2 against X_<variant>.mm2 on both
+engines, check the answer spaces agree, and report the ratio. Query-only time, best of 3."""
+import glob, os, re, subprocess, sys
+TOOK = re.compile(r"took (\d+) ms")
+def run(binary, prog, out, steps, reps=3):
+    """Best-of-`reps` query time and the resulting space, or (None, None) if the run failed.
+
+    The target is cleared before every attempt and the exit status is checked: without both, a
+    crashed or timed-out run leaves the PREVIOUS run's space in place and the caller compares
+    stale output, which reads as agreement.
+    """
+    best = None
+    for _ in range(reps):
+        if os.path.exists(out):
+            os.remove(out)
+        try:
+            r = subprocess.run([binary, "run", prog, "--steps", str(steps), out],
+                               capture_output=True, timeout=600)
+        except subprocess.TimeoutExpired:
+            return None, None
+        if r.returncode != 0 or not os.path.exists(out):
+            return None, None
+        m = TOOK.search(r.stdout.decode("utf-8", "replace"))
+        ms = int(m.group(1)) if m else -1
+        best = ms if best is None else min(best, ms)
+    return best, open(out, "rb").read()
+def key_lines(dump, prefixes):
+    return sorted(l for l in dump.decode("utf-8", "replace").split("\n")
+                  if any(l.startswith("(" + p) for p in prefixes))
+def main(d, steps, prefixes):
+    names = sorted({os.path.basename(f).rsplit("_", 1)[0] for f in glob.glob(d + "/*_naive.mm2")})
+    print("%-22s %-10s %9s %9s %8s   %9s %9s %8s  %s" %
+          ("example", "variant", "lf naive", "lf opt", "x", "pz naive", "pz opt", "x", "agree"))
+    for n in names:
+        base = f"{d}/{n}_naive.mm2"
+        for v in sorted(glob.glob(f"{d}/{n}_*.mm2")):
+            tag = os.path.basename(v)[len(n) + 1:-4]
+            if tag == "naive":
+                continue
+            row, agree = [], []
+            for e in ["lf", "pz"]:
+                # ABBA: time each program twice, on either side of the other, and keep the best
+                # of each. Always running the baseline first biases a long benchmark against
+                # whichever runs second, because drift over the pair is monotonic.
+                bn1, bd = run(f"/tmp/paj-v4-{e}", base, f"/tmp/bp_{n}_{e}_n.space", steps)
+                on1, od = run(f"/tmp/paj-v4-{e}", v, f"/tmp/bp_{n}_{e}_o.space", steps)
+                on2, _ = run(f"/tmp/paj-v4-{e}", v, f"/tmp/bp_{n}_{e}_o.space", steps)
+                bn2, _ = run(f"/tmp/paj-v4-{e}", base, f"/tmp/bp_{n}_{e}_n.space", steps)
+                # `if (bn1 or bn2)` would read a genuine 0 ms as failure; only None is failure.
+                best = lambda *xs: min([x for x in xs if x is not None], default=None)
+                bn, on = best(bn1, bn2), best(on1, on2)
+                if bn is None or on is None:
+                    row += ["t/o", "t/o", 0.0]; agree.append("?"); continue
+                row += [bn, on, bn / max(on, 0.5)]
+                agree.append("y" if key_lines(bd, prefixes) == key_lines(od, prefixes) else "N")
+            print("%-22s %-10s %9s %9s %7.1fx   %9s %9s %7.1fx  %s" %
+                  (n, tag, row[0], row[1], row[2], row[3], row[4], row[5], "".join(agree)))
+if __name__ == "__main__":
+    main(sys.argv[1], int(sys.argv[2]), sys.argv[3].split(","))
diff --git a/examples/transforms/generate.py b/examples/transforms/generate.py
new file mode 100755
index 00000000..d7a19b9b
--- /dev/null
+++ b/examples/transforms/generate.py
@@ -0,0 +1,110 @@
+#!/usr/bin/env python3
+"""Generate the measured programs for the two source-level transforms.
+
+  chain_{naive,staged}.mm2   a chain query R-S-T, joined directly vs Yannakakis-staged
+  proj_{keyfirst,keylast}.mm2  the same projection under both column orders
+  tc_{naive,delta}.mm2       transitive closure, re-joined in full vs semi-naive
+
+Run:  generate.py OUTDIR   then  mork run OUTDIR/<prog>.mm2 --steps 300 /tmp/out.space
+"""
+import os, random, sys
+
+RULES = {'cyc_naive': '(exec 9 (, (e $a $b) (e $b $c) (e $c $d) (e $d $f) (e $f $g) (e $g $a)) (, (cyc6 $a)))', 'cyc_staged': '(exec (1 0) (, (e $a $b) (e $b $c) (e $c $d)) (, (p3 $a $d)))\n(exec (1 1) (, (p3 $a $d) (e $d $f) (e $f $g) (e $g $a)) (, (cyc6 $a)))', 'clq_naive': '(exec 9 (, (edge $x0 $x1) (edge $x0 $x2) (edge $x0 $x3) (edge $x1 $x2) (edge $x1 $x3) (edge $x2 $x3))\n        (, (c4 $x0 $x1 $x2 $x3)))', 'clq_staged': '(exec (1 0) (, (edge $x0 $x1) (edge $x0 $x2) (edge $x1 $x2)) (, (tri $x0 $x1 $x2)))\n(exec (1 1) (, (tri $x0 $x1 $x2) (edge $x0 $x3) (edge $x1 $x3) (edge $x2 $x3))\n            (, (c4 $x0 $x1 $x2 $x3)))', 'craft_naive': '(exec 9 (, (recipe $p (numIngredients 2)) (recipe $p (result (id $n)))\n           (recipe $p (pattern 0 $x)) (recipe $p (key ($x $xi)))\n           (recipe $p (pattern 1 $y)) (recipe $p (key ($y $yi)))\n           (inventory $xi) (inventory $yi))\n        (, (craftable $n)))', 'craft_staged': '(exec (1 0) (, (recipe $p (pattern 0 $x)) (recipe $p (key ($x $xi))) (inventory $xi)) (, (ok0 $p)))\n(exec (1 1) (, (recipe $p (pattern 1 $y)) (recipe $p (key ($y $yi))) (inventory $yi)) (, (ok1 $p)))\n(exec (1 2) (, (recipe $p (numIngredients 2)) (ok0 $p) (ok1 $p) (recipe $p (result (id $n))))\n            (, (craftable $n)))', 'lts_naive': '(exec (1 Z) (, (exec (1 $l) $p $t) (fuelN (S $k)) (state $s) (trans $s $u))\n            (O (+ (exec (1 (S $l)) $p $t)) (+ (state $u)) (+ (fuelN $k)) (- (fuelN (S $k)))))', 'lts_delta': ';; One exec: take the worklist, publish successors into both the state set and the worklist,\n;; retire what was taken. A separate promotion exec would be starved -- this family re-adds\n;; itself and sorts first, so it consumes all the fuel before the promoter ever runs.\n(exec (1 Z) (, (exec (1 $l) $p $t) (fuelD (S $k)) (dstate $s) (trans $s $u))\n            (O (+ (exec (1 (S $l)) $p $t)) (+ (state $u)) (+ (dstate $u))\n               (- (dstate $s)) (+ (fuelD $k)) (- (fuelD (S $k)))))', 'pc3_naive': '(exec (1 Z) (, (exec (1 $l) $p $t) (fuel (S $k))\n               (petri (? $c $pl $b)) (petri (! $c $pl)))\n            (O (+ (exec (1 (S $l)) $p $t)) (+ (petri $b)) (+ (fuel $k)) (- (fuel (S $k)))))', 'pc3_delta': ';; Symmetric arms. A self-join over one relation needs BOTH deltas: new receivers against\n;; every message, and every receiver against new messages. With only the second, a\n;; communication that derives a RECEIVER never reacts with a message already in the soup.\n((arm 0) (, (dnew (? $c $pl $b)) (petri (! $c $pl)))\n         (O (+ (petri $b)) (+ (dnew $b)) (- (dnew (? $c $pl $b)))))\n((arm 1) (, (petri (? $c $pl $b)) (dnew (! $c $pl)))\n         (O (+ (petri $b)) (+ (dnew $b)) (- (dnew (! $c $pl)))))\n;; round-robin over the arms, the way process_calculus_bench drives its own two rules\n(exec (IC 0 1 FUEL) (, (exec (IC $x $y (S $c)) $sp $st) ((arm $x) $p $t))\n                    (, (exec (IC $y $x $c) $sp $st) (exec (R $x) $p $t)))', 'pc3_consume': '(exec (1 Z) (, (exec (1 $l) $p $t) (fuel (S $k))\n               (petri (? $c $pl $b)) (petri (! $c $pl)))\n            (O (+ (exec (1 (S $l)) $p $t)) (+ (petri $b))\n               (- (petri (? $c $pl $b))) (- (petri (! $c $pl)))\n               (+ (fuel $k)) (- (fuel (S $k)))))'}
+
+def main(outdir):
+    os.makedirs(outdir, exist_ok=True)
+    w = lambda n, s: open(os.path.join(outdir, n), "w").write(s)
+    random.seed(9)
+
+    # ---- chain query: T is narrow, so most S and R tuples dangle
+    ny = nz = 600
+    R = [(f"x{i}", f"y{random.randrange(ny)}") for i in range(60000)]
+    S = [(f"y{random.randrange(ny)}", f"z{random.randrange(nz)}") for i in range(60000)]
+    T = [(f"z{i}", f"w{j}") for i in range(8) for j in range(3)]
+    data = ([f"(R {a} {b})" for a, b in R] + [f"(S {a} {b})" for a, b in S]
+            + [f"(T {a} {b})" for a, b in T])
+    w("chain_naive.mm2", "\n".join(data) + "\n"
+      "(exec 9 (, (R $x $y) (S $y $z) (T $z $w)) (, (out $x $w)))\n")
+    w("chain_staged.mm2", "\n".join(data) + """
+;; Yannakakis: project, semi-join bottom-up, semi-join top-down, join the reduced relations.
+;; Every projection is `(, (Rel $key $_))` -- the shape the projection cut answers with one
+;; witness per key -- which is why the reduced relations are emitted KEY-FIRST.
+(exec (1 0) (, (T $z $_))            (, (Tz $z)))
+(exec (1 1) (, (S $y $z) (Tz $z))    (, (S1 $y $z)))
+(exec (1 2) (, (S1 $y $_))           (, (S1y $y)))
+(exec (1 3) (, (R $x $y) (S1y $y))   (, (R1 $y $x)))
+(exec (1 4) (, (R1 $y $_))           (, (R1y $y)))
+(exec (1 5) (, (S1 $y $z) (R1y $y))  (, (S2 $z $y)))
+(exec (1 6) (, (S2 $z $_))           (, (S2z $z)))
+(exec (1 7) (, (T $z $w) (S2z $z))   (, (T1 $z $w)))
+(exec (2 0) (, (R1 $y $x) (S2 $z $y) (T1 $z $w)) (, (out $x $w)))
+""")
+
+    # ---- the projection alone, under both column orders
+    P = [(f"y{random.randrange(600)}", f"z{random.randrange(600)}") for _ in range(80000)]
+    pd = "\n".join(f"(S {a} {b})" for a, b in P)
+    w("proj_keyfirst.mm2", pd + "\n(exec 0 (, (S $y $_)) (, (Sy $y)))\n")
+    w("proj_keylast.mm2", pd + "\n(exec 0 (, (S $_ $z)) (, (Sz $z)))\n")
+
+    # ---- transitive closure over a chain: |path| is quadratic, each frontier is linear
+    n = 220
+    edges = "\n".join(f"(edge n{i} n{i+1})" for i in range(n - 1))
+    w("tc_naive.mm2", edges + """
+(exec (0 0) (, (edge $x $y)) (, (path $x $y)))
+(exec (1 Z) (, (exec (1 $l) $p $t) (path $x $y) (edge $y $z))
+            (, (exec (1 (S $l)) $p $t) (path $x $z)))
+""")
+    w("tc_delta.mm2", edges + """
+(exec (0 0) (, (edge $x $y)) (, (front Z $x $y) (path $x $y)))
+(exec (1 Z) (, (exec (1 $l) $p $t) (front $l $x $y) (edge $y $z))
+            (, (exec (1 (S $l)) $p $t) (front (S $l) $x $z) (path $x $z)))
+""")
+
+    E = set()
+    while len(E) < 900:
+        a, b = random.randrange(70), random.randrange(70)
+        if a != b: E.add((a, b))
+    edges = "\n".join("(e n%d n%d)" % (a, b) for a, b in sorted(E)) + "\n"
+    w("cyc_naive.mm2", edges + RULES["cyc_naive"] + "\n")
+    w("cyc_staged.mm2", edges + RULES["cyc_staged"] + "\n")
+
+    C = set()
+    while len(C) < 3600:
+        a, b = random.randrange(200), random.randrange(200)
+        if a < b: C.add((a, b))
+    cedges = "\n".join("(edge n%d n%d)" % (a, b) for a, b in sorted(C)) + "\n"
+    w("clq_naive.mm2", cedges + RULES["clq_naive"] + "\n")
+    w("clq_staged.mm2", cedges + RULES["clq_staged"] + "\n")
+
+    L = []
+    for pi in range(400):
+        L += ["(recipe r%d (numIngredients 2))" % pi, "(recipe r%d (result (id item%d)))" % (pi, pi),
+              "(recipe r%d (pattern 0 sx%d))" % (pi, pi), "(recipe r%d (pattern 1 sy%d))" % (pi, pi)]
+        for k in range(12):
+            L.append("(recipe r%d (key (sx%d ing%d)))" % (pi, pi, (pi * 3 + k) % 600))
+            L.append("(recipe r%d (key (sy%d ing%d)))" % (pi, pi, (pi * 5 + k) % 600))
+    L += ["(inventory ing%d)" % i for i in range(600)]
+    craft = "\n".join(L) + "\n"
+    w("craft_naive.mm2", craft + RULES["craft_naive"] + "\n")
+    w("craft_staged.mm2", craft + RULES["craft_staged"] + "\n")
+
+    tr = "\n".join("(trans s%d s%d)" % (i, (i * 7 + j * 13 + 1) % 6000)
+                    for i in range(6000) for j in range(3)) + "\n(state s0)\n"
+    w("lts_naive.mm2", tr + RULES["lts_naive"] + "\n")
+    w("lts_delta.mm2", tr + "(dstate s0)\n" + RULES["lts_delta"] + "\n")
+
+    for n in (200, 400, 800):
+        soup = "\n".join("(petri (? c%d p%d (! c%d p%d)))" % (i, i, i + 1, i + 1) for i in range(n))
+        fuel = "Z"
+        for _ in range(n + 5): fuel = "(S %s)" % fuel
+        head = soup + "\n(petri (! c0 p0))\n(fuel %s)\n" % fuel
+        w("pc%d_naive.mm2" % n, head + RULES["pc3_naive"] + "\n")
+        # everything is new at the start, so the worklist is seeded with the whole soup
+        dnew = soup.replace("(petri ", "(dnew ") + "\n(dnew (! c0 p0))\n"
+        w("pc%d_delta.mm2" % n, soup + "\n(petri (! c0 p0))\n" + dnew
+                                + RULES["pc3_delta"].replace("FUEL", fuel) + "\n")
+        w("pc%d_consume.mm2" % n, head + RULES["pc3_consume"] + "\n")
+    print("wrote all programs to " + outdir)
+
+if __name__ == "__main__":
+    main(sys.argv[1] if len(sys.argv) > 1 else ".")
diff --git a/kernel/src/leapfrog.rs b/kernel/src/leapfrog.rs
index fa4ab804..0b845694 100644
--- a/kernel/src/leapfrog.rs
+++ b/kernel/src/leapfrog.rs
@@ -965,6 +965,24 @@ pub fn unify_join_zipper_partial(
     run_unify_join(map, factors, var_order, nvars, false).0
 }
 
+/// As [`unify_join_zipper_partial`], but under the projection cut: `cut_mask` names the variables
+/// whose value nothing downstream reads. TEST tooling -- it is how the cut's answers are compared
+/// against the enumeration they stand in for.
+#[cfg(test)]
+fn unify_join_zipper_cut(
+    map: &PathMap<()>,
+    factors: &[Factor],
+    var_order: &[usize],
+    nvars: usize,
+    cut_mask: u64,
+) -> BTreeSet<Vec<Option<Vec<u8>>>> {
+    let plan = join_plan(map, factors, var_order, nvars).expect("factors must flatten into steps");
+    let mut state = join_state(map, &plan, var_order, nvars);
+    state.cut_mask = cut_mask;
+    state.recurse(0);
+    state.out
+}
+
 /// As [`unify_join_zipper_partial`], but returns each answer as one variable-coordinated tuple
 /// encoding (query variables `0..nvars` in order, sharing one intro map), so a free variable that
 /// spans answer positions renders with coordinated NewVar/VarRef the way MORK's emit does.
@@ -1094,6 +1112,7 @@ fn join_state<'a>(
         on_match: None,
         loc_buf: Vec::new(),
         stopped: false,
+        cut_mask: 0,
 
         #[cfg(test)]
         out: BTreeSet::new(),
@@ -1134,11 +1153,13 @@ fn run_unify_join_stream_bindings(
     factors: &[Factor],
     var_order: &[usize],
     nvars: usize,
+    cut_mask: u64,
     on_match: &mut dyn FnMut(&Bindings, Expr) -> bool,
 ) {
     let plan = join_plan(map, factors, var_order, nvars)
         .expect("parsed factors must flatten into steps");
     let mut state = join_state(map, &plan, var_order, nvars);
+    state.cut_mask = cut_mask;
     state.on_match = Some(on_match);
     state.recurse(0);
 }
@@ -1319,6 +1340,7 @@ fn scan_subterm(body: Expr, at: usize, intro: &mut u8) -> Option<SubtermScan> {
 pub fn query_multi_leapfrog<F: FnMut(Result<&[u32], &Bindings>, Expr) -> bool>(
     map: &PathMap<()>,
     pat_expr: Expr,
+    cut_mask: u64,
     mut effect: F,
 ) -> usize {
     // The join owns every body the engine hands it, so parsing is a precondition rather than a
@@ -1355,7 +1377,7 @@ pub fn query_multi_leapfrog<F: FnMut(Result<&[u32], &Bindings>, Expr) -> bool>(
         // per-answer allocation of the emit path (a BTreeMap deep clone) is gone.
         effect(Err(bindings), loc)
     };
-    run_unify_join_stream_bindings(map, &factors, &var_order, nvars, &mut on_match);
+    run_unify_join_stream_bindings(map, &factors, &var_order, nvars, cut_mask, &mut on_match);
     candidate
 }
 
@@ -1456,6 +1478,10 @@ struct UnifyJoin<'a> {
     /// fact as the stock contract's `loc`) here instead of collecting rows, and a `false` return
     /// stops the search. The engine dispatch uses this.
     on_match: Option<&'a mut dyn FnMut(&Bindings, Expr) -> bool>,
+    /// Body variables whose value nothing downstream reads, as
+    /// [`crate::space::Space::projection_cut_mask`] computed it. Zero for every caller with no
+    /// template to project through, which is the unchanged enumeration.
+    cut_mask: u64,
     /// Scratch for the streamed `loc`: factor 0's stored fact bytes, refilled per accepted
     /// assignment so the stream costs no allocation per answer.
     loc_buf: Vec<u8>,
@@ -1584,6 +1610,10 @@ impl UnifyJoin<'_> {
         // The leapfrog principle: lead with the smallest domain so the leading factor enumerates
         // few candidates and the rest seek. This is what makes a selective factor, say (e a $y)
         // with a few edges, drive the join instead of the whole relation.
+        if parts.len() == 1 && v < 64 && (self.cut_mask >> v) & 1 == 1 {
+            self.consume_lead_cut(&parts, 0, v, i);
+            return;
+        }
         self.rank_parts(&mut parts);
         let nr = self.partition_restrictors(&mut parts);
         self.consume_lead(&parts, nr, v, i);
@@ -2105,6 +2135,60 @@ impl UnifyJoin<'_> {
         self.free_bufs.push(buf);
     }
 
+    /// One witness for `v`, whose whole domain nothing downstream reads.
+    ///
+    /// Separate from [`Self::consume_lead`] so the enumerating path keeps the code it had: a
+    /// `cut` branch inside the candidate fill's loops measured 6% on counter_machine. If the
+    /// witness does not match, the level re-runs as a full enumeration, so the cut can only ever
+    /// drop a duplicate.
+    fn consume_lead_cut(&mut self, parts: &[usize], nr: usize, v: usize, i: usize) {
+        if self.stopped {
+            return;
+        }
+        let f = parts[0];
+        let pattern = self.query_var_env(v);
+        let free_key = self
+            .deref_env(pattern)
+            .var_opt()
+            .expect("the lead level runs only for a still-free join variable");
+        let mut buf = self.free_bufs.pop().unwrap_or_default();
+        {
+            // One candidate, wherever the column's enumeration starts.
+            let cur = &mut self.cursors[f];
+            cur.first();
+            if let Some(k) = cur.key() {
+                let vars = cur.key_var_counts();
+                buf.push_from(k, vars);
+            }
+            cur.reset_to_floor();
+        }
+        let mut matched = false;
+        if buf.len > 0 {
+            let cand = &buf.entries[0];
+            let mut cont = |this: &mut Self| {
+                matched = true;
+                this.next_step[f] += 1;
+                this.consume_var_parts(&parts[1..], 0, v, i);
+                this.next_step[f] -= 1;
+            };
+            let vars = buf.meta[0];
+            if vars.1 == 0 {
+                let data_env = self.data_env_for(f, cand, vars);
+                let previous = self.bindings.insert(free_key, data_env);
+                debug_assert!(previous.is_none(), "deref ended at a bound var");
+                self.with_bound_path_bytes(f, cand, 0, &mut cont);
+                self.bindings.remove(&free_key);
+            } else {
+                self.match_candidate(f, pattern, cand, vars, &mut cont);
+            }
+        }
+        buf.len = 0;
+        self.free_bufs.push(buf);
+        if !matched && !self.stopped {
+            self.consume_lead(parts, nr, v, i);
+        }
+    }
+
     /// Consume the confirmed column of each restrictor in turn, then continue. The mutual seek
     /// established that `value` -- a ground symbol -- is stored at this column and that the column
     /// holds no stored variable, so `consume_col` would seek to exactly this value, bind it with no
@@ -2566,6 +2650,67 @@ mod tests {
         v
     }
 
+    /// The projection cut must answer exactly what the enumeration answers, once the variable
+    /// nobody reads is projected away -- and it must actually be doing something, which the
+    /// uncut row count pins.
+    #[test]
+    fn the_projection_cut_keeps_every_answer_it_is_allowed_to_lose() {
+        let mut map = PathMap::<()>::new();
+        map.insert(&nest("r", &[sym("a")]), ());
+        map.insert(&nest("r", &[sym("b")]), ());
+        // `a` witnesses four values of the don't-care column, `b` exactly one: the cut has to
+        // collapse the four without losing `b`, whose only witness is the last one.
+        for w in ["p", "q", "s", "t"] {
+            map.insert(&nest("s", &[sym("a"), sym(w)]), ());
+        }
+        map.insert(&nest("s", &[sym("b"), sym("t")]), ());
+
+        // (, (r $x) (s $x $_)) -- $x is 0, the don't-care is 1.
+        let body = conj(&[
+            nest("r", &[new_var()]),
+            nest("s", &[var_ref(0), new_var()]),
+        ]);
+        let be = Expr::from_slice(&body);
+        let (factors, nvars) = parse_body_factors(&be).unwrap();
+        let var_order: Vec<usize> = (0..nvars).collect();
+        assert_eq!(nvars, 2);
+
+        let full = unify_join_zipper_cut(&map, &factors, &var_order, nvars, 0);
+        let cut = unify_join_zipper_cut(&map, &factors, &var_order, nvars, 1 << 1);
+
+        // The cut is not vacuous: the enumeration answers five rows, the cut two.
+        assert_eq!(full.len(), 5);
+        assert_eq!(cut.len(), 2);
+        // Projected on the variable anything downstream can actually read, they agree.
+        let project = |rows: &BTreeSet<Vec<Option<Vec<u8>>>>| -> BTreeSet<Option<Vec<u8>>> {
+            rows.iter().map(|row| row[0].clone()).collect()
+        };
+        assert_eq!(project(&cut), project(&full));
+        assert_eq!(project(&cut).len(), 2);
+    }
+
+    /// The mask is computed in `space.rs` over the body's bytes and indexed in the join by the id
+    /// `parse_body_factors` assigns. Both number variables by first occurrence; this pins that
+    /// they agree, because a disagreement would silently cut the WRONG variable.
+    #[test]
+    fn the_masks_variable_numbering_is_the_joins_numbering() {
+        let body = conj(&[
+            nest("r", &[new_var(), new_var()]),
+            nest("s", &[var_ref(1), new_var()]),
+        ]);
+        let be = Expr::from_slice(&body);
+        let (factors, nvars) = parse_body_factors(&be).unwrap();
+        assert_eq!(nvars, 3);
+        // The join reads the third variable as the second ARGUMENT of factor 1 ...
+        // Column 0 is the relation head, so the second argument is `cols[2]`.
+        let FactorColumn::Var(last) = factors[1].cols[2] else { panic!("expected a join variable") };
+        assert_eq!(last, 2);
+        // ... and the mask, given a template that reads only the first two, names that same one.
+        let tpl = nest("out", &[var_ref(0), var_ref(1)]);
+        let mask = crate::space::Space::projection_cut_mask(be, &[ExprEnv::new(0, Expr::from_slice(&tpl))]);
+        assert_eq!(mask, 1 << last);
+    }
+
     #[test]
     fn safe_body_routes_flat_ground_answers() {
         let mut map = PathMap::<()>::new();
diff --git a/kernel/src/main.rs b/kernel/src/main.rs
index 5ca02c01..4f6a0b1a 100644
--- a/kernel/src/main.rs
+++ b/kernel/src/main.rs
@@ -1,7 +1,7 @@
 #![feature(string_from_utf8_lossy_owned)]
 
 use mork::{expr, prefix, sexpr, space};
-use mork::space::{transitions, unifications, writes, Space, ACT_PATH};
+use mork::space::{transitions, unifications, writes, Space, act_path};
 use mork_frontend::bytestring_parser::Parser;
 use mork_expr::{item_byte, serialize, SourceItem, Tag};
 use pathmap::PathMap;
@@ -852,6 +852,80 @@ f
 /// A bare top-level SYMBOL conjunct is an existence check on that atom: the body fires when the
 /// symbol is present and never when it is absent. It is also a shape the leapfrog join declines
 /// (no arity, so no columns to seek), so this covers the fallback under either feature setting.
+/// The projection cut: a body variable no template reads, mentioned once, in its conjunct's
+/// trailing run, may be answered with ONE witness instead of its whole domain. What matters is
+/// that this never changes the answer set -- so every shape below is checked, including the ones
+/// the cut must refuse.
+fn projection_cut_variables() {
+    let mut s = Space::new();
+
+    const SPACE_EXPRS: &str = r#"
+(r a)
+(r b)
+(s a p)
+(s a q)
+(s a t)
+(s b t)
+(gg p 1)
+(gg p 2)
+(gg q 3)
+(hh (kk p 1))
+(hh (kk p 2))
+(hh (kk q 3))
+(jl 1)
+(jl 2)
+(jl 3)
+(jr 2)
+(jr 3)
+(jr 4)
+(je 7)
+(sv k plain)
+(sv k (f $z))
+(sv k (g $w $v))
+(exec (0 0) (, (r $x) (s $x $_)) (, (cut1 $x)))
+(exec (0 1) (, (gg $m $n)) (, (keep1 $n)))
+(exec (0 2) (, (hh (kk $mm $nn))) (, (keep2 $nn)))
+(exec (0 3) (, (jl $p) (jr $p) (je $q)) (, (keep3 $q)))
+(exec (0 4) (, (sv $y $_)) (, (cut2 $y)))
+    "#;
+
+    s.add_all_sexpr(SPACE_EXPRS.as_bytes()).unwrap();
+    let t0 = Instant::now();
+    let steps = s.metta_calculus(1000000000000000);
+    println!("elapsed {} steps {} size {}", t0.elapsed().as_millis(), steps, s.btm.val_count());
+
+    let mut v = vec![];
+    s.dump_all_sexpr(&mut v).unwrap();
+    let res = String::from_utf8_lossy_owned(v);
+    println!("result: {res}");
+    let rows = |p: &str| res.lines().filter(|l| l.starts_with(p)).count();
+
+    // `$_` is trailing, mentioned once, and unread: `a` has three witnesses and `b` one, and the
+    // answer is one row each either way.
+    assert!(res.contains("(cut1 a)
+") && res.contains("(cut1 b)
+"), "both keys must answer");
+    assert_eq!(rows("(cut1 "), 2, "one row per key, whatever the fan-out");
+
+    // A witness may be schematic. `(f $z)` is what a leftmost descent reaches -- an arity byte
+    // sorts below a symbol byte -- so this is also the shape that catches a cut reporting a
+    // variable-carrying fact as ground.
+    assert_eq!(rows("(cut2 "), 1, "schematic witnesses collapse to the one key");
+    assert!(res.contains("(cut2 k)
+"));
+
+    // `$m` is NOT trailing: it decides which subtrie `$n` is drawn from, so pinning it would drop
+    // `$n` values rather than duplicates. All three must survive, nested or not.
+    assert_eq!(rows("(keep1 "), 3, "a non-trailing don't-care must keep enumerating");
+    assert_eq!(rows("(keep2 "), 3, "... one level down as well");
+
+    // `$p` is unread but mentioned twice, so it is a join variable and must still intersect:
+    // jl and jr agree on 2 and 3, so the body holds and `$q` comes through exactly once.
+    assert_eq!(rows("(keep3 "), 1, "a repeated variable is a join variable, not a don't-care");
+    assert!(res.contains("(keep3 7)
+"));
+}
+
 fn top_level_symbol() {
     let mut s = Space::new();
 
@@ -1324,7 +1398,10 @@ fn sink_hash_expr() {
     let res = String::from_utf8_lossy_owned(v);
 
     println!("result: {res}");
-    assert_eq!(res, "(result XoicVnQv2bk)\n(result tspt4QCdRB8)\n");
+    // gxhash 3.x, which #146 made actually compile -- the previous constants came from the
+    // hasher that was silently used while the `gxhash` cfg never matched. Stable across
+    // platforms for a given major version, per gxhash's own guarantee.
+    assert_eq!(res, "(result -Egab4rQ3Nc)\n(result ru8oOBGFlq0)\n");
 }
 
 fn sink_even_half() {
@@ -1973,7 +2050,7 @@ fn source_act_two_bipolar_equal_crossed() {
     "#;
 
         act_s.add_all_sexpr(SPACE_EXPRS.as_bytes()).unwrap();
-        act_s.backup_tree(format!("{ACT_PATH}two_bipolar_equal_crossed.act")).unwrap();
+        act_s.backup_tree(format!("{}two_bipolar_equal_crossed.act", act_path())).unwrap();
     };
 
     let mut s = Space::new();
@@ -2005,7 +2082,7 @@ fn source_space_act_two_bipolar_equal_crossed() {
     "#;
 
         act_s.add_all_sexpr(SPACE_EXPRS.as_bytes()).unwrap();
-        act_s.backup_tree(format!("{ACT_PATH}space_two_bipolar_equal_crossed.act")).unwrap();
+        act_s.backup_tree(format!("{}space_two_bipolar_equal_crossed.act", act_path())).unwrap();
     };
 
     let mut s = Space::new();
@@ -2998,7 +3075,7 @@ fn sink_act_readback() {
 
     {
         let mut s = Space::new();
-        s.restore_tree(format!("{}sink_act_readback.act", ACT_PATH));
+        s.restore_tree(format!("{}sink_act_readback.act", act_path()));
         let mut v = vec![];
         s.dump_all_sexpr(&mut v).unwrap();
         let res = String::from_utf8_lossy_owned(v);
@@ -3026,7 +3103,7 @@ fn sink_act_mixed_readback() {
 
     {
         let mut s = Space::new();
-        s.restore_tree(format!("{}sink_act_mixed_readback.act", ACT_PATH));
+        s.restore_tree(format!("{}sink_act_mixed_readback.act", act_path()));
         let mut v = vec![];
         s.dump_all_sexpr(&mut v).unwrap();
         let res = String::from_utf8_lossy_owned(v);
@@ -3632,7 +3709,7 @@ fn bench_logic_query_act() {
 
     // let mut expr_buf = vec![];
     // std::fs::File::open(format!("{PROJECT_PATH}/resources/big.act")).unwrap().read_to_end(&mut expr_buf).unwrap();
-    std::fs::copy(format!("{PROJECT_PATH}/resources/big.act"), format!("{}big.act", ACT_PATH));
+    std::fs::copy(format!("{PROJECT_PATH}/resources/big.act"), format!("{}big.act", act_path()));
 
     let mut t0 = Instant::now();
     s.add_all_sexpr(b"(exec 0 (I (ACT big (axiom $x)) (ACT big (axiom $x))) (, (combined $x)))").unwrap();
@@ -6279,6 +6356,7 @@ fn main() {
             data_varref_absorbs_query_compound_newvars();
             top_level_match();
             top_level_symbol();
+            projection_cut_variables();
             large_statement();
 
             process_calculus_reverse();
diff --git a/kernel/src/sinks.rs b/kernel/src/sinks.rs
index 4c6bacbf..084e6310 100644
--- a/kernel/src/sinks.rs
+++ b/kernel/src/sinks.rs
@@ -30,7 +30,7 @@ use eval::EvalScope;
 use eval_ffi::{ExprSink, ExprSource};
 use mork_expr::macros::SerializableExpr;
 use crate::{expr, pure};
-use crate::space::ACT_PATH;
+use crate::space::act_path;
 
 #[derive(Eq, PartialEq, Debug)]
 pub enum WriteResourceRequest {
@@ -329,7 +329,7 @@ impl Sink for ACTSink {
         trace!(target: "sink", "ACT finalizing");
         let _ = it.next().unwrap() else { unreachable!() };
         pathmap::arena_compact::ArenaCompactTree::dump_from_zipper(
-            self.tmp.read_zipper(), |_v| 0, format!("{}{}.act", ACT_PATH, self.file)).map(|_tree| ());
+            self.tmp.read_zipper(), |_v| 0, format!("{}{}.act", act_path(), self.file)).map(|_tree| ());
         true
     }
 }
diff --git a/kernel/src/space.rs b/kernel/src/space.rs
index df99a3a6..fcfe1e76 100644
--- a/kernel/src/space.rs
+++ b/kernel/src/space.rs
@@ -32,8 +32,44 @@ pub static mut transitions: usize = 0;
 pub static mut unifications: usize = 0;
 pub static mut writes: usize = 0;
 
-pub static ACT_PATH: &'static str = "/dev/shm/";
-// pub static ACT_PATH: &'static str = "/mnt/data/";
+/// Where `ArenaCompactTree` files are written and mmapped from, always ending in a separator.
+///
+/// Set the `ACT_PATH` environment variable to choose the directory. Otherwise the default is the
+/// best temporary location the platform offers: on Linux `/dev/shm`, a tmpfs, so an ACT never
+/// reaches a disk; elsewhere the OS temp directory, which is `TMPDIR` on macOS (launchd always
+/// sets it, per-user) and `TEMP`/`TMP` on Windows -- neither has a `/dev/shm` to fall back to,
+/// which is why the old hardcoded one made every ACT test fail off Linux.
+///
+/// The directory is created if it does not exist, so a caller pointing `ACT_PATH` at a fresh
+/// path does not have to make it first.
+pub fn act_path() -> &'static str {
+    static PATH: std::sync::OnceLock<String> = std::sync::OnceLock::new();
+    PATH.get_or_init(|| {
+        let mut p = std::env::var("ACT_PATH")
+            .ok()
+            .filter(|s| !s.is_empty())
+            .unwrap_or_else(default_act_dir);
+        if !p.ends_with('/') && !p.ends_with(std::path::MAIN_SEPARATOR) {
+            p.push(std::path::MAIN_SEPARATOR);
+        }
+        if let Err(e) = std::fs::create_dir_all(&p) {
+            warn!(target: "act", "ACT_PATH {p} is not usable: {e}");
+        }
+        p
+    })
+}
+
+fn default_act_dir() -> String {
+    #[cfg(target_os = "linux")]
+    {
+        // A tmpfs when it is mounted, which is the point: an ACT stays in memory.
+        if std::path::Path::new("/dev/shm").is_dir() {
+            return "/dev/shm".to_string();
+        }
+    }
+    // `temp_dir` reads TMPDIR on macOS and TEMP/TMP on Windows, and falls back to /tmp on unix.
+    std::env::temp_dir().to_string_lossy().into_owned()
+}
 
 /// The pattern's distinct variables as a synthetic expression of `n` `NewVar`s. Only the debug
 /// cross-check of [`mork_expr::pattern_cycles_and_intros`] applies it now; the live path needs no
@@ -109,8 +145,35 @@ pub(crate) const VARS: [u64; 4] = {
 // - `references` can be elided by not putting the virtual $ Expr's on the `stack` such that _k maps directly to the indices
 // - keeping a needle instead of a stack to avoid the `reverse` (would also create the opportunity to be even more lazy about instruction gen)
 // - use descend_to and re-evaluated the added sub-path to do much better on long paths
+/// Descend the FIRST complete subterm below the focus, reporting how many bytes that took (0 if
+/// the focus is a dead end) and OR-ing into `var_facts` the bit of every factor whose bytes the
+/// descent found a variable in.
+///
+/// That second job is not optional. `vs!` is the only other place the walk learns a candidate is
+/// non-ground, and this descent goes around it: a leftmost subterm may well carry a variable --
+/// an arity byte sorts below a symbol byte, so a compound like `(f $z)` is exactly what gets
+/// picked -- and reporting the fact as ground would let a consumer stamp it so.
+fn descend_first_subterm<Z : ZipperMoving + Zipper + ZipperProduct>(loc: &mut Z, var_facts: &mut u64) -> usize {
+    let (mut owed, mut payload) = (1u32, 0u32);
+    let mut n = 0usize;
+    while owed > 0 || payload > 0 {
+        if !loc.descend_first_byte() {
+            loc.ascend(n);
+            return 0;
+        }
+        n += 1;
+        let b = *loc.path().last().unwrap();
+        let head = payload == 0;
+        mork_expr::subterm_parse_step(b, &mut owed, &mut payload);
+        if head && matches!(byte_item(b), Tag::NewVar | Tag::VarRef(_)) {
+            *var_facts |= 1u64 << loc.focus_factor().min(63);
+        }
+    }
+    n
+}
+
 fn coreferential_transition<Z : ZipperProduct, F: FnMut(&mut Z, u64) -> ()>(
-    loc: &mut Z, mut stack: &mut Vec<ExprEnv>, references: &mut Vec<u32>, var_facts: u64, f: &mut F) {
+    loc: &mut Z, mut stack: &mut Vec<ExprEnv>, references: &mut Vec<u32>, var_facts: u64, cut_mask: u64, f: &mut F) {
     macro_rules! vs {
         ($e:expr, $nv:expr) => {{
             let m = loc.child_mask().and(&ByteMask(VARS));
@@ -133,7 +196,7 @@ fn coreferential_transition<Z : ZipperProduct, F: FnMut(&mut Z, u64) -> ()>(
                 loc.descend_to_byte(b);
                 debug_assert!(loc.path_exists());
                 let vf = var_facts | (1u64 << loc.focus_factor().min(63));
-                coreferential_transition(loc, stack, references, vf, f);
+                coreferential_transition(loc, stack, references, vf, cut_mask, f);
                 if !loc.ascend_byte() { unreachable_unchecked() };
             }
         }};
@@ -158,6 +221,20 @@ fn coreferential_transition<Z : ZipperProduct, F: FnMut(&mut Z, u64) -> ()>(
                         Some((idx, prev))
                     } else { None };
 
+                    // One witnessing subterm stands for the whole subtrie, so take the leftmost
+                    // instead of enumerating every variable, size class and arity below here.
+                    if e.n == 0 && e.v < 64 && (cut_mask >> e.v) & 1 == 1 {
+                        let mut vf = var_facts;
+                        let n = descend_first_subterm(loc, &mut vf);
+                        if n > 0 {
+                            coreferential_transition(loc, stack, references, vf, cut_mask, f);
+                            loc.ascend(n);
+                        }
+                        if let Some((idx, prev)) = restore { references[idx] = prev; }
+                        stack.push(e);
+                        return;
+                    }
+
                     vs!(e, true);
 
                     let m = loc.child_mask().and(&ByteMask(SIZES));
@@ -168,7 +245,7 @@ fn coreferential_transition<Z : ZipperProduct, F: FnMut(&mut Z, u64) -> ()>(
                         debug_assert!(loc.path_exists());
                         if !loc.descend_first_k_path(size as _) { unreachable_unchecked() }
                         loop {
-                            coreferential_transition(loc, stack, references, var_facts, f);   
+                            coreferential_transition(loc, stack, references, var_facts, cut_mask, f);   
                             if !loc.to_next_k_path(size as _) { break }
                         }
                         if !loc.ascend_byte() { unreachable_unchecked() }
@@ -183,7 +260,7 @@ fn coreferential_transition<Z : ZipperProduct, F: FnMut(&mut Z, u64) -> ()>(
                         static nv: u8 = item_byte(Tag::NewVar);
                         let ol = stack.len();
                         for _ in 0..a { stack.push(ExprEnv::new(255, Expr { ptr: ((&nv) as *const u8).cast_mut() })) }
-                        coreferential_transition(loc, stack, references, var_facts, f);
+                        coreferential_transition(loc, stack, references, var_facts, cut_mask, f);
                         stack.truncate(ol);
                         if !loc.ascend_byte() { unreachable_unchecked() };
                     }
@@ -209,14 +286,14 @@ fn coreferential_transition<Z : ZipperProduct, F: FnMut(&mut Z, u64) -> ()>(
                     };
                     stack.push(addition);
                     vs!(e, false);
-                    coreferential_transition(loc, stack, references, var_facts, f);
+                    coreferential_transition(loc, stack, references, var_facts, cut_mask, f);
                     stack.pop();
                 }
                 Tag::SymbolSize(size) => {
                     vs!(e, false);
                     if loc.descend_to_existing_byte(e_byte) {
                         if loc.descend_to_check(&*slice_from_raw_parts(e.base.ptr.byte_add(e.offset as usize + 1), size as usize)) {
-                            coreferential_transition(loc, stack, references, var_facts, f);
+                            coreferential_transition(loc, stack, references, var_facts, cut_mask, f);
                         }
                         loc.ascend((size as usize) + 1); // The expression length + the e_byte
                     }
@@ -227,7 +304,7 @@ fn coreferential_transition<Z : ZipperProduct, F: FnMut(&mut Z, u64) -> ()>(
                         let stackl = stack.len();
                         e.args(&mut stack);
                         stack[stackl..].reverse();
-                        coreferential_transition(loc, stack, references, var_facts, f);
+                        coreferential_transition(loc, stack, references, var_facts, cut_mask, f);
                         stack.truncate(stack.len() - arity as usize);
                         loc.ascend_byte();
                     }
@@ -1098,22 +1175,128 @@ impl Space {
     /// which `query_multi` handles (or fails on) exactly as it always has, plus the encoding
     /// pathologies `parse_body_factors` rejects (a `VarRef` naming a variable the body never
     /// introduced, or more than `u8::MAX` variables).
-    pub fn query_multi_dispatch<F : FnMut(Result<&[u32], &Bindings>, Expr) -> bool>(btm: &PathMap<()>, pat_expr: Expr, mut effect: F) -> usize {
+    /// The body variables no template reads, that the body mentions once, and that sit in their
+    /// conjunct's trailing run. A bitmask over the body's variable numbering (`NewVar`s in
+    /// first-occurrence order), which is what both engines index by.
+    ///
+    /// The trailing-run condition is the soundness one: anything earlier in a conjunct decides
+    /// which subtrie the later columns come from, so `(s (f $_) $y)` must keep enumerating `$_`
+    /// while `(s $y (f $_))` need not.
+    pub fn projection_cut_mask(pat_expr: Expr, templates: &[ExprEnv]) -> u64 {
+        let head = unsafe { *pat_expr.ptr };
+        let Tag::Arity(nargs) = byte_item(head) else { return 0 };
+        debug_assert!((nargs as usize) < 64, "byte_item masks an arity to six bits");
+
+        // One pass over the body, from the pointer: count every variable's mentions, and record
+        // per conjunct how long its trailing run of `NewVar`s is and how many variables its end
+        // had numbered.
+        let mut occ = [0u32; 64];
+        let mut nv = 0usize;
+        let mut runs = [(0u8, 0u8); 64];
+        let mut any_run = false;
+        let mut i = 1usize;
+        for c in 0..nargs as usize {
+            let (mut owed, mut payload) = (1u32, 0u32);
+            let mut run = 0u8;
+            while owed > 0 {
+                let b = unsafe { *pat_expr.ptr.add(i) };
+                let tag = byte_item(b);
+                i += 1;
+                owed -= 1;
+                match tag {
+                    // A symbol's payload is stepped over in one go, so this walk is per ITEM.
+                    Tag::SymbolSize(size) => { i += size as usize; run = 0; }
+                    Tag::Arity(a) => { owed += a as u32; run = 0; }
+                    Tag::NewVar => {
+                        // The encoding caps a routable body at 63 variables, and a mask cannot
+                        // name what it cannot index: a body past the cap simply opts out.
+                        if nv >= 64 { return 0 }
+                        occ[nv] += 1;
+                        nv += 1;
+                        run = run.saturating_add(1);
+                    }
+                    Tag::VarRef(r) => {
+                        debug_assert!((r as usize) < 64, "byte_item masks a VarRef to six bits");
+                        occ[r as usize] += 1;
+                        run = 0;
+                    }
+                }
+                let _ = payload;
+            }
+            debug_assert!(nv <= 64);
+            runs[c] = (run, nv as u8);
+            any_run |= run > 0;
+        }
+        if !any_run { return 0 }
+
+        let trailing = |runs: &[(u8, u8); 64], read: u64| -> u64 {
+            let mut m = 0u64;
+            for c in 0..nargs as usize {
+                let (run, end) = runs[c];
+                for k in 0..run as usize {
+                    let Some(v) = (end as usize).checked_sub(1 + k) else { break };
+                    if occ[v] != 1 || (read >> v) & 1 == 1 { break }
+                    m |= 1u64 << v;
+                }
+            }
+            m
+        };
+        // Only a variable mentioned once can be cut; if none survives that, no template is read.
+        let candidates = trailing(&runs, 0);
+        if candidates == 0 { return 0 }
+
+        // Now earned: which of them does some template read? A ground-stamped template holds no
+        // variable by the stamp's own contract, so it is skipped without being walked.
+        let mut read = 0u64;
+        for t in templates.iter() {
+            if t.ground_stamp() != 0 { continue }
+            let e = t.subsexpr();
+            let (mut owed, mut j) = (1u32, 0usize);
+            while owed > 0 {
+                let b = unsafe { *e.ptr.add(j) };
+                j += 1;
+                owed -= 1;
+                match byte_item(b) {
+                    Tag::SymbolSize(size) => j += size as usize,
+                    Tag::Arity(a) => owed += a as u32,
+                    Tag::NewVar => {}
+                    Tag::VarRef(r) => {
+                        debug_assert!((r as usize) < 64, "byte_item masks a VarRef to six bits");
+                        read |= 1u64 << r;
+                    }
+                }
+            }
+            // Every candidate is spoken for; nothing can be cut, so stop reading templates.
+            if read & candidates == candidates { return 0 }
+        }
+
+        // A read variable stops its conjunct's run at that point, not just for itself.
+        trailing(&runs, read)
+    }
+
+    pub fn query_multi_dispatch<F : FnMut(Result<&[u32], &Bindings>, Expr) -> bool>(btm: &PathMap<()>, pat_expr: Expr, cut_mask: u64, mut effect: F) -> usize {
         // Which engine answers the space-to-space transform is a compile-time choice and nothing
         // more: with the `leapfrog` feature the join owns every body, and without it the module
         // does not exist. `query_multi` stays reachable for the paths that are not dispatched --
         // the pattern-directed dumps and the interpreted source/sink transforms.
         #[cfg(feature = "leapfrog")]
         {
-            crate::leapfrog::query_multi_leapfrog(btm, pat_expr, effect)
+            crate::leapfrog::query_multi_leapfrog(btm, pat_expr, cut_mask, effect)
         }
         #[cfg(not(feature = "leapfrog"))]
         {
-            Self::query_multi(btm, pat_expr, effect)
+            Self::query_multi_proj(btm, pat_expr, cut_mask, effect)
         }
     }
 
-    pub fn query_multi<F : FnMut(Result<&[u32], &Bindings>, Expr) -> bool>(btm: &PathMap<()>, pat_expr: Expr, mut effect: F) -> usize {
+    pub fn query_multi<F : FnMut(Result<&[u32], &Bindings>, Expr) -> bool>(btm: &PathMap<()>, pat_expr: Expr, effect: F) -> usize {
+        Self::query_multi_proj(btm, pat_expr, 0, effect)
+    }
+
+    /// [`Self::query_multi`] under the projection cut: `cut_mask` names the body variables whose
+    /// value nothing downstream reads, which the descent answers with one subterm instead of
+    /// every one. A zero mask is the unchanged walk.
+    pub fn query_multi_proj<F : FnMut(Result<&[u32], &Bindings>, Expr) -> bool>(btm: &PathMap<()>, pat_expr: Expr, cut_mask: u64, mut effect: F) -> usize {
         let pat_newvars = pat_expr.newvars();
         trace!(target: "query_multi", "pattern (newvars={}) {:?}", pat_newvars, serialize(unsafe { pat_expr.span().as_ref().unwrap() }));
         let n_factors = pat_expr.arity().unwrap() as usize;
@@ -1130,7 +1313,7 @@ impl Space {
         }));
         prz.reserve_buffers(1 << 32, 32);
 
-        Self::query_multi_raw(&mut prz, &pat_args[1..], effect)
+        Self::query_multi_raw_proj(&mut prz, &pat_args[1..], cut_mask, effect)
     }
 
     #[inline]
@@ -1145,7 +1328,7 @@ impl Space {
             ResourceRequest::ACT(name) => {
                 let act = mmaps.as_mut().unwrap().entry(OwnedSourceItem::from(name)).or_insert_with(|| {
                     trace!(target: "query_multi_i", "open new ACT {}", name);
-                    ArenaCompactTree::open_mmap(format!("{ACT_PATH}{name}.act")).unwrap()
+                    ArenaCompactTree::open_mmap(format!("{}{name}.act", act_path())).unwrap()
                 });
                 trace!(target: "query_multi_i", "taking RZ of {}", name);
                 Resource::ACT(act.read_zipper())
@@ -1257,9 +1440,15 @@ impl Space {
         }
     }
 
-    #[cfg(feature="no_search")]
+    /// The zero-mask wrapper every other caller keeps using: sinks, dumps and the interpreted
+    /// source/sink transforms are byte-for-byte the unchanged walk.
     #[inline(always)]
-    pub fn query_multi_raw<PZ : ZipperProduct, F : FnMut(Result<&[u32], &Bindings>, Expr) -> bool>(mut prz: &mut PZ, sources: &[ExprEnv], mut effect: F) -> usize {
+    pub fn query_multi_raw<PZ : ZipperProduct, F : FnMut(Result<&[u32], &Bindings>, Expr) -> bool>(prz: &mut PZ, sources: &[ExprEnv], effect: F) -> usize {
+        Self::query_multi_raw_proj(prz, sources, 0, effect)
+    }
+
+    #[cfg(feature="no_search")]
+    pub fn query_multi_raw_proj<PZ : ZipperProduct, F : FnMut(Result<&[u32], &Bindings>, Expr) -> bool>(mut prz: &mut PZ, sources: &[ExprEnv], cut_mask: u64, mut effect: F) -> usize {
         let mut candidate = 0;
         // One pair buffer for the whole enumeration: `unify` drains it, so a `clear` per
         // candidate makes it allocation-free after warmup.
@@ -1324,7 +1513,7 @@ impl Space {
 
     #[cfg(not(feature="no_search"))]
     #[inline(always)]
-    pub fn query_multi_raw<PZ : ZipperProduct, F : FnMut(Result<&[u32], &Bindings>, Expr) -> bool>(mut prz: &mut PZ, sources: &[ExprEnv], mut effect: F) -> usize {
+    pub fn query_multi_raw_proj<PZ : ZipperProduct, F : FnMut(Result<&[u32], &Bindings>, Expr) -> bool>(mut prz: &mut PZ, sources: &[ExprEnv], cut_mask: u64, mut effect: F) -> usize {
         let mut stack = sources[0..].iter().rev().cloned().collect::<Vec<_>>();
 
         let mut references: Vec<u32> = vec![];
@@ -1338,7 +1527,7 @@ impl Space {
 
         BREAK.with_borrow_mut(|a| {
             if unsafe { setjmp(a) == 0 } {
-                coreferential_transition(prz, &mut stack, unsafe { ((&references) as *const Vec<u32>).cast_mut().as_mut().unwrap() }, 0u64, &mut |loc, var_facts| {
+                coreferential_transition(prz, &mut stack, unsafe { ((&references) as *const Vec<u32>).cast_mut().as_mut().unwrap() }, 0u64, cut_mask, &mut |loc, var_facts| {
                     let e = Expr { ptr: loc.origin_path().as_ptr().cast_mut() };
                     trace!(target: "query_multi", "pi {:?}", loc.path_indices());
                     trace!(target: "query_multi", "at {:?}", e);
@@ -1364,6 +1553,25 @@ impl Space {
                         let span_stamp = |k: usize, start: usize, end: usize| -> u16 {
                             let len = end - start;
                             let ground = var_facts & (1u64 << k.min(63)) == 0;
+                            // `stamp_ground` is unsafe for a reason: a stamp on a span that does
+                            // hold a variable makes consumers settle by memcmp and skip variable
+                            // hunts over it. Re-derive the answer here in debug builds so any
+                            // path that reaches the leaf with a wrong bit is caught at the source
+                            // rather than as a wrong answer somewhere downstream.
+                            #[cfg(debug_assertions)]
+                            if ground {
+                                let mut j = start;
+                                while j < end {
+                                    match byte_item(opath[j]) {
+                                        Tag::SymbolSize(size) => j += 1 + size as usize,
+                                        Tag::NewVar | Tag::VarRef(_) => {
+                                            panic!("fact {k} reported ground but holds a variable \
+                                                    at byte {j} of [{start},{end})");
+                                        }
+                                        Tag::Arity(_) => j += 1,
+                                    }
+                                }
+                            }
                             if ground && len <= u16::MAX as usize { len as u16 } else { 0 }
                         };
 
@@ -1475,6 +1683,10 @@ impl Space {
         let mut tpl_args = Vec::with_capacity(64);
         ExprEnv::new(0, tpl_expr).args(&mut tpl_args);
         let mut templates: Vec<_> = tpl_args[1..].iter().map(|ee| ee.subsexpr()).collect();
+        // The cut drops duplicate answers, so only a sink idempotent in them may use it: this
+        // plain `,` -> `,` form writes into the trie, while `O` and the source/sink transforms
+        // can aggregate over how many answers arrive.
+        let cut_mask = Self::projection_cut_mask(pat_expr, &tpl_args[1..]);
         let mut template_prefixes: Vec<_> = templates.iter().map(|e| unsafe { e.prefix().unwrap_or_else(|x| x).as_ref().unwrap() }).collect();
         let mut subsumption = Self::prefix_subsumption(&template_prefixes[..]);
         let mut placements = subsumption.clone();
@@ -1520,7 +1732,7 @@ impl Space {
 
 
         let mut any_new = false;
-        let touched = Self::query_multi_dispatch(&read_copy, pat_expr, |refs_bindings, loc| 'query:{
+        let touched = Self::query_multi_dispatch(&read_copy, pat_expr, cut_mask, |refs_bindings, loc| 'query:{
             trace!(target: "transform", "data {}", serialize(unsafe { loc.span().as_ref().unwrap()}));
             unsafe { writes += template_prefixes.len(); }
             match refs_bindings {
@@ -2031,4 +2243,141 @@ impl Drop for Space {
             drop(z3.stdin.take())
         }
     }
-}
\ No newline at end of file
+}
+
+#[cfg(test)]
+mod projection_cut_tests {
+    use super::*;
+
+    fn sym(t: &str) -> Vec<u8> {
+        let mut v = vec![item_byte(Tag::SymbolSize(t.len() as u8))];
+        v.extend_from_slice(t.as_bytes());
+        v
+    }
+    fn raw_sym(payload: &[u8]) -> Vec<u8> {
+        let mut v = vec![item_byte(Tag::SymbolSize(payload.len() as u8))];
+        v.extend_from_slice(payload);
+        v
+    }
+    fn nest(parts: &[Vec<u8>]) -> Vec<u8> {
+        let mut v = vec![item_byte(Tag::Arity(parts.len() as u8))];
+        for p in parts { v.extend_from_slice(p) }
+        v
+    }
+    fn rel(name: &str, args: &[Vec<u8>]) -> Vec<u8> {
+        let mut parts = vec![sym(name)];
+        parts.extend_from_slice(args);
+        nest(&parts)
+    }
+    fn conj(factors: &[Vec<u8>]) -> Vec<u8> {
+        let mut parts = vec![sym(",")];
+        parts.extend_from_slice(factors);
+        nest(&parts)
+    }
+    fn nv() -> Vec<u8> { vec![item_byte(Tag::NewVar)] }
+    fn vr(i: u8) -> Vec<u8> { vec![item_byte(Tag::VarRef(i))] }
+
+    fn mask(body: &[u8], templates: &[Vec<u8>]) -> u64 {
+        let be = Expr::from_slice(body);
+        let ts: Vec<ExprEnv> = templates
+            .iter()
+            .map(|t| ExprEnv::new(0, Expr::from_slice(&t[..])))
+            .collect();
+        Space::projection_cut_mask(be, &ts[..])
+    }
+
+    #[test]
+    fn trailing_singleton_no_template_reads_is_cut() {
+        // (, (r $x $y) (s $y $_))  ->  (out $x $y):  only $_ (index 2) is cuttable.
+        let body = conj(&[rel("r", &[nv(), nv()]), rel("s", &[vr(1), nv()])]);
+        let tpl = rel("out", &[vr(0), vr(1)]);
+        assert_eq!(mask(&body, &[tpl]), 1 << 2);
+    }
+
+    #[test]
+    fn a_variable_a_template_reads_is_never_cut() {
+        // The same body, but the template now reads $_ as well: nothing is cuttable.
+        let body = conj(&[rel("r", &[nv(), nv()]), rel("s", &[vr(1), nv()])]);
+        let tpl = rel("out", &[vr(0), vr(2)]);
+        assert_eq!(mask(&body, &[tpl]), 0);
+    }
+
+    #[test]
+    fn a_repeated_variable_is_never_cut() {
+        // $y and $z are join variables: no template reads them, but pinning one to a single
+        // value would change which tuples the OTHER factors can still match.
+        let body = conj(&[
+            rel("r", &[nv(), nv()]),
+            rel("s", &[vr(1), nv()]),
+            rel("t", &[vr(2)]),
+        ]);
+        let tpl = rel("out", &[vr(0)]);
+        assert_eq!(mask(&body, &[tpl]), 0);
+    }
+
+    #[test]
+    fn only_the_conjuncts_trailing_run_is_cut() {
+        // (, (s (f $_) $y)): $_ decides the subtrie $y is drawn from, so it must keep
+        // enumerating even though nothing reads it.
+        let body = conj(&[rel("s", &[rel("f", &[nv()]), nv()])]);
+        let tpl = rel("out", &[vr(1)]);
+        assert_eq!(mask(&body, &[tpl]), 0);
+        // Swapped, the same variable IS the trailing item -- nested inside `(f ...)` or not.
+        let body = conj(&[rel("s", &[nv(), rel("f", &[nv()])])]);
+        let tpl = rel("out", &[vr(0)]);
+        assert_eq!(mask(&body, &[tpl]), 1 << 1);
+    }
+
+    #[test]
+    fn a_run_of_trailing_dont_cares_is_cut_whole() {
+        let body = conj(&[rel("s", &[nv(), nv(), nv()])]);
+        let tpl = rel("out", &[vr(0)]);
+        assert_eq!(mask(&body, &[tpl]), (1 << 1) | (1 << 2));
+    }
+
+    #[test]
+    fn every_template_is_consulted() {
+        // The second template is the only reader of $y: one template is not enough to conclude
+        // a variable is unread.
+        let body = conj(&[rel("r", &[nv(), nv()])]);
+        let first = rel("out", &[vr(0)]);
+        let second = rel("also", &[vr(1)]);
+        assert_eq!(mask(&body, &[first.clone()]), 1 << 1);
+        assert_eq!(mask(&body, &[first, second]), 0);
+    }
+
+    #[test]
+    fn a_symbol_payload_that_spells_a_variable_tag_is_not_read_as_one() {
+        // The payload carries the NewVar and VarRef tag bytes. Counting them as variables would
+        // shift the numbering and mark the wrong bit.
+        let poison = raw_sym(&[item_byte(Tag::NewVar), item_byte(Tag::VarRef(0))]);
+        let body = conj(&[rel("r", &[nv(), poison.clone()]), rel("s", &[vr(0), nv()])]);
+        let tpl = rel("out", &[vr(0)]);
+        assert_eq!(mask(&body, &[tpl]), 1 << 1);
+        // ... and in the template, where it would otherwise fake a read of variable 0.
+        let tpl_poison = rel("out", &[vr(1), poison]);
+        assert_eq!(mask(&body, &[tpl_poison]), 0);
+    }
+
+    #[test]
+    fn a_body_past_the_encodings_variable_cap_opts_out_entirely() {
+        // Rather than bounds-check every access, the walk stops at the cap and the body opts
+        // out. A zero mask is the unchanged enumeration, so that is the conservative direction.
+        // (Two conjuncts because an arity caps at 63 too.)
+        let low: Vec<Vec<u8>> = (0..34).map(|_| nv()).collect();
+        let high: Vec<Vec<u8>> = (0..34).map(|_| nv()).collect();
+        let body = conj(&[rel("r", &low), rel("s", &high)]);
+        assert_eq!(mask(&body, &[rel("out", &[vr(0)])]), 0);
+        // ... while a body at the cap still marks normally.
+        let at_cap: Vec<Vec<u8>> = (0..40).map(|_| nv()).collect();
+        let body = conj(&[rel("r", &at_cap)]);
+        let m = mask(&body, &[rel("out", &[vr(0)])]);
+        assert_eq!(m, ((1u64 << 40) - 1) & !1, "bits 1..=39, stopping at the one the template reads");
+    }
+
+    #[test]
+    fn a_body_with_no_variables_cuts_nothing() {
+        let body = conj(&[rel("r", &[sym("a")])]);
+        assert_eq!(mask(&body, &[rel("out", &[sym("b")])]), 0);
+    }
+}