nb-22 — Expansions you can answer about, answers you can explain

← Course mapChapter 22 / 25 · Advanced II

Northbridge course, advanced (nb-13 → nb-14 → nb-22). All law is fictional; every desk, surcharge, waiver and billed month is synthetic and unofficial. No real municipal deployment or legal-validity claims. Engine law 0.1.0, semantics law.core/0.2.

1. Situation

The Northbridge inquiry desk handles walk-in questions all day. Its norms share shapes with different fillings: a repeat inquirer pays a callback fee, a first-timer gets only a notice, and an inspection held at an open desk draws a surcharge unless the case was waived. Writing each norm by hand would mean copying the same rule shape over and over — so the desk declares each shape once as an expansion and fills it in per case.

The desk must also answer for its answers. A visitor billed for twelve months asks: is that a big inquiry, and why? A borderline case at six months asks: what single record would flip the answer? The desk replies with a status, a because-list naming the exact rule that fired, and — for the borderline case — the cheapest flip with a replayable certificate.

nb-13: Repeatable norms without copying introduced the expansion; nb-14: Why this answer and what would change it introduced asking, explaining, properties and the what-if game. This article joins both in one desk: expansions explained through their generated rules, queries of both applicable kinds, one property, one finite counterfactual with all equi-minimal solutions, and rejection probes for two removed spellings.

2. Prerequisites

nb-01: First permit: facts, a rule and a question: facts, strict rules, the four truth statuses, law test. nb-03: Exceptions and conflicting rules: defeasible rules, priorities. nb-13: Repeatable norms without copying: expansion, params, expand, exports, identifiers, metadata. nb-14: Why this answer and what would change it: ask, explanation, property, counterfactual, replay.

Each combination below is explained where it first appears: applicable parameter classes, optional premises (some/none fillings), explanations of generated rules (the because-list naming a self/... identifier), applicable query kinds (Money, Integer), all equi-minimal solutions, and rejection probes for removed spellings.

3. Minimal example

All excerpts are from packs/examples/language-demo/inquiry/package.law (identifiers as written; the rest cut), except the last two — whole files.

Excerpt 1 — the callback template (lines 33–49). Repeat visitors and first-timers both get a callback response, but only the repeat case depends on a prior record. Watch the params block: a binder for the visitor, an option<...> premise for the possibly-absent cause, and two fixed-arity relations for the ground and the result.

expansion callback {
    params {
        subject: binder;
        cause: option<relation(subject)>;
        ground: relation(subject);
        result: relation(subject);
    }
    exports { applicability = self/applicable; }
    emit rule self/applicable strict {
        for subject;
        when ground(subject);
        if some cause as g { when g(subject); }
        then result(subject);
        scope from self; effective from self; labels from self; source from self;
    }
}

One idea: the if some cause as g line makes the extra premise conditional. When the instance binds none, the generated rule has no such premise at all.

Excerpt 2 — both fillings (lines 51–65). The repeat fee needs the repeat record; the first-timer notice needs nothing beyond the filing:

expand callback RepeatFee {
    label en unofficial "repeat inquiry draws a callback fee";
    bind subject = a: Applicant;
    cause = some repeat_inquirer;
    ground = inquiry_filed;
    result = callback_fee;
}

expand callback FirstNotice {
    label en unofficial "first inquiry draws only a notice";
    bind subject = a: Applicant;
    cause = none;
    ground = inquiry_filed;
    result = callback_notice;
}

One idea: none is a real filling, not an omission. The notice instance needs no cause at all and always fires on its ground.

Excerpt 3 — the inspection template head (lines 82–101). An inspection at an open desk draws a surcharge of a fixed kind, unless a listed exception applies. Watch the params block grow: a second binder, a value for the surcharge kind, a ground plus a list<...> of conditions, a result, and cases with non-empty premise lists (min 1).

expansion inspection {
    params {
        subject: binder;
        matter: binder;
        option: value;
        ground: relation(subject, matter);
        conditions: list<relation(subject, matter)> min 0;
        result: relation(subject, matter, option);
        excluded: cases { premises: list<relation(subject, matter)> min 1; };
    }
    exports { applicability = self/applicable; }
    emit rule self/applicable defeasible {
        for subject; for matter;
        when ground(subject, matter);
        for each p in conditions { when p(subject, matter); }
        then result(subject, matter, option);
        scope from self; effective from self; labels from self; source from self;
    }

One idea: min 0 versus min 1 is the contract. Conditions may be empty, but every exception case must list at least one premise.

Excerpt 4 — the exception loop (lines 102–116). Each listed case emits a defeater plus a priority: key(c) names both, and metadata comes from c with fallback to the site.

    for each c in excluded {
        emit rule self/excluded/key(c)/excludes defeasible {
            for subject; for matter;
            for each p in c.premises { when p(subject, matter); }
            then not result(subject, matter, option);
            scope from self; effective from self;
            labels from c prefix "[excludes] "; source from c fallback self;
        }
        emit priority self/excluded/key(c)/priority {
            prefer self/excluded/key(c)/excludes over self/applicable;
            reason explicit_exception;
            labels from c prefix "[priority] "; source from c fallback self;
        }
    }
}

One idea: the defeater has a stable address. The self/excluded/key(c)/excludes identifier lets explanations and priorities point at exactly the generated rule they mean.

Excerpt 5 — the inspection instance (lines 118–131). Ann is inspected at city hall while the desk is open; a waiver would lift the surcharge:

expand inspection DeskSurcharge {
    label en unofficial "inspection at an open desk draws a surcharge unless waived";
    bind subject = a: Applicant;
    bind matter = o: Office;
    option = Surcharge;
    ground = inspects_at;
    conditions = [desk_open];
    result = surcharged_for;
    effective [@2026-01-01, @2027-01-01);
    case excluded Waiver {
        label en unofficial "waiver exemption";
        premises = [waived_case];
    }
}

One idea: the instance binds every parameter class at once — binders, value, ground, conditions, result, window and the waiver case — so the generated rules are fully determined.

Excerpt 6 — the two query kinds and the what-if declaration (lines 139–149 and 174–179). The desk doubles the inquiry fee for one question, counts central residents for another, and declares the six-month what-if game up front:

query DoubleInquiryFee(months: Integer) -> Money {
    let base: Money = demo.northbridge.calculations::permit_fee(months);
    return 2 * base;
}

query InquiryCount() -> Integer {
    return count(collect all a: Applicant where demo.northbridge.vocabulary::resident(a) and demo.northbridge.vocabulary::lives_in(a, demo.northbridge.vocabulary::central));
}

counterfactual FlipToBigInquiry {
    target big_inquiry(6);
    mutable inquired_months;
    immutable city_tariff;
    cost EditInquiryCost;
}

One idea: target, moves and prices first, search second. The counterfactual block declares what may change (mutable), what must not (immutable) and what changes cost — before any search runs.

Excerpt 7 — the property (lines 99–102 of the test file packs/examples/language-demo/inquiry/tests/inquiry.lawtest). The doubled inquiry count must cover the plain count for every recorded value:

property InquiryDoubledCoversInquiry {
    forall m in collect v: Integer where inquired_months(v);
    expect double_inquired(m) >= m;
}

One idea: one statement, every matching fact. The forall ranges over all collected values; a single counterexample would fail the property.

Standalone 1 — the archived rejection probe inquiry/evidence/snippets/concept-migration.law.txt (not valid current syntax). concept is no longer accepted as a declaration:

language "law.core" version "0.2";
package probe version "0.1.0";
namespace "urn:probe";
entity Applicant;
concept resident(a: Applicant);

Standalone 2 — the archived rejection probe inquiry/evidence/snippets/except-migration.law.txt (not valid current syntax). The current spelling is unless:

language "law.core" version "0.2";
package probe version "0.1.0";
namespace "urn:probe";
entity Applicant;
relation filed(x: Applicant) kind empirical;
relation covered(x: Applicant) kind institutional;
relation blocked(x: Applicant) kind empirical;
rule CoverOld defeasible {
    for x: Applicant;
    when filed(x);
    except_when blocked(x);
    then covered(x);
}

4. Command and result

Run the inquiry suite from the repository root:

law test packs/examples/language-demo/inquiry

Observed result (engine law 0.1.0) — ten tests plus one property, all green. Every ok line means the answer matched its expectation; the Russian total reads “11 проверено, 11 прошли, 0 не прошли, 0 не исполнены; код 0”: 11 checked, 11 passed, 0 failed, 0 unexecuted, exit code 0:

law test demo.northbridge.inquiry: мир demo.northbridge.inquiry, demo.northbridge.calculations, demo.northbridge.vocabulary
  ok   [demo.northbridge.inquiry] tests/inquiry.lawtest / repeat inquiry draws the fee
  ok   [demo.northbridge.inquiry] tests/inquiry.lawtest / fee needs the repeat record
  ok   [demo.northbridge.inquiry] tests/inquiry.lawtest / first inquiry draws only a notice
  ok   [demo.northbridge.inquiry] tests/inquiry.lawtest / desk inspection draws the surcharge
  ok   [demo.northbridge.inquiry] tests/inquiry.lawtest / waiver lifts the surcharge
  ok   [demo.northbridge.inquiry] tests/inquiry.lawtest / rule reads the same function as the query
  ok   [demo.northbridge.inquiry] tests/inquiry.lawtest / query does not invent support
  ok   [demo.northbridge.inquiry] tests/inquiry.lawtest / count of central residents leads to the callback
  ok   [demo.northbridge.inquiry] tests/inquiry.lawtest / inquiry fee is non-negative
  ok   [demo.northbridge.inquiry] tests/inquiry.lawtest / negative inquiry fails the gate
  ok   [demo.northbridge.inquiry] tests/inquiry.lawtest / urn:law:demo:northbridge:inquiry#InquiryDoubledCoversInquiry
итого: 11 проверено, 11 прошли, 0 не прошли, 0 не исполнены; код 0

The last ok line is the property — it holds across all matching facts. The suite also proves the domain non-empty: the gate tests show the property ranges over real records, not a vacuous set.

The package also checks clean. The questions below run against the InquiryCity case (facts only, §168.4). First, the twelve-month question:

law engine check packs/examples/language-demo/inquiry
law ask packs/examples/language-demo/inquiry_cases --case InquiryCity --query 'evaluate truth(demo.northbridge.inquiry::big_inquiry(12));' --query-id big-inquiry-12 --format json

Observed: "truthStatus":"TRUE_ONLY" — twelve months at 10 EUR each clear the 50 EUR bar, so the desk answers that twelve billed months are a big inquiry. Now the borderline case:

law ask packs/examples/language-demo/inquiry_cases --case InquiryCity --query 'evaluate truth(demo.northbridge.inquiry::big_inquiry(6));' --query-id big-inquiry-6 --format text

Observed: Не установлено ни что «big_inquiry» (m: 6), ни обратное — “it is established neither that big_inquiry holds nor the reverse”. That is NEITHER, with no derivation steps: six months conclude nothing either way. The desk cannot call it big — but it has not shown it small.

Explanations read saved proof graphs, so save each answer (--out) first and then explain it. Start with Ann’s surcharge:

law ask packs/examples/language-demo/inquiry_cases --case InquiryCity --query 'evaluate truth(demo.northbridge.inquiry::surcharged_for(entity_ref("urn:demo:northbridge:ann"), entity_ref("urn:demo:northbridge:city-hall"), demo.northbridge.inquiry::Surcharge));' --query-id surcharge-ann --format json --out /tmp/nb22-ask-surcharge
law engine explain /tmp/nb22-ask-surcharge --json

Observed: "conclusion":"surcharged_for(ann, city-hall, surcharge): TRUE_ONLY" with "because":["urn:proof:apply:DeskSurcharge/applicable:...", "urn:proof:assert:...#insp","urn:proof:assert:...#open"]. Three steps: the generated rule DeskSurcharge/applicable, the inspection record (#insp) and the open-desk record (#open). The first step names the generated rule — expansions explain through their instances, not through the template. The plain rule explains the same way (BigInquiry plus i12):

law ask packs/examples/language-demo/inquiry_cases --case InquiryCity --query 'evaluate truth(demo.northbridge.inquiry::big_inquiry(6));' --query-id big-inquiry-6 --format json --out /tmp/nb22-ask6
law engine explain /tmp/nb22-ask6 --json

Observed: "conclusion":"big_inquiry(6): NEITHER" with "because":[]. Nothing fired, so there is nothing to list — an empty because-list is what NEITHER looks like under explanation.

The what-if runs against the frozen exhibits in packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/. Ask what single record would flip the six-month case:

law engine counterfactual --program packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-world.json --case packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-case.json --input packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-input.json

Observed: "status":"FOUND", "solverProfile":"law.solver.finite-enumeration/0.1", one solution — ...#add-i6 at "cost":"1", "cutoffCost":"1", one candidate checked. The cheapest flip is adding the six-month record at cost 1, and the cutoff of 1 certifies that nothing cheaper exists. With two equal-cost candidates the solver admits the tie instead of picking silently:

law engine counterfactual --program packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-world.json --case packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-case.json --input packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-input-two.json

Observed: "status":"FOUND" with both solutions, each at cost 1, "cutoffCost":"1", two candidates checked. Both cheapest flips are listed; the cutoff still certifies minimality. The desk ships the flip with a replay certificate — check it:

law engine counterfactual --program packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-world.json --case packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-case.json --input packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-input.json --verify packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-cf-result.json

Observed: {"kind":"counterfactual-verification","result":"urn:law:demo:northbridge:inquiry#FlipInquiryInput01/result","valid":true}. The flip replays to its certificate: the answer can be trusted without re-running the search.

A certificate pins the exact program it was computed against. programHash is the semantic hash of the linked world IR — directly observable, and equal to the value pinned in both nb-input.json and nb-cf-result.json. See it for yourself:

law engine semhash packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-world.json

Observed: sha256:cfe2fcb840dc20acc62c87636904558c9cb4066d37de132863db1c2478ec0409, exit 0. It is not the file’s byte hash. Re-serialize the world with different whitespace and the hash stands still:

mkdir -p /tmp/nb22-stale
python3 - <<'EOF'
import json
w = json.load(open('packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-world.json'))
json.dump(w, open('/tmp/nb22-stale/world-ws.json', 'w'), indent=1, ensure_ascii=False)
EOF
law engine semhash /tmp/nb22-stale/world-ws.json

Observed: still sha256:cfe2fcb8…, exit 0 — canonicalization makes byte layout irrelevant. Same for a metadata-only annotation:

mkdir -p /tmp/nb22-stale
python3 - <<'EOF'
import json
w = json.load(open('packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-world.json'))
w['metadata'] = {'note': 'stale-cert probe'}
json.dump(w, open('/tmp/nb22-stale/world-meta.json', 'w'), ensure_ascii=False)
EOF
law engine semhash /tmp/nb22-stale/world-meta.json

Observed: still sha256:cfe2fcb8…, exit 0 — metadata sits outside the semantic preimage. The minimal change that really moves the hash is one Money literal in the BigInquiry rule node (50 EUR → 51 EUR, the >= 50 EUR line of the inquiry world):

mkdir -p /tmp/nb22-stale
python3 - <<'EOF'
import json
w = json.load(open('packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-world.json'))
n = [x for x in w['nodes'] if x.get('id') == 'urn:law:demo:northbridge:inquiry#BigInquiry'][0]
n['body']['items'][1]['right']['value'] = '51'
json.dump(w, open('/tmp/nb22-stale/world-threshold.json', 'w'), ensure_ascii=False)
EOF
law engine semhash /tmp/nb22-stale/world-threshold.json

Observed: sha256:8b4127d767a8cd3fb715203d311e58f2c704c30ab1cd9d59868a6bd9a0f00bbf, exit 0. One literal moved the hash: the program is semantically a different world now. Re-verifying the old certificate against the changed program is refused before any reasoning, with both hashes named:

mkdir -p /tmp/nb22-stale
python3 - <<'EOF'
import json
w = json.load(open('packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-world.json'))
n = [x for x in w['nodes'] if x.get('id') == 'urn:law:demo:northbridge:inquiry#BigInquiry'][0]
n['body']['items'][1]['right']['value'] = '51'
json.dump(w, open('/tmp/nb22-stale/world-threshold.json', 'w'), ensure_ascii=False)
EOF
law engine counterfactual --program /tmp/nb22-stale/world-threshold.json --case packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-case.json --input packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-input.json --verify packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-cf-result.json

Observed (stdout, stderr empty, exit 1): {"error":{"code":"COUNTERFACTUAL_PROGRAM_HASH_MISMATCH","message":"counterfactual input programHash is sha256:cfe2fcb840dc20acc62c87636904558c9cb4066d37de132863db1c2478ec0409, actual is sha256:8b4127d767a8cd3fb715203d311e58f2c704c30ab1cd9d59868a6bd9a0f00bbf"}}.

That refusal is only the first of two layers. Renew the input envelope for the new program — re-pin programHash, re-seal contentHash via law engine canon (a recipe that reproduces the frozen 8133f6f0… envelope hash exactly, so it is trusted for the new one) — but present the old result, and the replay layer refuses instead:

mkdir -p /tmp/nb22-stale
python3 - <<'EOF'
import json
w = json.load(open('packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-world.json'))
n = [x for x in w['nodes'] if x.get('id') == 'urn:law:demo:northbridge:inquiry#BigInquiry'][0]
n['body']['items'][1]['right']['value'] = '51'
json.dump(w, open('/tmp/nb22-stale/world-threshold.json', 'w'), ensure_ascii=False)
inp = json.load(open('packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-input.json'))
inp['programHash'] = 'sha256:8b4127d767a8cd3fb715203d311e58f2c704c30ab1cd9d59868a6bd9a0f00bbf'
json.dump({k: v for k, v in inp.items() if k != 'contentHash'}, open('/tmp/nb22-stale/input-new-nohash.json', 'w'), ensure_ascii=False)
json.dump(inp, open('/tmp/nb22-stale/input-new-tmp.json', 'w'), ensure_ascii=False)
EOF
CH=$(law engine canon /tmp/nb22-stale/input-new-nohash.json | sha256sum | cut -d' ' -f1)
python3 - <<EOF
import json
inp = json.load(open('/tmp/nb22-stale/input-new-tmp.json'))
inp['contentHash'] = 'sha256:$CH'
json.dump(inp, open('/tmp/nb22-stale/input-new.json', 'w'), indent=1, ensure_ascii=False)
EOF
law engine counterfactual --program /tmp/nb22-stale/world-threshold.json --case packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-case.json --input /tmp/nb22-stale/input-new.json --verify packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-cf-result.json

Observed (exit 1): {"error":{"code":"COUNTERFACTUAL_CERTIFICATE_INVALID","message":"counterfactual result does not replay to the claimed canonical certificate"}}. Pin check first, canonical replay comparison second: a certificate cannot be accepted piecemeal, and it cannot silently survive a program change even when the outcome is the same.

The fix is mechanical — re-obtain the certificate against the changed program with stock tools only. Solve afresh, then verify the fresh result:

mkdir -p /tmp/nb22-stale
python3 - <<'EOF'
import json
w = json.load(open('packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-world.json'))
n = [x for x in w['nodes'] if x.get('id') == 'urn:law:demo:northbridge:inquiry#BigInquiry'][0]
n['body']['items'][1]['right']['value'] = '51'
json.dump(w, open('/tmp/nb22-stale/world-threshold.json', 'w'), ensure_ascii=False)
inp = json.load(open('packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-input.json'))
inp['programHash'] = 'sha256:8b4127d767a8cd3fb715203d311e58f2c704c30ab1cd9d59868a6bd9a0f00bbf'
json.dump({k: v for k, v in inp.items() if k != 'contentHash'}, open('/tmp/nb22-stale/input-new-nohash.json', 'w'), ensure_ascii=False)
json.dump(inp, open('/tmp/nb22-stale/input-new-tmp.json', 'w'), ensure_ascii=False)
EOF
CH=$(law engine canon /tmp/nb22-stale/input-new-nohash.json | sha256sum | cut -d' ' -f1)
python3 - <<EOF
import json
inp = json.load(open('/tmp/nb22-stale/input-new-tmp.json'))
inp['contentHash'] = 'sha256:$CH'
json.dump(inp, open('/tmp/nb22-stale/input-new.json', 'w'), indent=1, ensure_ascii=False)
EOF
law engine counterfactual --program /tmp/nb22-stale/world-threshold.json --case packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-case.json --input /tmp/nb22-stale/input-new.json > /tmp/nb22-stale/result-new.json
law engine counterfactual --program /tmp/nb22-stale/world-threshold.json --case packs/examples/language-demo/inquiry/counterfactual/inquiry-flip/nb-case.json --input /tmp/nb22-stale/input-new.json --verify /tmp/nb22-stale/result-new.json

Observed: solve reports "status":"FOUND", solution ...#add-i6 at cost 1 (new contentHash sha256:9e74d3f3…); --verify reports "valid":true, exit 0. Same verdict, new hashes, fresh certificate — old certificates stay invalid by design. The stale program now has a certificate of its own, and the two worlds can no longer share paperwork.

Finally, the archived source files serve as rejection probes for the two removed spellings:

law engine check packs/examples/language-demo/inquiry/evidence/snippets/concept-migration.law.txt
law engine check packs/examples/language-demo/inquiry/evidence/snippets/except-migration.law.txt

The warning and check OK outputs recorded for engine law 0.1.0 are historical. The removed spellings are rejected by the current compiler and must not be used in new packages; the probes remain only as evidence of the former migration phase. Neither file may serve as a template for new norms.

5. Why this construct

The desk declares each norm shape once. Applicable parameter classes say in one params block what an instance supplies: binders, fixed-arity relations, value, integer/window, list, cases, option. The inspection instance binds every class at once and the suite stays 11/11.

Optional premises let a rule fire on a record when it exists and without one when none is bound. The fee needs its repeat record (without it, NEITHER); the notice always fires on its ground alone.

Exports and identifiers address generated rules from outside. exports publishes self/applicable; key(c) addresses each defeater and priority. The surcharge explanation names DeskSurcharge/applicable to prove it.

Metadata carries scope, dates, labels and sources from the site (and per case) into every generated node. The 2026 window bounds the surcharge tests; the waiver case carries its [excludes] prefix.

Applicable query kinds compute Money and Integer values once instead of copying arithmetic into rules. Both reader rules derive through the same permit_fee (12 → TRUE_ONLY).

The property holds one claim across all matching facts — the eleventh ok line — while the gate tests prove the domain non-empty. The finite counterfactual names the cheapest flip with a price tag: add-i6 at cost 1 with cutoffCost 1. Equally-minimal solutions admit ties honestly: both cost-1 solutions listed, cutoffCost 1, never a silent pick.

The replay certificate lets the desk trust the flip without re-running the search: --verify reports valid:true on pinned hashes. Migration warnings keep old spellings loud: E1328 on both snippets, yet check OK and no norm executes.

Why not plain hand-written tests?

Hand-written tests assert conclusions, but they never prove minimality, list ties, or explain generated rules by identifier — cutoffCost plus the because-list do.

The proof is the suite, the asks, the explanations, the FOUND pair, the replay and both warnings: each executed above, none asserted in prose.

What is not proven: that six months should be big, that cost 1 is fair, or that the waiver is wise. The rest is fictional data.

6. Changed condition

File the waiver and the surcharge flips. inspects_at plus desk_open with no waiver gives TRUE_ONLY through DeskSurcharge/applicable; add the single waived_case fact and the same question is FALSE_ONLY through DeskSurcharge/excluded/Waiver/excludes winning by priority. One added assertion, two statuses — because the defeater fires only on its premise, and the priority prefers it over the base rule.

The six-month question is the same logic as a what-if: NEITHER today, TRUE_ONLY after adding inquired_months(6).

7. Typical mistake

The mistake is calling the query declaration as if it were a question — asking law ask to evaluate the query itself:

law ask packs/examples/language-demo/inquiry_cases --case InquiryCity --query 'evaluate demo.northbridge.inquiry::DoubleInquiryFee(12);' --query-id try-query-call --format text

Observed: {"error":{"code":"LDC-E1105","message":"... DoubleInquiryFee: символ не экспортирован пакетом ..."}} — “the symbol is not exported by the package”. A query is a declaration, not a relation and not a term: not askable, not usable in rule conditions (LDC-E2105), not cross-package addressable.

The fix is to ask through a reader rule instead. The computation inside the query runs only through reader rules like BigInquiry — fee(...) is the function, DoubleInquiryFee is the query, and the query is never askable through truth(...).

8. Limits

Expansions generate; they do not reason. A missing key(c) would collapse two defeaters into one address, with no error to warn you.

Queries invent no support. One recorded month yields NEITHER for the big-inquiry question, never FALSE_ONLY: the machine concludes nothing either way rather than establishing the negation.

The boundaries are profile facts. LDC-E1105/LDC-E2105, the property-expect E1105/E2403 restrictions, the E1328 warnings, and the solver profile describe this implementation (law 0.1.0, law.core/0.2), never the language in general.

Finite search needs a finite game. The solver checks the listed candidates; it never invents new ones.

Certificates pin the semantic program, not its bytes. --verify refuses a stale programHash before any reasoning — but whitespace and metadata never move that hash. Only a real program change does, and one Money literal suffices. Old certificates stay invalid after renewal by design.

The observed refusal stands: calling a query from law ask is LDC-E1105.

9. Exercise

Predict each answer without running the engine, then check with the commands above:

some repeat_inquirer versus none: which filling needs a record, and which status does the fee test report without one?
Which three proof steps would explain list for the surcharge, and why is the waiver defeater absent?
Two cost-1 candidates: how many solutions, what cutoffCost, and what does --verify report?
law engine check over each migration snippet: which code, and does the file still pass?
Three world edits — re-indent the JSON, add a top-level metadata note, change the BigInquiry 50 to 51: predict which move programHash, then run the three semhash commands. Then predict the stale --verify diagnostic code and exit code before running it.

Write each prediction first, run the commands, and explain any miss in one sentence. Checkable solution: full solution with checkable answers.

10. Sources

Source: packs/examples/language-demo/inquiry/package.law (both expansions, both queries, the reader rules, the counterfactual)
Tests: packs/examples/language-demo/inquiry/tests/inquiry.lawtest
Case and exhibits: inquiry_cases/ (InquiryCity), inquiry/counterfactual/inquiry-flip/, inquiry/evidence/snippets/
Suite tour: packs/examples/language-demo/README.md
Language reference: docs/language/09-advanced-cheat-sheet.law.md, docs/language/06-testing-a-package.law.md
Prerequisite: nb-01: First permit: facts, a rule and a question, nb-03: Exceptions and conflicting rules, nb-13: Repeatable norms without copying, nb-14: Why this answer and what would change it

Three levels:

Northbridge use (this article): one desk writes each norm shape once, answers with status plus because-list (including through generated rules), guarantees a doubling property, quotes the cheapest flip with a replay certificate, lists every tied flip, and preserves the former spelling probes as rejection cases — verified by the suite, the asks, the explanations, the FOUND pair and the replay above.
Domain template: declare each shape once; publish generated rules through exports and stable identifiers; explain from the proof graph; state universal claims as properties; declare what-ifs with target, mutables and cost model, and ship every flip with its replay check. Never call a query where a relation is expected; never write a rejected legacy probe as a norm.
Confirmed example elsewhere: the templates package (8/8) and the queries package use the same shapes and machinery.
Confirmed external formalization (corpus): pledge successor duties (Civil Code of Kazakhstan, art. 323) — package kz.corpus.civilcode, corpus/laws/kz/codes/civil-code/tests/323-art323-successor-bears-duties-by-default.lawtest:10-13: the canonical truth expectation triple (result_kind, truth_status, evaluation_status — all three axes) behind evaluate truth(successor_bears_all_pledgor_duties(...)), the same triple the art. 192/160/163 scenarios repeat. Evidence: docs/research/constructs/24-queries/corpus-forms.en.md §2 (rated exemplary). Limit of verification: presence of the named construct at the cited lines only, confirmed by direct file read; no claim about deployment, runtime behaviour, or legal correctness.

Documentation for Arxo. Writings — blog.arxo.io.

Anonymous visit counts on stats.arxo.io, no cookies.