nb-16 — Exact computation and proven bounds

← Course mapChapter 16 / 25 · Mathematics branch

Northbridge course, math branch (needs beginner only; companion to nb-15: Quantities and dimensions). All law is fictional; every act, load figure and threshold is synthetic and unofficial. Northbridge itself is a synthetic training story — no real deployment and no claim about live legislation follows from anything below. Engine law 0.1.0, semantics law.core/0.2, std 0.2.0.

Situation

A Northbridge inspector certifies a new substation feeder. Is a declared 120 kW transformer load really at or above the 44-unit heavy-load threshold — exactly, with no floating-point doubt in the comparison? Does a feeder run declared as 5 km clear the 1000 m long-trip mark, again with nothing silently rounded on the way? And where a number is genuinely uncertain, she wants a proven interval — a lower and an upper bound the answer is guaranteed to sit between — that still settles the question.

This article turns that desk work into four mechanisms: fractions kept as fractions, Money arithmetic that never rounds silently, rounding that always names its mode, and proven intervals that remember how they were computed. You will run the exact-scalar, rounding and bounds tests, watch a computed interval refuse to equal a hand-written twin, then change one condition and watch it equal itself. Each term is introduced where it is first used.

Prerequisites

nb-01: First permit: facts, a rule and a question: facts, one rule, one question, and law test as the way to check a claim. nb-04: The permit fee: typed constants, pure functions, Money with its currency, and the fact that rounding is always an explicit call (round, div_round) with a named mode such as "HALF_UP". This article adds exactness and intervals on top: nothing here changes truth statuses, and no advanced construct (procedures, appeals, precedents) is required.

Minimal example

Excerpt from packs/examples/language-demo/math02/package.law (lines 39–42, identifiers as written) — the exact-scalar chain:

rule LoadScalar(q: Quantity) strict {
    when load_q(q);
    then load_scalar(scalar_of(magnitude(q) / magnitude(1 m)));
}

Look at the head: a magnitude is the bare numeric content of a quantity once its unit is fixed, so the division forms a dimensionless ratio and scalar_of turns it into a Rational — an exact rational value, serialized as an irreducible fraction such as 5/1, never 5.0. The division inside is exact: no precision is lost between the measured quantity and the scalar.

Excerpt from the same file (lines 51–56) — the threshold asked against that exact scalar, the threshold itself an exact (44/1)-form literal:

rule HeavyLoad strict {
    for v: Rational;
    when load_scalar(v)
        and v >= (44/1);
    then heavy_load();
}

Excerpt from the same file (lines 123–124) — rounding done out loud. round rounds an already computed value; div_round divides and rounds the exact quotient — each to a precision, under a named mode:

pure function half_rounded(x: Decimal) -> Decimal = round(x, 0, "HALF_UP");
pure function ratio_seventh() -> Decimal = div_round(7.0, 2.0, 1, "HALF_UP");

Excerpt from the same file (lines 102–112) — bounds carry their derivation. The first rule compares a computed sum against a foreign-written literal; the second compares the computation against itself:

rule BoundsOk strict {
    when bounds_add(bounds_const(1, 2), bounds_const(1, 3)) == bounds_const(5, 6);
    then bounds_ok();
}

relation bounds_same() kind institutional;

rule BoundsSame strict {
    when bounds_add(bounds_const(1, 2), bounds_const(1, 3)) == bounds_add(bounds_const(1, 2), bounds_const(1, 3));
    then bounds_same();
}

Look at the two when lines side by side: both compute the same interval sum, but the right-hand side differs. bounds_const(1, 2) is the degenerate interval [1/2, 1/2], and bounds_add is the interval sum [a.lo + b.lo, a.hi + b.hi]. A derivation is the record of which computation produced a value — two textually identical expressions evaluated separately have different derivations — and == on bounds is derivation-sensitive: it holds only between values sharing one derivation.

Command and result

The math02 package is self-contained (its test world pins demo.northbridge.math02 plus units.si), so one command checks everything:

law test packs/examples/language-demo/math02

Observed result (engine law 0.1.0):

law test demo.northbridge.math02: мир demo.northbridge.math02, units.si
  ok   [demo.northbridge.math02] tests/math02.lawtest / days between dates
  ok   [demo.northbridge.math02] tests/math02.lawtest / hours and minutes between instants
  ok   [demo.northbridge.math02] tests/math02.lawtest / minutes between instants
  ok   [demo.northbridge.math02] tests/math02.lawtest / period starts and ends
  ok   [demo.northbridge.math02] tests/math02.lawtest / end of month
  ok   [demo.northbridge.math02] tests/math02.lawtest / year boundaries
  ok   [demo.northbridge.math02] tests/math02.lawtest / end of year
  ok   [demo.northbridge.math02] tests/math02.lawtest / day of week
  ok   [demo.northbridge.math02] tests/math02.lawtest / text length
  ok   [demo.northbridge.math02] tests/math02.lawtest / scalar of five kilometres in metres
  ok   [demo.northbridge.math02] tests/math02.lawtest / load scalar below the threshold is not derived
  ok   [demo.northbridge.math02] tests/math02.lawtest / scalar capped above by the second threshold
  ok   [demo.northbridge.math02] tests/math02.lawtest / kilometres converted to metres
  ok   [demo.northbridge.math02] tests/math02.lawtest / short trip fails the threshold
  ok   [demo.northbridge.math02] tests/math02.lawtest / rounding
  ok   [demo.northbridge.math02] tests/math02.lawtest / division with precision
  ok   [demo.northbridge.math02] tests/math02.lawtest / minimum and maximum of the set
  ok   [demo.northbridge.math02] tests/math02.lawtest / maximum of the set
  ok   [demo.northbridge.math02] tests/math02.lawtest / sum of the set
  ok   [demo.northbridge.math02] tests/math02.lawtest / count of the set
  ok   [demo.northbridge.math02] tests/math02.lawtest / bare variable compared against the threshold
  ok   [demo.northbridge.math02] tests/math02.lawtest / decimal literals compared
  ok   [demo.northbridge.math02] tests/math02.lawtest / computed value compared against the threshold
  ok   [demo.northbridge.math02] tests/math02.lawtest / bounds carry derivation: foreign derivation is unequal
  ok   [demo.northbridge.math02] tests/math02.lawtest / bounds addition executes
  ok   [demo.northbridge.math02] tests/math02.lawtest / exact scalar value (5 m)
  ok   [demo.northbridge.math02] tests/math02.lawtest / determinism: the same addition equals itself
  ok   [demo.northbridge.math02] tests/math02.lawtest / guard fact visible to the rule
  ok   [demo.northbridge.math02] tests/math02.lawtest / quantity clamp: max yields scalar 120
  ok   [demo.northbridge.math02] tests/math02.lawtest / bounds division: foreign derivation is unequal
  ok   [demo.northbridge.math02] tests/math02.lawtest / bounds multiplication: foreign derivation is unequal
  ok   [demo.northbridge.math02] tests/math02.lawtest / bounds subtraction: foreign derivation is unequal
  ok   [demo.northbridge.math02] tests/math02.lawtest / bounds scaling: foreign derivation is unequal
  ok   [demo.northbridge.math02] tests/math02.lawtest / division determinism: the same quotient equals itself
  ok   [demo.northbridge.math02] tests/math02.lawtest / bounds root: foreign derivation is unequal
  ok   [demo.northbridge.math02] tests/math02.lawtest / bounds root is deterministic
  ok   [demo.northbridge.math02] tests/math02.lawtest / certified functions are deterministic
  ok   [demo.northbridge.math02] tests/math02.lawtest / foreign profile is unequal
  ok   [demo.northbridge.math02] tests/math02.lawtest / bounds rounding yields a value
  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

The static check passes too:

law engine check packs/examples/language-demo/math02/package.law

check OK: packs/examples/language-demo/math02/package.law

All 42 answers matched their expectations. The Russian summary reads итого: 42 проверено, 42 прошли, 0 не прошли, 0 не исполнены; код 0 — 42 checked, 42 passed, 0 failed, 0 unexecuted, exit code 0 — and the header again pins the units.si world member the conversions need.

Five of those forty-two tests carry this article. exact scalar value (5 m) asserts load_q(5 m) and asks truth(load_scalar(5/1)): TRUE_ONLY — the inspector’s exact fraction is really there. scalar of five kilometres in metres asserts load_q(5 km) and asks truth(heavy_load()): TRUE_ONLY, since the scalar 5000 clears (44/1). rounding evaluates half_rounded(2.5) and expects 3.0; division with precision evaluates ratio_seventh() and expects 3.5 — both roundings land where the named mode says they should. bounds addition executes evaluates bounds_add(bounds_const(1, 2), bounds_const(1, 3)) and expects COMPUTED — the arithmetic runs; equality is the next section’s question.

Money exactness is confirmed next door, in the fee package from nb-04: The permit fee:

law test packs/examples/language-demo/calculations

итого: 9 проверено, 9 прошли, 0 не прошли, 0 не исполнены; код 0

3 * 10 EUR is exactly 30 EUR: the currency travels with the value, nothing rounded along the way. The summary (9 проверено, 9 прошли, 0 не прошли — 9 checked, 9 passed, 0 failed) confirms the whole fee package agrees.

Why this construct

The inspector needs “at or above the threshold” and “the rounded share” certified so the machine gives the same answer every run — no binary-float wobble, no hidden rounding step. Rational keeps fractions exact, Money keeps currency exact, explicit round/div_round puts precision and mode in the open, and Bounds answers with a proven interval that records how it was derived.

Why not plain decimals or silent rounding?

Decimal literals (120.0 >= 44.0, the dec_ok test) compare fine for terminating decimals, but only Rational stays exact through division. And rounding without a named mode would hide which rounding the clerk approved.

The evidence is the tests above: exact scalar value (5 m) for exactness, rounding and division with precision for named-mode rounding, bounds addition executes plus the derivation pair below for bounds. What is not proven is that 44, 1000 m or HALF_UP are the right thresholds or the right mode. The tests prove the machine applies the declared numbers; no test can prove the inspector picked wisely. Figures are fictional data, not legal advice.

Changed condition

Change one side of the bounds comparison: a foreign literal becomes the identical computation. bounds_ok() asks whether bounds_add(bounds_const(1, 2), bounds_const(1, 3)) equals the separately written bounds_const(5, 6) — same arithmetic, different derivation — and the answer is NEITHER. bounds_same() asks the same sum against itself, and the answer is TRUE_ONLY. Same numbers, same operation; only the derivation identity changed, and the verdict flipped with it, because == on bounds compares derivations, not digits.

The pattern repeats across every bounds operation. Division, multiplication, subtraction, scaling and the certified root each have a foreign-derivation test (NEITHER) plus a determinism twin (div_self, sqrt_self: TRUE_ONLY). Even the precision profile is part of the derivation: cert_cross compares sin_bounds(0, "p8/0.1") against sin_bounds(0, "p16/0.1") and gets NEITHER, while cert_all compares each certified function against itself and gets TRUE_ONLY.

Bounds still settle a downstream result when the rule asks what the interval guarantees. round_ok() holds because round_bounds(bounds_const(1, 2), 2, "HALF_UP") is provably 0.5 (bounds rounding yields a value: TRUE_ONLY). Sufficiency is not “the interval looks right” — it is “compared against the same derivation, or reduced to the value the interval guarantees”.

Typical mistake

The mistake is expecting a computed bounds value to equal a hand-written literal with the same endpoints. A newcomer reads bounds_add(bounds_const(1, 2), bounds_const(1, 3)), works out [5/6, 5/6] on paper, writes bounds_const(5, 6) on the other side of ==, and expects TRUE. The observable consequence is NEITHER — the bounds_ok test pins exactly this. The arithmetic is right; the comparison is not, because == on bounds also checks who derived it.

The fix: never assert equality between a bounds computation and a foreign literal. Compare a computation against itself, or reduce the bounds to a guaranteed value first (round_bounds) and compare that — textual equality of the endpoints is not enough.

Limits

Everything above runs under the verified profile only: law 0.1.0, law.core/0.2. Exact square roots are a 0.4-profile feature and are refused in a 0.2 package — a refusal of this profile and implementation, not a language-wide inability:

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

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 refusal names both layers: LDC-E2403 says the function is not proved PURE_DETERMINISTIC (no effect descriptor for exact_sqrt), and LDC-E2105 says the name is not declared in the file or the std list. The certified stand-ins (sqrt_bounds, sin_bounds, cos_bounds, exp_bounds, ln_bounds, pi_bounds with a "p8/0.1"-style profile) are the 0.2-executable form; mixing profiles (p8 vs p16) compares unequal by design.

Exactness is not contagious. Rational and Money are exact; Decimal division that needs a fixed precision must go through div_round with a named mode. There is no default rounding anywhere — a computation that needs rounding and does not call for it does not get it silently.

Bounds equality is derivation-sensitive by contract. Any rule that asserts computed-bounds == foreign-literal will stay NEITHER. This is the documented §259.2 semantics (determinism of one’s own derivation), not a prover gap to work around.

scalar_of needs its two conditions. The registry plumbing behind the exact scalar requires the units.si import and units.si explicitly in the test world (see the P10 lesson comment in the package source). Without both, resolution fails silently.

Exercise

Without running the engine, predict, then check with law test:

load_scalar(5/1) given load_q(5 m) — truth status, and why the fraction form matters rather than 5.0?
heavy_load() given load_q(22 kW) — truth status? Which premise of HeavyLoad is never satisfied, and why?
bounds_same() — truth status? What would bounds_ok() return for the same arithmetic, and what single property differs between them?
cert_cross() — truth status? What does it tell you about the precision profile as part of a derivation?

Write down each prediction first; run the suite; explain any miss in one sentence. Check your work against the full solution: exact scalar, threshold, derivation pair and profile.

Sources

Northbridge use (this article): exact scalar chain (LoadScalar/HeavyLoad), named-mode rounding (half_rounded, ratio_seventh), bounds derivation pair (BoundsOk/BoundsSame), verified by the 42-test math02 run above.
Domain template: whenever a threshold decision must be reproducible, compute in Rational, compare against an exact (n/1)-form literal, round only through round/div_round with a named mode, and compare bounds only against their own derivation or against a value the interval provably reduces to.
Confirmed formalization elsewhere: exact Money arithmetic in demo.northbridge.calculations (permit_fee(3) is exactly 30 EUR, 9 checked, 9 passed) — same exactness contract, different value family.
Confirmed external formalization (corpus): High-36 average retired-pay base (10 U.S.C. §1407(c)(1)) — package us.code.military_retirement, corpus/laws/us/military-retirement/01-retired-pay.law:271-281: div_round(Money, Decimal, scale, policy) single-rounding share (then retired_pay_base(m, div_round(t, 36.0, 2, "HALF_UP"))) — Money divided by a Decimal divisor (36.0, not 36), one rounding over the exact quotient under an explicit HALF_UP policy, no double rounding. Evidence: docs/research/constructs/21-expressions-quantities/corpus-forms.en.md §3 (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.