# 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; 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 min 0; result: relation(subject, matter, option); excluded: cases { premises: list 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 - < /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.
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: ```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.