Markdown for LLMs
nb-17 — Numeric families and support boundaries
The source Markdown for this article. Copy it into your assistant or download it as a text file.
# nb-17 — Numeric families and support boundaries
*Northbridge course, math branch (needs beginner only:
[nb-01: First permit: facts, a rule and a question](/tutorials/northbridge/nb-01-first-permit/) → [nb-04: The permit fee](/tutorials/northbridge/nb-04-permit-fee/)).
All law is fictional; every resident, report, invoice and certificate
is synthetic and unofficial. No real municipal deployment or
legal-validity claims. Tool `law 0.1.0`, language version `0.2`,
semantics `law.core/0.2`, std `0.2.0` (from `law --version`, quoted
below).*
## Situation
Mira, the Northbridge permits clerk, receives two numbers she is
asked to certify. A footbridge inspection report states that a load
factor stays inside a proven square-root bound. A foreign contractor
submits an invoice in USD and asks the office to convert it to KZT at
the day rate, and a second contractor asks the office to solve a
tariff equation for him. The auditor's question is blunt: *which of
these numbers can our pinned machine prove, and which must it
refuse — and is each refusal a property of our build or of the
language itself?*
You will run the certified calls the pinned build does prove, then
watch it refuse the rest — each refusal naming the exact layer that
rejected it. The answer is never "the language cannot do this"; it
is always "this build, at this layer, for this version." Each new
term is introduced where it is first used.
## Prerequisites
[nb-01: First permit: facts, a rule and a question](/tutorials/northbridge/nb-01-first-permit/):
facts, strict rules, the four truth statuses (`TRUE_ONLY` means
established, `NEITHER` means established neither way), `law test`
as the way to check a claim.
[nb-04: The permit fee](/tutorials/northbridge/nb-04-permit-fee/): Money arithmetic and
rounding — the everyday numbers this article contrasts with the
gated families.
New here: certified bounds calls that execute only with an explicit
profile argument, names outside the `0.2` support list, and three
refusal codes at three different layers — each introduced where it
first appears below.
## Minimal example
Excerpts 1–2 are from `packs/examples/language-demo/math02/package.law`
(identifiers as written; relations, imports and unrelated rules cut).
Standalones A–C are complete probe files from
`packs/examples/language-demo/boundaries/evidence/snippets/`
(checked with `law engine check`; the `.law.txt` suffix only keeps
the package scanner from picking them up).
Excerpt 1 — self-determinism under one profile (lines 172–175).
A rule that compares a certified root bound with *itself*.
```law
rule SqrtSelf strict {
when sqrt_bounds(4, "p8/0.1") == sqrt_bounds(4, "p8/0.1");
then sqrt_self();
}
```
Look at the `when` line: the same certified call
(`sqrt_bounds(4, "p8/0.1")`) on both sides of `==`. The quoted
`"p8/0.1"` is the **cert profile** — the name of the exact proven
certificate the result carries. A **derivation** is the recorded
history of how a value was computed; the same derivation under the
same certificate is equal to itself, and this self-equality is what
`0.2` guarantees.
Excerpt 2 — the same call under two profiles (lines 186–189).
Only the profile name changes.
```law
rule CertCross strict {
when sin_bounds(0, "p8/0.1") == sin_bounds(0, "p16/0.1");
then cert_cross();
}
```
Look at what changed: only the right-hand profile, `"p8/0.1"` →
`"p16/0.1"`. The profile name is part of the derivation's history —
so a different certificate means a different derivation, and the
equality does not hold. The suite expects `NEITHER` for this rule.
Standalone A — full content of `sqrt02.law.txt`: exact root without
a certificate, in language `0.2`.
```law
language "law.core" version "0.2";
package probe version "0.1.0";
namespace "urn:probe";
function f(x: Rational) -> Rational = exact_sqrt(x);
```
Look at the last line: a bare `exact_sqrt` with no profile. The
name is simply not in the `0.2` support list, so the file is refused
with two codes, not executed. This tiny frozen probe is a **refusal
slice**: its only job is to show one boundary loudly. It is checked,
never executed.
Standalone B — full content of `solve02.law.txt`: a solver call,
same shape, same fate.
```law
language "law.core" version "0.2";
package probe version "0.1.0";
namespace "urn:probe";
function f(x: Rational) -> Rational = solve_linear(x, 1);
```
Look at the last line again: same four-line shape, different
forbidden name. Solver terms (`solve_linear`, the 0.6 family) and
the `Number` answer domain (0.4) live behind the same boundary as
exact algebra — refused in this profile.
Standalone C — full content of `v04.law.txt`: a newer language
version than the tool implements.
```law
language "law.core" version "0.4";
package probe version "0.1.0";
namespace "urn:probe";
relation r(x: Integer) kind empirical;
```
Look at the first line: the header declares language `0.4`. The
refusal happens at the version layer, before any name is even looked
up — the content below the header is never examined.
## Command and result
The tool, language and semantics versions are five separate facts,
and every refusal below names exactly one of them. The tool version
is what is installed; the language version is what the file header
declares; the exact semantics is the `law.core/0.2` revision plus the
std release; implementation support is the std v1-list of declared
names plus effect descriptors; the observed run is what the commands
below printed:
```sh
law --version
```
Observed:
```text
law 0.1.0
семантика: law.core/0.2
std для языка 0.2: 0.2.0
```
The Russian lines pin the semantics (`семантика: law.core/0.2`) and
the std release for language 0.2 (`std для языка 0.2: 0.2.0`). A
**numeric family** is a group of number-like types and functions that
are versioned and supported together — integers and rationals in one
family, certified real functions in another, solvers and conversions
in further ones. The executable side — every family `0.2`
supports — is green:
```sh
law test packs/examples/language-demo/math02
```
Observed (last lines; engine `law 0.1.0`):
```text
ok [demo.northbridge.math02] tests/math02.lawtest / unit conversion by value
ok [demo.northbridge.math02] tests/math02.lawtest / quantity returned into a unit
ok [demo.northbridge.math02] tests/math02.lawtest / unit exponent
итого: 42 проверено, 42 прошли, 0 не прошли, 0 не исполнены; код 0
```
All 42 answers matched their expectations (`итого: 42 проверено, 42
прошли, 0 не прошли, 0 не исполнены; код 0` — 42 checked, 42 passed,
0 failed, 0 unexecuted, exit code 0). The neighbouring boundaries
package is green too:
```sh
law test packs/examples/language-demo/boundaries
```
Observed: `итого: 21 проверено, 21 прошли, 0 не прошли, 0 не
исполнены; код 0` — 21 checked, 21 passed, 0 failed, 0 unexecuted,
exit code 0.
```text
итого: 21 проверено, 21 прошли, 0 не прошли, 0 не исполнены; код 0
```
Both suites passing means every supported call behaved as declared.
Now the refusals, each naming its layer. The version refusal first:
```sh
law engine check packs/examples/language-demo/boundaries/evidence/snippets/v04.law.txt
```
Observed: `error LDC-E1401: версия языка "0.4" не поддерживается`
("language version 0.4 is not supported"), followed by the migration
report ([§266.1](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/35-part-xxxiii-a-language-versioning.ru.md#2661-language-versions): `0.1 [withdrawn]`, `0.2 [supported]`, revisions
`0.2.1`–`0.2.4`). The machine refuses the *version*, not the content:
this build reads `0.2` and will not read `0.4` headers at all.
The exact-algebra refusal carries two codes at once:
```sh
law engine check packs/examples/language-demo/boundaries/evidence/snippets/sqrt02.law.txt
```
Observed, in full — two codes, hence two layers rejected the file:
```text
packs/examples/language-demo/boundaries/evidence/snippets/sqrt02.law.txt:4:10: error LDC-E2403: COMPUTABILITY_NOT_PROVED (LDC-E2403): function "f" не доказана как PURE_DETERMINISTIC: вызов "exact_sqrt" не имеет доступного effect descriptor (imported/unknown dependency) (§46/§47.5)
packs/examples/language-demo/boundaries/evidence/snippets/sqrt02.law.txt:4:39: error LDC-E2105: функция "exact_sqrt" не объявлена (ни в файле, ни в std v1-списке)
```
The first code (`LDC-E2403`) says the function is not proved
`PURE_DETERMINISTIC` — the call has no available effect descriptor.
The second (`LDC-E2105`) says the name is not declared, neither in
the file nor in the std v1-list. Support and semantics each said no.
The solver refusal is the identical pair for a different name:
```sh
law engine check packs/examples/language-demo/boundaries/evidence/snippets/solve02.law.txt
```
Observed: `error LDC-E2403 ... вызов "solve_linear" не имеет
доступного effect descriptor ...` ("the call has no available
effect descriptor") plus `error LDC-E2105: функция "solve_linear"
не объявлена (ни в файле, ни в std v1-списке)` ("the function is
not declared, neither in the file nor in the std v1-list").
`fx_convert`, `pi`, `temp_convert`, `angle_convert` and `ln2`
report the same pair (verified per snippet); a query used as a
term (`query02.law.txt`) reports `E2105` alone — one layer, not
two (see [nb-14: Why this answer and what would change it](/tutorials/northbridge/nb-14-why-this-answer/)).
## Why this construct
Mira's auditor question — which numbers can the pinned machine prove?
— is answered by knowing the usable surface without guessing.
Integers, Rationals, Decimals, Money, Quantities, date/time spans,
`HALF_UP` rounding, `unit_convert` with the pinned `units.si`, and
certified bounds calls with an explicit profile all execute — 42 of
42 in the suite above.
Read `"p8/0.1"` as a certificate identity, not a precision wish.
`SqrtSelf` (same derivation, same profile) is `TRUE_ONLY`; `SqrtX`
(`sqrt_bounds(4, "p8/0.1") == bounds_const(2, 1)`, lines 167–170 of
the package) is `NEITHER`. A foreign derivation is never equal,
however plausible its digits look.
Cross-profile equality fails to keep parallel certificates apart.
`CertCross` (`p8` vs `p16`) is `NEITHER` with `COMPUTED`: both sides
computed, and the comparison honestly reports inequality of
derivations. The mirror image — any profile equals itself — replays
with the `p32` probe in Changed condition below (`TRUE_ONLY`, 43 of
43).
Each refusal sits at its layer. `E2105` (not declared in the file or
the std v1-list) is an *implementation-support* fact; `E2403`
(computability not proved, no effect descriptor) is an *exact
semantics* fact. Both gates must pass, and the probes fail both.
`query02` fails only the first gate, which is why it carries one
code instead of two.
The version refusal separates the tool from the language. `E1401`
says tool `law 0.1.0` implements no `0.4` semantics; the attached
migration report names the supported branch (`0.2`, revisions
`0.2.1`–`0.2.4`). It never says `0.4` content is meaningless — only
that this build will not read it.
<details>
<summary>Why not hand-written digits or a bare exact call?</summary>
Hand-writing the digits (`bounds_const(2, 1)` where the root belongs)
looks equal and is not — the suite keeps `BoundsOk`/`SqrtX` at
`NEITHER` precisely to catch that substitution. Reading a bare
`exact_sqrt` where a certified call belongs is caught louder, at
check time.
</details>
The evidence is the 42/42 and 21/21 suites, the `TRUE_ONLY` /
`NEITHER` / `NEITHER` triple (`sqrt_self`, `sqrt_x`, `cert_cross`),
and the five quoted refusal outputs — each executed above, none
asserted in prose. What is not proven is that any certificate is
mathematically correct, or that `p16` is "better" than `p8`. The
machine proves which comparisons hold under which certificate;
choosing a profile for a real bridge report is engineering judgment,
and Northbridge's bridge is fiction.
## Changed condition
`SqrtSelf` derives `sqrt_self()` as `TRUE_ONLY` — the identical
call with the identical profile on both sides. Change exactly one
token, the right-hand profile `"p8/0.1"` → `"p16/0.1"`
(`CertCross`), and the same shape of question becomes `NEITHER`:
both bounds computed (`COMPUTED`), the equality of derivations
gone. Change the profile consistently on both sides instead and the
status returns to `TRUE_ONLY`. One name changed asymmetrically flips
the answer; changed symmetrically it changes nothing — because
equality here compares derivations, not digits.
Replay recipe (standalone scratch copy; the repo suite is untouched):
```sh
cp -r packs/examples/language-demo/math02 /tmp/nb17-p32
```
Append after `SqrtSelf` in `/tmp/nb17-p32/package.law`:
```law
relation sqrt_self32() kind institutional;
rule SqrtSelf32 strict {
when sqrt_bounds(4, "p32/0.1") == sqrt_bounds(4, "p32/0.1");
then sqrt_self32();
}
```
Add `/tmp/nb17-p32/tests/p32.lawtest`:
```law
language "law.core" version "0.2";
package demo.northbridge.math02 version "0.1.0";
namespace "urn:law:demo:northbridge:math02";
test "p32 self equals itself" {
given {
context { legal_time @2026-03-01; decision_time @2026-03-01T09:00:00Z; knowledge_time @2026-03-01T09:00:00Z; timezone "UTC"; }
}
evaluate truth(sqrt_self32());
expect truth_status == TRUE_ONLY;
}
```
Register `tests/p32.lawtest` in `/tmp/nb17-p32/law.toml` suites and run:
```sh
law test /tmp/nb17-p32
```
Observed: `p32 self equals itself` ok,
`43 проверено, 43 прошли, 0 не прошли` — 43 checked, 43 passed, 0
failed. The fresh profile behaves exactly like `p8`: equal to
itself, silent toward others.
## Typical mistake
The mistake is asserting a certified result against a hand-written
constant:
Excerpt — `SqrtX` from
`packs/examples/language-demo/math02/package.law` lines 167–170
(the rule is real; the mistake is the author's TRUE_ONLY expectation).
```law
rule SqrtX strict {
when sqrt_bounds(4, "p8/0.1") == bounds_const(2, 1);
then sqrt_x();
}
```
The author reads "root of four is two" and expects `TRUE_ONLY`.
The observed consequence (`bounds root: foreign derivation is
unequal`) is `truth_status == NEITHER`. The constant on the right
carries a different derivation from the certified call on the left,
so the comparison fails — determinism (`BoundsSame`, `SqrtSelf`,
`DivSelf`: identical expression against itself, all `TRUE_ONLY`)
is the only equality the bounds surface offers.
The fix: never compare a certified call with anything except the
textually identical call. If the digits must appear, recompute them
through the same call on both sides.
## Limits
Every status above holds for the verified profile only: tool
`law 0.1.0`, language `0.2`, semantics `law.core/0.2`, std
`0.2.0`. Newer tool builds, other language versions and other
std releases have their own support lists; re-run, do not
assume.
Refusals are profile facts. `E1401`/`E2105`/`E2403`
describe this build's version support, std v1-list and effect
descriptors. None states that `Number`, `Algebraic`,
`RealExpr`, solvers or conversions are inexpressible in
general — the audit records all three families as
`normative_boundary`.
Certificates pin identity, not truth. A `TRUE_ONLY` on
`sqrt_self()` certifies that one derivation equals itself, not
that the certificate's mathematics is right.
One observed extra boundary: a `query` declaration used as a
term is refused with `E2105` alone ([nb-14: Why this answer and what would change it](/tutorials/northbridge/nb-14-why-this-answer/)) — same code, one
layer, no computability complaint.
## Exercise
Without running the engine, predict, then check with the commands
above:
1. `sqrt_self()` versus `sqrt_x()`: which truth status each, and
what distinguishes the two comparisons?
2. `cert_cross()` (`p8` vs `p16`): which truth status, which
evaluation status, and what does that pair mean?
3. `law engine check` over `sqrt02.law.txt`: which two codes, in
which order, and which layer (version / support / semantics)
does each name?
4. `law engine check` over `v04.law.txt`: which code, and does it
claim anything about the `0.4` language in general?
5. `fx_convert` (`fx02.law.txt`) and `DoubleIt`-in-condition
(`query02.law.txt`): which codes each, and what would have to
change — and at which of the five version layers — before
either could execute?
Write down each prediction first; run the commands; explain any
miss in one sentence. Check your work against the
[full solution: self-equality, cross-profile silence and refusal layers](/tutorials/northbridge/solutions/nb-17-solutions/).
## Sources
- Source: `packs/examples/language-demo/math02/package.law`
(certified rules `SqrtX`, `SqrtSelf`, `CertAll`, `CertCross`,
rounding `RoundHalf`, unit rules `ConvOk`, `QBackOk`, `ExpoOk`)
- Tests: `packs/examples/language-demo/math02/tests/math02.lawtest`
(42 tests: spans, bounds, aggregates, derivation-sensitive
comparisons, determinism probes)
- Refusal slices:
`packs/examples/language-demo/boundaries/evidence/snippets/v04.law.txt`
(`E1401`), `sqrt02.law.txt`, `solve02.law.txt`, `fx02.law.txt`,
`pi02.law.txt`, `ln02.law.txt`, `temp02.law.txt`,
`angle02.law.txt` (`E2105 + E2403`), `query02.law.txt`
(`E2105` alone); frozen outputs `evidence/ev-*.txt`
- Audit: `packs/examples/language-demo/matrix-audit-P11.json`
(`types`: `Number`, `Algebraic`, `RealExpr` —
`normative_boundary`)
- Suite tour: `packs/examples/language-demo/README.md`
(math02 §, boundaries § with the full frozen-refusal table)
- Prerequisite: [nb-01: First permit: facts, a rule and a question](/tutorials/northbridge/nb-01-first-permit/),
[nb-04: The permit fee](/tutorials/northbridge/nb-04-permit-fee/); next: [nb-15: Quantities and dimensions](/tutorials/northbridge/nb-15-quantities/)
Three levels:
1. **Northbridge use** (this article): the clerk certifies only
what the pinned build proves — self-identical certified
bounds (`TRUE_ONLY`), honest silence on cross-profile and
foreign-derivation comparisons (`NEITHER`), and loud,
layer-named refusals for solvers, conversions and newer
versions — verified by the 42/42 plus 21/21 suites and the
quoted `E1401` / `E2105 + E2403` outputs above.
2. **Domain template:** whenever a regime gates numeric methods
by version, separate the five layers (tool, language, exact
semantics, implementation support, observed run); execute
only under explicit certificate profiles; compare certified
values solely with textually identical calls; freeze every
refusal as a replayable slice with its codes; never read a
profile refusal as a language-wide inability.
3. **Confirmed example elsewhere:** the same `E2105 + E2403`
pair fires for seven unrelated names (`exact_sqrt`,
`solve_linear`, `fx_convert`, `pi`, `ln2`, `temp_convert`,
`angle_convert`) and `E1401` for the `0.4` header — the
boundary machinery is uniform across families, per the
boundaries README table and the frozen `ev-*.txt` exhibits,
not a quirk of one square root.
4. **Confirmed external formalization (corpus):** VIN check digit
via Euclidean remainder (US, 49 CFR) — package `us.cfr.vin`,
`corpus/laws/us/vin/02-check-digit.law:282-287`:
`then vin_check_remainder(vin, total mod 11)` — the remainder is
taken of a whole total as `Integer mod Integer`
(`0 <= r < |b|` for any signs), never of an inexact magnitude
(`Decimal` has no remainder). A family boundary in live law:
this computation belongs to the Integer family and is refused
elsewhere. Evidence:
`docs/research/constructs/21-expressions-quantities/corpus-forms.en.md`
[§9](/tutorials/northbridge/nb-01-first-permit/#9-three-levels) (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.