From e92c8e00290bab8db328058c437b471c0f1671a4 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sun, 12 Jul 2026 09:59:59 -0300 Subject: algebraic identities of plus and times discharge symbolically --- docs/core-design-and-pipeline.org | 17 +++++++++-------- docs/vm.org | 7 +++++-- 2 files changed, 14 insertions(+), 10 deletions(-) (limited to 'docs') diff --git a/docs/core-design-and-pipeline.org b/docs/core-design-and-pipeline.org index c81b58a..eda5429 100644 --- a/docs/core-design-and-pipeline.org +++ b/docs/core-design-and-pipeline.org @@ -117,14 +117,15 @@ two of the ladder in decision 10: - 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. + domains decided by kind inclusion, interval entailment, and the + unit identities of the numeric relations, with refutations backed + by counterexamples. + +Not yet present: symbolic discharge beyond that fragment (richer +algebraic theories, 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. * What embedding means diff --git a/docs/vm.org b/docs/vm.org index a51b85a..d678acd 100644 --- a/docs/vm.org +++ b/docs/vm.org @@ -106,8 +106,11 @@ 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. +symbolically. The unit identities of the numeric relations discharge +too: =[Plus left: X right: 0 result: X]= holds over all integers by +the algebra of =Plus=, in the flat membership form of decision 14, +and fails over strings, which do not add. A universal outside that +fragment is a non total plan, rejected, as decision 10 requires. * Membership criteria as domains -- cgit v1.2.3