symbolic discharge: universals over infinite domains decided by intervals

1 files changed, 11 insertions, 6 deletions

diff --git a/docs/core-design-and-pipeline.org b/docs/core-design-and-pipeline.org
index 823a24e..c81b58a 100644
--- a/docs/core-design-and-pipeline.org
+++ b/docs/core-design-and-pipeline.org
@@ -111,13 +111,18 @@ two of the ladder in decision 10:
   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 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, and
-active constraint propagation over residue. Each arrives as a
+  instead of failing the plan;
+- interval propagation over residue: contradictions fail, finite
+  integer ranges enumerate;
+- symbolic discharge, first fragment: universals over infinite
+  domains decided by kind inclusion and interval entailment, with
+  refutations backed by counterexamples.
+
+Not yet present: symbolic discharge beyond the interval fragment
+(algebraic identities of relations, arithmetic decrease measures)
+and Rocq certificates as admission evidence. Each arrives as a
 strengthening of admission or planning; none changes the semantics
 of what is already admitted.