Merge architecture: pick up lib/maude/confluence.sx (mau/confluent?)

plans/maude-on-sx.md

@@ -162,6 +162,19 @@ spike: it justifies a maude-driven optimiser in `lib/artdag` and the eventual
 affects matching/canon, NOT auto-reduction — write explicit identity eqs (or
 read off the canonical form) if you need `0 + N` to reduce in the term itself.
 
+**Confluence / critical-pair checking (lib/maude/confluence.sx, 12 tests):**
+`mau/confluent?` answers the plan's substrate question "can confluence be
+checked." Two-sided syntactic unification (`mau/u-unify`, with occurs check) →
+critical pairs from LHS overlaps (`mau/critical-pairs`) → joinability via
+`mau/ac-equal?` of the normal forms (`mau/non-joinable-pairs` gives the
+diagnostics, `mau/cp->str` renders `left <?> right`). Caught `f(a)=b, a=c` as
+non-confluent (`b <?> f(c)`); confirmed peano/idempotent/AC examples confluent.
+SCOPE: unification is SYNTACTIC — exact for free/constructor ops, an
+under-approximation for AC overlaps (full AC-unification is NP/infinitary, out
+of scope), but joinability uses the AC-canonical form so AC laws still join
+correctly. This is the CID-stability oracle for the artdag optimiser: an
+optimisation rule set is content-id-stable iff `mau/confluent?` holds.
+
 Pacing down to hardening. Possible niche future work: membership
 axioms (`mb`/`cmb`), critical-pair / confluence checking, meta-search, full
 mixfix (multi-`_` ops, juxtaposition `__`).