mutual recursion admitted under lexicographic measures

1 files changed, 8 insertions, 6 deletions

diff --git a/docs/core-design-and-pipeline.org b/docs/core-design-and-pipeline.org
index 9e085f8..823a24e 100644
--- a/docs/core-design-and-pipeline.org
+++ b/docs/core-design-and-pipeline.org
@@ -107,15 +107,17 @@ meaning; the =WORLD= functor is the seam it plugs into.
 What the implementation enforces today is rung one and part of rung
 two of the ladder in decision 10:
 
-- structural decrease on self recursive rules, with the witness
-  demanded ground at unfolding;
+- lexicographic structural decrease across call graph components,
+  with every measure position demanded ground at unfolding; self
+  recursion and mutual recursion are the same check;
 - bounded enumeration through =Between=;
-- decidable negation and universals only over decidable quantifiers.
+- decidable negation and universals only over decidable quantifiers;
+- residuation: open membership returns as residual constraints
+  instead of failing the plan.
 
 Not yet present: symbolic discharge (algebraic proof of universals
-over infinite domains), Rocq certificates as admission evidence,
-mutual recursion under a lexicographic measure, and a constraint
-store that residuates instead of rejecting. Each arrives as a
+over infinite domains), Rocq certificates as admission evidence, and
+active constraint propagation over residue. Each arrives as a
 strengthening of admission or planning; none changes the semantics
 of what is already admitted.