Markdown for LLMs
nb-16 — Exact computation and proven bounds
The source Markdown for this article. Copy it into your assistant or download it as a text file.
# nb-16 — Exact computation and proven bounds
*Northbridge course, math branch (needs beginner only; companion to
[nb-15: Quantities and dimensions](/tutorials/northbridge/nb-15-quantities/)). 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](/tutorials/northbridge/nb-01-first-permit/):
facts, one rule, one question, and `law test` as the way to check a
claim. [nb-04: The permit fee](/tutorials/northbridge/nb-04-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:
```law
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:
```law
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:
```law
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:
```law
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:
```sh
law test packs/examples/language-demo/math02
```
Observed result (engine `law 0.1.0`):
```text
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:
```sh
law engine check packs/examples/language-demo/math02/package.law
```
```text
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](/tutorials/northbridge/nb-04-permit-fee/):
```sh
law test packs/examples/language-demo/calculations
```
```text
итого: 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.
<details>
<summary>Why not plain decimals or silent rounding?</summary>
`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.
</details>
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:
```sh
law engine check packs/examples/language-demo/boundaries/evidence/snippets/sqrt02.law.txt
```
```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 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](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/34-part-xxxiii-standard-library.ru.md#2592-сертифицированные-границы-errata-e-0136-decision-0154) 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`:
1. `load_scalar(5/1)` given `load_q(5 m)` — truth status, and why the
fraction form matters rather than `5.0`?
2. `heavy_load()` given `load_q(22 kW)` — truth status? Which premise
of `HeavyLoad` is never satisfied, and why?
3. `bounds_same()` — truth status? What would `bounds_ok()` return for
the same arithmetic, and what single property differs between them?
4. `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](/tutorials/northbridge/solutions/nb-16-solutions/).
## Sources
1. **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.
2. **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.
3. **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.
4. **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](/tutorials/northbridge/nb-01-first-permit/#3-minimal-example) (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.
## Links
- Source: `packs/examples/language-demo/math02/package.law`
- Tests: `packs/examples/language-demo/math02/tests/math02.lawtest`
- Suite tour: `packs/examples/language-demo/README.md`
- Refusal surface: `packs/examples/language-demo/boundaries/evidence/snippets/sqrt02.law.txt`
(exact_sqrt in a 0.2 package), `packs/examples/language-demo/boundaries/README.md`
- Language reference: `docs/language/08-cheat-sheet.law.md`
(`Rational`, `Money`, `Bounds`, `round`/`div_round`/`round_bounds`/`scalar_of` signatures)
- Prerequisite: [nb-04: The permit fee](/tutorials/northbridge/nb-04-permit-fee/); math-branch companion:
[nb-15: Quantities and dimensions](/tutorials/northbridge/nb-15-quantities/)