symbolic discharge: universals over infinite domains decided by intervals

3 files changed, 27 insertions, 13 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.
 
diff --git a/docs/virtual-machine-specification.org b/docs/virtual-machine-specification.org
index 828bc3c..f84bc84 100644
--- a/docs/virtual-machine-specification.org
+++ b/docs/virtual-machine-specification.org
@@ -135,9 +135,10 @@ without changing admitted semantics:
   one-sided comparisons; difference constraints between variables,
   arithmetic relations, and propagation through record structure
   are the next strengths;
-- symbolic discharge: algebraic evidence for universals over
-  infinite domains, and arithmetic decrease measures for recursion
-  that structural containment cannot see;
+- symbolic discharge beyond the interval fragment: algebraic
+  identities of relations (universals mentioning =Plus= and kin),
+  and arithmetic decrease measures for recursion that structural
+  containment cannot see;
 - Rocq certificates as admission evidence, and extraction of the
   lexicographic search itself (the containment core is already
   extracted);
diff --git a/docs/vm.org b/docs/vm.org
index 446cee2..a51b85a 100644
--- a/docs/vm.org
+++ b/docs/vm.org
@@ -96,10 +96,18 @@ open goals cannot happen.
 =Exists= lowers to a conjunction at loading, since query variables
 are existential already; its =variable:= is renamed apart so the
 scope cannot be forged. =ForAll= runs when its quantifier is
-decidable: every solution of the quantifier must satisfy the body. A
-universal over an infinite domain is a non total plan, rejected, as
-decision 10 requires. Variables that live only under a universal are
-not answer variables.
+decidable: every solution of the quantifier must satisfy the body.
+Variables that live only under a universal are not answer variables.
+
+A universal over an infinite domain is never enumerated. It gets one
+chance at symbolic discharge: when quantifier and body both read as
+kind and interval constraints over the quantified variable, the
+engine decides entailment algebraically. Every natural is at least
+zero: proven. Not every integer is: refuted, and the refutation is
+backed by a concrete counterexample. Every integer is a rational:
+proven, which is decision 12's subtype inclusion decided
+symbolically. A universal outside that fragment is a non total plan,
+rejected, as decision 10 requires.
 
 * Membership criteria as domains