Markdown for LLMs
nb-23 — Numbers and the standard library: every figure the 0.2 machine proves
The source Markdown for this article. Copy it into your assistant or download it as a text file.
# nb-23 — Numbers and the standard library: every figure the 0.2 machine proves
All law in this series is fictional; every meter, tariff, bill and
calendar 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).
## 1. Situation
Mira, the Northbridge water clerk, closes the March billing. Three
metered tanks hold 12, 9 and 15 cubic metres. A 2,500-litre rooftop
tank trips the 2,000-litre inspection threshold, and a 900-litre one
does not. A 2 km pipe run converts to 2,000 metres. The quarterly
bill of 1,410 KZT divides by three months into exactly 470 KZT,
while 1,000 KZT divided by three refuses loudly instead of rounding
quietly. A 2 March meter reading plus ten calendar days falls due on
12 March, and three working days later is 5 March.
Her auditor asks one question per number: *which of these did the
pinned machine prove, which did it refuse — and is each refusal a
property of our build or of the language itself?* This article
answers with one green suite plus pinned refusal reproducers.
Three ideas run through the answers. Number-like types ship in
**numeric families** — exact rationals in one family, certified
bounds in another, solvers and currency conversion in further ones —
each versioned and supported together. Operators follow a **kind
discipline**: each one names its operand kinds explicitly, so `Money
/ Decimal` is exact or loud while `Money / Integer` is rejected at
check time. And certified rounding faces **certificate sufficiency**:
does this interval sit inside a single rounding cell, or must the
machine refuse to guess? Truth statuses work as in
[nb-01: First permit: facts, a rule and a question](/tutorials/northbridge/nb-01-first-permit/) (`TRUE_ONLY` =
established, `NEITHER` = established neither way).
## 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` as the way to check a claim.
[nb-04: The permit fee](/tutorials/northbridge/nb-04-permit-fee/): `Money` arithmetic and
`HALF_UP` rounding — the everyday numbers this article completes.
[nb-15: Quantities and dimensions](/tutorials/northbridge/nb-15-quantities/): `Quantity`,
`Magnitude`, `units.si`, explicit conversion.
[nb-16: Exact computation and proven bounds](/tutorials/northbridge/nb-16-exact-bounds/):
exact rationals and derivation-carrying `Bounds`.
[nb-17: Numeric families and support boundaries](/tutorials/northbridge/nb-17-numeric-families/):
certified profiles and the version boundary — this article turns its
map into one green suite plus pinned refusal reproducers.
Each new function is explained where it first appears: `abs`, `pow`,
`average` with its precision policy, `div_round` over `Money`,
`percent`, `text_matches` as a conjunct, `add_business_days` /
`add_calendar_period` / `add_legal_term` with their calendar, the
monotone `Bounds` lift, the `math::` and `bounds::` short spellings,
and `rounds_to` with its three arms.
## 3. Minimal example
Excerpts are from `packs/examples/language-demo/numerics/package.law`
(identifiers as written; unrelated rules cut). Standalones are complete
probe files: save each pair and run the section 4 command against it.
Excerpt 1 — exact kinds stay apart (lines 52–71). Mira's billing
divides meter readings three ways. Watch the return types: three
divisions, three result kinds, no silent conversion.
```law
pure function half7() -> Rational = 7 / 2;
pure function exact_half() -> Decimal = 7.0 / 2.0;
pure function third() -> Rational = 10.0 / 3.0;
```
One idea: `7 / 2` is `Rational`, `7.0 / 2.0` is `Decimal` (its
denominator is 10-smooth), and `10.0 / 3.0` is `Rational` again —
the kind is computed from the operands, never wished by the author.
Excerpt 2 — money divides exactly or loudly (lines 84–95). The
quarterly bill splits three ways; a thousand KZT does not split at
all. Watch the divisor kind in both lines:
```law
pure function monthly() -> Money = 1410 KZT / 3.0;
pure function baddiv() -> Money = 1000 KZT / 3.0;
```
One idea: the divisor is `Decimal`, never `Integer`. `1410 KZT /
3` with an integer divisor is rejected at check time (`LDC-E2108`),
and the inexact quotient is a coded `INEXACT_DIVISION`, never a
quietly rounded amount.
Standalone A — full content of `probe.law`: the average that refuses
to guess over integers. Mira's three tank readings average to
exactly twelve — yet this rule fires nothing:
```law
language "law.core" version "0.2";
package probe version "0.1.0";
namespace "urn:probe";
relation reading(k: Integer) kind empirical;
relation avg_silent() kind institutional;
rule AvgSilent strict {
when average(collect all x: Integer where reading(x)) == 12;
then avg_silent();
}
```
One idea: `average` over `Integer` has no rounding policy to
apply, so the rule never fires. The same call over `Money` (with
`2, "HALF_UP"`) or over `Decimal` does fire — the kind decides.
Standalone B — full content of `probe.lawtest` for Standalone A
(header plus one test, complete as shown). The three readings are
asserted, and the test expects silence:
```law
language "law.core" version "0.2";
package probe version "0.1.0";
namespace "urn:probe";
test "average over integers stays silent" {
given {
context { legal_time @2026-03-02; decision_time @2026-03-02T09:00:00Z; knowledge_time @2026-03-02T09:00:00Z; timezone "UTC"; }
assert "r12": reading(12) { origin case_input; }
assert "r9": reading(9) { origin case_input; }
assert "r15": reading(15) { origin case_input; }
}
evaluate truth(avg_silent());
expect truth_status == NEITHER;
}
```
One idea: silence here is specified behaviour, not missing data.
Compare section 6, where the same readings feed `sum`, `min`, `max`
and `count` — and every one of those fires.
The suite's real counterparts live in
[numerics/package.law](https://github.com/arxohq/law/blob/master/packs/examples/language-demo/numerics/package.law)
(`AvgSilent`, `AvgBill` over `Money`, `AvgSample` over `Decimal`) and
[tests/numerics.lawtest](https://github.com/arxohq/law/blob/master/packs/examples/language-demo/numerics/tests/numerics.lawtest).
The calendar, policy and source the date terms need are lines 14–49
of the same package file; the refusal reproducers are
[evidence/snippets/](https://github.com/arxohq/law/blob/master/packs/examples/language-demo/numerics/evidence/snippets/).
## 4. Command and result
Pin the machine first: five facts — tool, language, semantics,
std, binary. Run from the repository root:
```sh
law --version
```
Observed:
```text
law 0.1.0
семантика: law.core/0.2
std для языка 0.2: 0.2.0
хэш бинаря: sha256:78dea06ce928547e87bd9875a2556cc663def37cbb78c8b04aa0da57839c95d7
```
The Russian lines name the semantics (`семантика: law.core/0.2`),
the std version for language 0.2 (`std для языка 0.2: 0.2.0`) and the
binary hash (`хэш бинаря`). These are separate facts: a newer tool
could keep the language version and still change what executes.
Now the whole executable surface in one run:
```sh
law test packs/examples/language-demo/numerics
```
Observed (last lines; engine `law 0.1.0`):
```text
ok [demo.northbridge.numerics] tests/numerics.lawtest / certified root rounds to three
ok [demo.northbridge.numerics] tests/numerics.lawtest / formula agrees on three
ok [demo.northbridge.numerics] tests/numerics.lawtest / wrong cell stays silent
ok [demo.northbridge.numerics] tests/numerics.lawtest / wide interval is loud
итого: 67 проверено, 67 прошли, 0 не прошли, 0 не исполнены; код 0
```
All 67 pass — the total reads "67 проверено, 67 прошли, 0 не
прошли, 0 не исполнены; код 0": 67 checked, 67 passed, 0 failed, 0
unexecuted, exit code 0. The last lines show the sufficiency
verdicts: the certified root publishes its cell, the wrong cell
stays silent, and the wide interval is loud.
The package checks clean and its imports are canonical:
```sh
law engine check packs/examples/language-demo/numerics
law fix imports packs/examples/language-demo/numerics
```
Observed: `check OK: packs/examples/language-demo/numerics` and
`блоки 'use self' канонические` — the `use self` blocks are
canonical. The package compiles and its imports need no repair.
Next, the standalone average probe from section 3. Save Standalones
A and B as `/tmp/nb23-probe/probe.law` and
`/tmp/nb23-probe/probe.lawtest`, then run:
```sh
law engine test /tmp/nb23-probe/probe.lawtest --program /tmp/nb23-probe/probe.law
```
Observed: `test PASS: average over integers stays silent`. The
pass means the rule stayed silent exactly as the test expects — the
machine refused the quiet integer mean.
One refusal pin, for the record — exact currency conversion.
Mira cannot convert bills at an exact rate in this build:
```sh
law engine check packs/examples/language-demo/numerics/evidence/snippets/fx02.law.txt
```
Observed, in full:
```text
packs/examples/language-demo/numerics/evidence/snippets/fx02.law.txt:7:10: error LDC-E2403: COMPUTABILITY_NOT_PROVED (LDC-E2403): function "f" не доказана как PURE_DETERMINISTIC: вызов "fx_convert" не имеет доступного effect descriptor (imported/unknown dependency) (§46/§47.5)
packs/examples/language-demo/numerics/evidence/snippets/fx02.law.txt:7:39: error LDC-E2105: функция "fx_convert" не объявлена (ни в файле, ни в std v1-списке)
```
All ten snippets refuse the same two-layer way (terms) or with
`LDC-E2101` (the `Number`, `Algebraic`, `RealExpr` types); each file
says so in its header comment. Two layers, both static — nothing
executes. `LDC-E2105` says the name is declared neither in the file
nor in the std v1-list, the executed 0.2 slice. `LDC-E2403` says
that without an effect descriptor for the callee, the enclosing
function cannot be proved `PURE_DETERMINISTIC` ([§46](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#46-functions)/[§47.5](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#475-computability-classification)).
Two pins below, one per profile family, in full — first the
RealExpr constant `ln2()` (profile 0.5, DECISION-0438 project).
Tool `law 0.1.0`, semantics `law.core/0.2`, std `0.2.0`, same
binary as above.
Standalone C — full content of
`boundaries/evidence/snippets/ln02.law.txt`: the `ln2` probe.
The `Rational` return type isolates the *term* refusal from the
separate `RealExpr`-type refusal below:
```law
language "law.core" version "0.2";
package probe version "0.1.0";
namespace "urn:probe";
function f() -> Rational = ln2();
```
```sh
law engine check packs/examples/language-demo/boundaries/evidence/snippets/ln02.law.txt
```
Observed, in full (exit 1):
```text
packs/examples/language-demo/boundaries/evidence/snippets/ln02.law.txt:4:10: error LDC-E2403: COMPUTABILITY_NOT_PROVED (LDC-E2403): function "f" не доказана как PURE_DETERMINISTIC: вызов "ln2" не имеет доступного effect descriptor (imported/unknown dependency) (§46/§47.5)
packs/examples/language-demo/boundaries/evidence/snippets/ln02.law.txt:4:28: error LDC-E2105: функция "ln2" не объявлена (ни в файле, ни в std v1-списке)
```
The same two layers as the currency pin: name resolution, then
computability proof. The Russian text says the function "is not
proved PURE_DETERMINISTIC" and "is not declared (neither in the file
nor in the std v1-list)".
Second, exact angle conversion (profile 0.7, DECISION-0440
project, versioned policy `units/0.7`):
Standalone D — full content of
`boundaries/evidence/snippets/angle02.law.txt`:
```law
language "law.core" version "0.2";
package probe version "0.1.0";
namespace "urn:probe";
function f() -> Rational = angle_convert(90, "deg", "rad", "units/0.7");
```
```sh
law engine check packs/examples/language-demo/boundaries/evidence/snippets/angle02.law.txt
```
Observed, in full (exit 1):
```text
packs/examples/language-demo/boundaries/evidence/snippets/angle02.law.txt:4:10: error LDC-E2403: COMPUTABILITY_NOT_PROVED (LDC-E2403): function "f" не доказана как PURE_DETERMINISTIC: вызов "angle_convert" не имеет доступного effect descriptor (imported/unknown dependency) (§46/§47.5)
packs/examples/language-demo/boundaries/evidence/snippets/angle02.law.txt:4:28: error LDC-E2105: функция "angle_convert" не объявлена (ни в файле, ни в std v1-списке)
```
Same two codes: naming the `units/0.7` policy in the call does
not conjure an implementation — the term is still outside the
executed slice.
Both refusals are facts about this build and this profile only.
The names are specified (`law.std.data` [§257](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/34-part-xxxiii-standard-library.ru.md#257-lawstddata) export list; `RealExpr`
nullary terms slice 0.5; exact units [§49.3](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#493-точные-единицы-под-версионированной-политикой-decision-0440) slice 0.7) and catalogued
(registry symbols with profiles `0.5`/`0.7`, `experimental`), but
this build executes the 0.2 line only. No version promise follows:
whether any future tool executes profiles 0.5/0.7 is an open
obligation recorded in section 8, not a claim these pins can verify.
## 5. Why this construct
Mira needs to know the usable surface without guessing. In 0.2,
`Integer`, `Natural`, `Decimal`, `Rational`, `Money`, `Quantity`,
`Magnitude`, `Bounds`, `Text`, dates and instants all execute — and
so do `abs`, `pow`, `sum`, `min`, `max`, `count`, `average` (over
`Money`/`Decimal`), `round`, `div_round`, `percent`, `text_length`,
`convert`, `with_unit`, `magnitude`, `unit_convert`, `scalar_of`,
`quantity_of`, `unit_exponent`, every date/time span and bound,
`add_duration`, the three calendar steps, all six certified leaves,
all five bounds compositions, `round_bounds` and `rounds_to`: 67 of
67 in the suite above.
The kind discipline keeps inexactness loud. `1410 KZT / 3.0` carries
the currency into `470 KZT`; `1000 KZT / 3.0` carries an
`INEXACT_DIVISION` issue the test pins by name; `470 KZT + 10 EUR`
stays `NEITHER` — mixed currencies never add. The `Integer` divisor
is refused even earlier, at check time.
The average silence refuses quiet integer means. `average` over
`{12, 9, 15}` as `Integer` fires nothing, while `sum`, `min`, `max`
and `count` over the same readings fire all four. The norm must name
its rounding (`2, "HALF_UP"`) and a roundable kind first.
The calendar separates three different date computations. Three
working days from 2 March land 5 March (the pinned table is
consulted). One calendar week and seven calendar days both land 10
March (the SPEC [§84.2](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/12-part-xii-events-actions-temporal-model.ru.md#842-calendarperiod) pair, no table involved). One calendar month
lands 3 April, not 2 April — `start_count = next_day` shifts the
step, and the suite pins the shifted date, not the naive guess. Ten
calendar days through `add_legal_term` land 12 March. Without the
policy, source and pinned calendar the terms stay silent;
`add_calendar_period` never touches the snapshot.
Derivation equality compares histories, not digits. Every bounds
composition equals itself across all five operations; the
hand-written `bounds_const(5, 6)` never equals the computed sum; the
lifted `ln` over `[1, 1]` equals itself but not the `ln` leaf over
`1` — same interval, different history.
Sufficiency publishes one cell or names two. `round_bounds` of the
certified root of nine at precision zero publishes `3`; `rounds_to`
agrees on the same cell; the neighbouring cell stays silent; the
wide `ln 2` interval at precision ten is `NEITHER` with a
`BOUNDS_INSUFFICIENT` issue naming both extreme cells. No guess is
ever published.
<details>
<summary>What catches the shortcuts?</summary>
Hand-writing the digits where a certified call belongs is caught by
derivation comparison. Calling `exact_sqrt`, `solve_linear`,
`fx_convert` or `currency_convert` is caught louder, at check time,
with the two pinned codes.
</details>
The proof is the 67/67 suite, the `BOUNDS_INSUFFICIENT` and
`INEXACT_DIVISION` issues pinned by name, and ten refusal
reproducers whose outputs are quoted verbatim. What the example does
NOT prove: that the refused names are meaningless — each refusal
names its layer (support vs semantics vs version) and says nothing
about the language in general. Nor does it prove that every `0.2`
name is covered here — `only`, interval predicates and deontic
surfaces belong to their own articles.
## 6. Changed condition
Change one substantial condition: replace the lifted logarithm
with the leaf logarithm as the comparison target. `LnLiftSelf`
compares `ln_bounds(bounds_const(1, 1), "p8/0.1")` with the
textually identical lift and fires `TRUE_ONLY`; `LnLiftLeaf`
compares the same lift with the `ln_bounds(1, "p8/0.1")` leaf and
stays `NEITHER`. The suite pins both (`lifted log is deterministic`
passes, `lift is not the leaf` passes as silence). Same interval
`[0, 0]`, different derivation, different outcome: equality reads
the history, not the digits.
A second change, on the calendar: ask for 2 April instead of 3 April
as the month step and the rule goes silent. `start_count = next_day`
is part of the answer, not of the question — the shifted date is the
specified one.
## 7. Typical mistake
The mistake is averaging integers and expecting twelve. Over
readings 12, 9 and 15 the mean is exactly twelve in every
schoolbook, yet `AvgSilent` fires nothing: `average` over `Integer`
has no rounding policy to apply and refuses the quiet integer
division.
The observable consequence is precise — `NEITHER`, pinned green by
the test `average over integers stays silent`. The fix is explicit
too: average the `Money` bills with `2, "HALF_UP"`, or average
`Decimal` samples. The same shape of mistake with `div_round` over
a `Quantity`, or `/` with an `Integer` divisor, is refused even
earlier — statically, with `LDC-E2108`.
## 8. Limits
Applicability bounds, all verified against tool `law 0.1.0`,
semantics `law.core/0.2`, std `0.2.0`. Refusals below are facts
about this build and this profile, never claims about the language
in general.
`Number`, `Algebraic`, `RealExpr`, `exact_sqrt`, `pi`, `ln2`,
`solve_linear`, `poly_nroots_2/3`, `poly_root_2/3`, `temp_convert`,
`angle_convert` and `fx_convert` (profiles 0.4–0.8) are refused at
two layers: `LDC-E2105` (not in the std v1-list) plus `LDC-E2403`
(no effect descriptor). The three types alone are refused with
`LDC-E2101`. Each has a frozen reproducer in `evidence/snippets/`
and an open obligation: a future tool with a 0.4–0.8 implementation
passes these layers, and these pins say nothing until then.
`currency_convert` is named by [§260](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/34-part-xxxiii-standard-library.ru.md#260-lawstdmoney) but sits in no executable
slice: same two codes, same treatment, same open obligation.
`average` over `Integer`/`Rational` stays silent (no quiet
division); `div_round` over `Quantity` and `/` with an `Integer`
divisor are static `LDC-E2108`.
`add_business_days` and `add_legal_term` over day units read the
pinned calendar through the deadline policy; without policy, source
and calendar they stay silent. `add_calendar_period` never reads
the snapshot, but it reads `start_count` (and `month_end` for
month/year steps).
Rule-body folding observes only the `TRUE_ONLY` arm of `rounds_to`
and `text_matches`: a wrong cell and an insufficient interval both
read as silence on the head relation. The arms are told apart one
level down — the term publishes the true cell, or raises
`BOUNDS_INSUFFICIENT` naming both extreme cells.
## 9. Exercise
Extend the water billing with a late-payment rule: a bill of
1,880 KZT split over four months is exactly 470 KZT per month, but
the same bill split over three months must be loud, not rounded.
Write one package rule plus two tests — (a) `truth == TRUE_ONLY`
for the exact quarterly split against 470 KZT, (b)
`issue(INEXACT_DIVISION)` for the three-way split — and run `law
test` on the package. Checkable expectation: both new tests pass
and the suite total grows by exactly two with zero failures.
Second, refusal reading. Run both `law engine check` commands from
section 4 and name, for each probe, the two diagnostic codes plus
the layer each belongs to (name resolution vs computability proof).
Then change the `ln2` probe's return type from `Rational` to
`RealExpr`, predict the new diagnostic set before running, and run
to confirm. Checkable solution:
[full solution with checkable answers](/tutorials/northbridge/solutions/nb-23-solutions/).
## 10. Sources
Northbridge role → domain template → confirmed external
formalization. Full sources: the package
[README](https://github.com/arxohq/law/blob/master/packs/examples/language-demo/numerics/README.md),
[package.law](https://github.com/arxohq/law/blob/master/packs/examples/language-demo/numerics/package.law)
and [tests](https://github.com/arxohq/law/blob/master/packs/examples/language-demo/numerics/tests/numerics.lawtest);
refusal pins in
[evidence/snippets/](https://github.com/arxohq/law/blob/master/packs/examples/language-demo/numerics/evidence/snippets/).
Water billing story → `demo.northbridge.numerics` (this article's
new template): meter thresholds, quarterly bills, notice and due
dates against the pinned March 2026 table.
Exact arithmetic, rounding, dimensions and certified bounds →
`law.std.data` [§257](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/34-part-xxxiii-standard-library.ru.md#257-lawstddata), `law.std.time` [§258](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/34-part-xxxiii-standard-library.ru.md#258-lawstdtime), `law.std.units` [§259](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/34-part-xxxiii-standard-library.ru.md#259-lawstdunits),
`law.std.money` [§260](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/34-part-xxxiii-standard-library.ru.md#260-lawstdmoney); calendar steps → [§84](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/12-part-xii-events-actions-temporal-model.ru.md#84-duration-types)–[§86](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/12-part-xii-events-actions-temporal-model.ru.md#86-deadline-policy); rounding formula →
[§64.2](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/10-part-x-propositions-and-four-valued-support.ru.md#642-отношение-округления-над-сертифицированными-границами-errata-e-0136); version lines 0.4–0.8 → registry
`spec/feature-registry.json`.
No external formalization is claimed for the refused profiles: the
0.4–0.8 semantics are design decisions (DECISION-0436/0438–0441
project, 0437 accepted 30.09.2026), and this build executes the 0.2
line only.
Confirmed external formalization on the 0.2 line (corpus):
five-year prescription deadline (French Civil Code, prescription
title) — package `fr.code_civil`,
`corpus/laws/fr/code-civil/20-prescription-extinctive.law:122-129`.
The period is built by a calendar step
(`then echeance_prescription_le(c, add_calendar_period(depart, 5 calendar_year))`),
not measured in days, with the policy carried by a case-context
line in every scenario test. Evidence:
`docs/research/constructs/20-deadline-calendar/corpus-forms.en.md`
[§1](/tutorials/northbridge/nb-01-first-permit/#1-situation) (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.