artdag: Phase 7 consumes lib/maude mau/confluent? (no bespoke confluence checker)

The CID-stability check now calls mau/confluent? / mau/non-joinable-pairs from
lib/maude/confluence.sx (merged in) instead of re-implementing critical-pair
analysis inside lib/artdag. Picks up confluence.sx via the architecture merge.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

plans/artdag-on-sx.md

@@ -156,13 +156,18 @@ declaratively and prove it equivalent to the hand-written `optimize.sx`.
 - [ ] Equivalence: assert the maude-optimised DAG == `optimize.sx`'s output on
   the existing fixtures (same nodes, same content ids) — the rule set must cover
   at least the hand-written passes.
-- [ ] Confluence / CID-stability check: a syntactic critical-pair / local-
-  confluence checker over the optimisation `eq`s — different rewrite orders must
-  reach the same normal form, else the optimiser is CID-unstable. Full
-  AC-unification is OUT OF SCOPE; check syntactic overlaps + joinability and use
-  `mau/canon` as the joinability oracle for AC laws.
+- [ ] Confluence / CID-stability check: **consume `mau/confluent?` from
+  `lib/maude/confluence.sx`** — do NOT build your own checker. Assert the
+  optimisation rule module is confluent (`(mau/confluent? rules-module)` is
+  true) so different rewrite orders reach the same normal form and the optimised
+  pipeline's content id is stable. On failure, `mau/non-joinable-pairs` +
+  `mau/cp->str` name the offending critical pair (fix the rule set, e.g. add the
+  joining law — see the `f(a)=b,a=c` → add `f(c)=b` pattern). It is a syntactic
+  critical-pair checker (exact for free/constructor ops; AC overlaps under-
+  approximated but joined via canonical form) — that matches what this optimiser
+  needs. API also: `mau/critical-pairs`, `mau/joinable?`.
 - [ ] `lib/artdag/tests/maude-optimize.sx` — bridge round-trip, each law,
-  equivalence-with-`optimize.sx`, confluence of the rule set.
+  equivalence-with-`optimize.sx`, `(mau/confluent? rules-module)` holds.
 - [ ] (later) cost-directed choice among confluent-equivalent forms; (optional)
   miniKanren scheduling.