nb-23 — Numbers and the standard library: every figure the 0.2 machine proves

← Course mapChapter 23 / 25 · Advanced II

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 (TRUE_ONLY = established, NEITHER = established neither way).

2. Prerequisites

nb-01: First permit: facts, a rule and a question: facts, strict rules, the four truth statuses, law test as the way to check a claim. nb-04: The permit fee: Money arithmetic and HALF_UP rounding — the everyday numbers this article completes. nb-15: Quantities and dimensions: Quantity, Magnitude, units.si, explicit conversion. nb-16: Exact computation and proven bounds: exact rationals and derivation-carrying Bounds. nb-17: Numeric families and support boundaries: 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.

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:

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:

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:

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 (AvgSilent, AvgBill over Money, AvgSample over Decimal) and 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/.

4. Command and result

Pin the machine first: five facts — tool, language, semantics, std, binary. Run from the repository root:

law --version

Observed:

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:

law test packs/examples/language-demo/numerics

Observed (last lines; engine law 0.1.0):

  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:

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:

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:

law engine check packs/examples/language-demo/numerics/evidence/snippets/fx02.law.txt

Observed, in full:

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/§47.5).

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:

language "law.core" version "0.2";
package probe version "0.1.0";
namespace "urn:probe";
function f() -> Rational = ln2();

law engine check packs/examples/language-demo/boundaries/evidence/snippets/ln02.law.txt

Observed, in full (exit 1):

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:

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");

law engine check packs/examples/language-demo/boundaries/evidence/snippets/angle02.law.txt

Observed, in full (exit 1):

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 export list; RealExpr nullary terms slice 0.5; exact units §49.3 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 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.

What catches the shortcuts?

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.

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

10. Sources

Northbridge role → domain template → confirmed external formalization. Full sources: the package README, package.law and tests; refusal pins in 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, law.std.time §258, law.std.units §259, law.std.money §260; calendar steps → §84–§86; rounding formula → §64.2; 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 (rated exemplary). Limit of verification: presence of the named construct at the cited lines only, confirmed by direct file read; no claim about deployment, runtime behaviour, or legal correctness.

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

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