Markdown for LLMs

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

The source Markdown for this article. Copy it into your assistant or download it as a text file.

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

*Northbridge course, advanced ([nb-13](/tutorials/northbridge/nb-13-expansions/) →
[nb-14](/tutorials/northbridge/nb-14-why-this-answer/) →
[nb-22](/tutorials/northbridge/nb-22-expansions-queries/)).
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](/tutorials/northbridge/nb-13-expansions/)
introduced the expansion; [nb-14: Why this answer and what would
change it](/tutorials/northbridge/nb-14-why-this-answer/) 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](/tutorials/northbridge/nb-01-first-permit/): facts, strict rules,
the four truth statuses, `law test`.
[nb-03: Exceptions and conflicting rules](/tutorials/northbridge/nb-03-exceptions/):
defeasible rules, priorities.
[nb-13: Repeatable norms without copying](/tutorials/northbridge/nb-13-expansions/):
expansion, params, expand, exports, identifiers, metadata.
[nb-14: Why this answer and what would change it](/tutorials/northbridge/nb-14-why-this-answer/):
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.

```law
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:

```law
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`).

```law
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.

```law
    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:

```law
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:

```law
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:

```law
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:

```law
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`:

```law
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:

```sh
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:

```text
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](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/24-part-xxiii-cases-snapshots-evaluation.ru.md#1684-пакет-дело-и-операция-ask-decision-0165)). First, the twelve-month
question:

```sh
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:

```sh
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:

```sh
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`):

```sh
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:

```sh
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:

```sh
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:

```sh
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:

```sh
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:

```sh
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:

```sh
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):

```sh
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:

```sh
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:

```sh
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:

```sh
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:

```sh
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.

<details>
<summary>Why not plain hand-written tests?</summary>

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

</details>

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:

```sh
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:

1. `some repeat_inquirer` versus `none`: which filling needs a record,
   and which status does the fee test report without one?
2. Which three proof steps would `explain` list for the surcharge, and
   why is the waiver defeater absent?
3. Two cost-1 candidates: how many solutions, what `cutoffCost`, and what
   does `--verify` report?
4. `law engine check` over each migration snippet: which code, and does
   the file still pass?
5. 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](/tutorials/northbridge/solutions/nb-22-solutions/).

## 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](/tutorials/northbridge/nb-01-first-permit/),
  [nb-03: Exceptions and conflicting rules](/tutorials/northbridge/nb-03-exceptions/),
  [nb-13: Repeatable norms without copying](/tutorials/northbridge/nb-13-expansions/),
  [nb-14: Why this answer and what would change it](/tutorials/northbridge/nb-14-why-this-answer/)

Three levels:

1. **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.
2. **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.
3. **Confirmed example elsewhere:** the templates package (8/8) and
   the queries package use the same shapes and machinery.
4. **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](/tutorials/northbridge/nb-01-first-permit/#2-prerequisites)
   (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.