Sum over items, not over grounds

Intention

I want to include each payment in the sum once, regardless of how many grounds apply.

Two grounds for excluding one payment once produced an understated base; the witness below repeats the error on a 500 KZT payment.

Correct formFrozen execution sceneBoundary

Incorrect form and why it stays silent

Incorrect form

sum(collect all x: Money, p: Payment, g: Ground where excluded_by(p, g) and amount(p, x))

List keeps substitutions: a payment with two grounds appears twice. First derive a single excluded flag per payment, then sum the payments.

Correct form

Arxo Law

language "law.core" version "0.2";
package recipes.l.r06 version "0.1.0";
namespace "urn:recipe:l-calc:06";

entity Payment;
entity Ground;
relation amount(p: Payment, x: Money) { key(p); }
relation excluded_by(p: Payment, g: Ground);
relation excluded(p: Payment);
relation total(x: Money);
rule Excluded strict { for p: Payment; for g: Ground; when excluded_by(p, g); then excluded(p); }
rule Sum strict { when true; then total(sum(collect all x: Money, p: Payment where excluded(p) and amount(p, x))); }

Frozen execution scene

Facts and choice	Question	Answer
1. one payment with two grounds	truth(total(500 KZT))	TRUE_ONLY / COMPUTED
2. mistaken sum over grounds	sum(collect all x: Money, p: Payment, g: Ground where excluded_by(p, g) and amount(p, x))	1000 KZT / COMPUTED
3. two 500 payments, grounds do not multiply the sum	truth(total(1000 KZT))	TRUE_ONLY / COMPUTED

one payment on two grounds

Arxo Law

test "one payment on two grounds" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert amount(entity_ref("urn:recipe:l-calc:06:p"), 500 KZT); assert excluded_by(entity_ref("urn:recipe:l-calc:06:p"), entity_ref("urn:recipe:l-calc:06:g")); assert excluded_by(entity_ref("urn:recipe:l-calc:06:p"), entity_ref("urn:recipe:l-calc:06:h"));
    }
    evaluate truth(total(500 KZT));
    expect truth_status == TRUE_ONLY;
    expect evaluation_status == COMPUTED;

}

mistaken total by grounds

Arxo Law

test "mistaken total by grounds" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert amount(entity_ref("urn:recipe:l-calc:06:p"), 500 KZT); assert excluded_by(entity_ref("urn:recipe:l-calc:06:p"), entity_ref("urn:recipe:l-calc:06:g")); assert excluded_by(entity_ref("urn:recipe:l-calc:06:p"), entity_ref("urn:recipe:l-calc:06:h"));
    }
    evaluate sum(collect all x: Money, p: Payment, g: Ground where excluded_by(p, g) and amount(p, x));
    expect value == 1000 KZT;
    expect evaluation_status == COMPUTED;

}

two payments, grounds do not multiply

Arxo Law

test "two payments, grounds do not multiply" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert amount(entity_ref("urn:recipe:l-calc:06:p"), 500 KZT); assert excluded_by(entity_ref("urn:recipe:l-calc:06:p"), entity_ref("urn:recipe:l-calc:06:g")); assert excluded_by(entity_ref("urn:recipe:l-calc:06:p"), entity_ref("urn:recipe:l-calc:06:h")); assert amount(entity_ref("urn:recipe:l-calc:06:a"), 500 KZT); assert excluded_by(entity_ref("urn:recipe:l-calc:06:a"), entity_ref("urn:recipe:l-calc:06:g"));
    }
    evaluate truth(total(1000 KZT));
    expect truth_status == TRUE_ONLY;
    expect evaluation_status == COMPUTED;

}

Counterfactual

Mutation: x: Money, p: Payment where excluded(p) → x: Money where excluded(p); expected LDC-E1317. Additional counterfactuals are shown as separate table rows.

Boundary

A key does not fix the unit of count and does not prove journal completeness. Without payments sum is empty and yields EMPTY_AGGREGATE; zero needs a separate completeness ground.

Pitfall

Summing over grounds multiplies the payment by its number of grounds; sum over the derived per-payment flag instead.