Markdown for LLMs
nb-15 — Quantities and dimensions
The source Markdown for this article. Copy it into your assistant or download it as a text file.
# nb-15 — Quantities and dimensions
*Math branch, needs beginner only ([nb-01: First permit: facts, a rule and a question](/tutorials/northbridge/nb-01-first-permit/) → [nb-02: Why a missing fact is not a refusal](/tutorials/northbridge/nb-02-missing-fact/) → [nb-03: Exceptions and conflicting rules](/tutorials/northbridge/nb-03-exceptions/) → [nb-04: The permit fee](/tutorials/northbridge/nb-04-permit-fee/)).
All law is fictional; every depot, truck route and load record is
synthetic and unofficial. No real municipal deployment or legal-validity
claims. Engine `law 0.1.0`, semantics `law.core/0.2`.*
## Situation
Northbridge runs a depot scale for road-maintenance trucks. Two
readings arrive on the same morning: truck A reports a trip length of
5 kilometres, truck B reports an axle load of 22 kilowatts of
auxiliary draw. The clerk's register has one threshold for "heavy
load" (44, in metres of wire-equivalent test load) and one for "long
trip" (1000 metres). The clerk asks two questions: is truck A heavy,
and is either trip long? The trap is that the readings carry
different dimensions — length versus power — and the numbers 5 and 22
mean nothing until each is reduced to a plain number in a named unit.
This article shows the 0.2 mechanism for that reduction. A reading
such as `5 km` is kept as one value — number glued to unit — until
an explicit step converts it and reduces it to a plain number the
threshold can judge. You will run that two-step chain for the heavy
and long verdicts, then for conversions and custom unit tags. 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, 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 comparison against
a threshold — the same shape as the scalar comparison here, but
Money needs no conversion step.
New here: quantities with units, explicit conversion, and the
two-rule meld/scalar chain — each introduced where it first appears
below.
## Minimal example
All fragments are excerpts: package header, imports and unrelated
rules cut. Identifiers as written.
Excerpt 1 — the meld/scalar chain (from
`packs/examples/language-demo/math02/package.law`, rules
`LoadScalar` and `HeavyLoad`). A **head computation** derives a
scalar relation from each quantity fact; a second rule compares the
bare variable against a Rational threshold.
```law
rule LoadScalar(q: Quantity) strict {
when load_q(q);
then load_scalar(scalar_of(magnitude(q) / magnitude(1 m)));
}
rule HeavyLoad strict {
for v: Rational;
when load_scalar(v)
and v >= (44/1);
then heavy_load();
}
```
Look at how the two rules divide the work. `LoadScalar` takes a
**Quantity** fact — a number glued to a unit, such as `5 km` — and
computes a scalar relation from it in the rule head: `magnitude(q)`
extracts the unit-carrying **Magnitude**, dividing by `magnitude(1
m)` forms a dimensionless ratio, and `scalar_of` turns that ratio
into a plain **Rational** number such as `5000/1`. The quantity
never meets the threshold directly; it is first *melded* into
`load_scalar`. `HeavyLoad` then compares that bare variable against
the Rational threshold `(44/1)`. Head computation plus bare-variable
comparison: that pair is the **meld/scalar chain**.
Excerpt 2 — explicit conversion before the same two-step pattern
(same file, rules `TripLength` and `LongTrip`):
```law
rule TripLength strict {
for q: Quantity;
when load_q(q);
then trip_length(scalar_of(unit_convert(magnitude(q), "m") / magnitude(1 m)));
}
rule LongTrip strict {
for v: Rational;
when trip_length(v)
and v >= (1000/1);
then long_trip();
}
```
Look at the head of `TripLength`: `unit_convert(magnitude(q),
"m")` states the target unit out loud — kilometres become metres
here, with no silent coercion. The rest is the same chain: scalar
first, threshold second. The only difference from Excerpt 1 is that
the conversion step is explicit in the call instead of implied by
the divisor.
Excerpt 3 — quantities built from raw numbers (same file, rule
`ConvOk`): `with_unit` attaches a tag, `convert` re-expresses the
value, and the equality is checked, not assumed.
```law
rule ConvOk strict {
when convert(with_unit(1, "km"), 1000, 1, "m") == with_unit(1000, "m");
then conv_ok();
}
```
Look at the single `when` line: `with_unit` builds a quantity from
a raw number plus an explicit tag, `convert` re-expresses it with a
stated factor (1000/1) and target tag, and the `==` checks the
result instead of assuming it. 1 km converts to 1000 m only because
both sides were constructed with stated units — the rule fires on
the equality of two explicit constructions.
Excerpt 4 — custom unit tags resolve locally (from
`packs/examples/language-demo/boundaries/package.law`, declarations
plus rule `PermitTagged`):
```law
unit permit = 1;
derived unit permit_rate = permit / permit;
rule PermitTagged strict {
when with_unit(5, "permit") == with_unit(5, "permit");
then permit_tagged();
}
```
Look at the declarations above the rule: `unit permit = 1` coins
a local tag, and `derived unit permit_rate = permit / permit`
derives a rate tag from it. The rule then compares two `with_unit`
quantities over the local tag. Units are not limited to the SI
registry — a package can declare its own tags for countable
non-physical things.
## Command and result
```sh
law test packs/examples/language-demo/math02
```
Observed result (engine `law 0.1.0`) — the header names the pinned
world, then 42 passing lines (seven shown, the rest cut for
brevity):
```text
law test demo.northbridge.math02: мир demo.northbridge.math02, units.si
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 / kilometres converted to metres
ok [demo.northbridge.math02] tests/math02.lawtest / short trip fails the threshold
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 — a passing suite, not a
verdict on any truck. The Russian summary reads `итого: 42 проверено,
42 прошли, 0 не прошли, 0 не исполнены; код 0` — 42 checked, 42
passed, 0 failed, 0 unexecuted, exit code 0. The header matters too:
the world (`мир`) lists `units.si` explicitly, and the SI registry
resolves only because that dependency is a pinned world member, not
merely an import (see Limits). The boundaries package confirms the
custom-tag side:
```sh
law test packs/examples/language-demo/boundaries
```
Observed — both tag tests pass inside a 21/21 green suite
(`итого: 21 проверено, 21 прошли, 0 не прошли, 0 не исполнены; код
0` — 21 checked, 21 passed, 0 failed, 0 unexecuted, exit code 0):
```text
ok [demo.northbridge.boundaries] tests/boundaries.lawtest / declared unit tag resolves
ok [demo.northbridge.boundaries] tests/boundaries.lawtest / derived tag resolves
итого: 21 проверено, 21 прошли, 0 не прошли, 0 не исполнены; код 0
```
Both packages also pass the static check (`check OK` for each
`package.law`), which confirms the sources are well-formed before
any test runs:
```sh
law engine check packs/examples/language-demo/math02/package.law
```
Observed: `check OK: packs/examples/language-demo/math02/package.law`.
The source is well-formed; the suite results above are its behavior.
## Why this construct
The Quantity keeps number and unit inseparable, so bare numbers never
meet thresholds. `load_q(5 km)` carries its dimension, and nothing
compares it until the chain reduces it. The `scalar of five
kilometres in metres` test derives `heavy_load()` from that fact
(5000 ≥ 44).
Conversion states its target instead of guessing it.
`unit_convert(magnitude(q), "m")` names `"m"` in the call, and
`convert(with_unit(1, "km"), 1000, 1, "m")` names the factor too.
The `kilometres converted to metres` and `unit conversion by value`
tests confirm both with TRUE_ONLY.
The two-rule chain separates computing from judging, so one scalar
serves several thresholds. `LoadScalar` feeds both `HeavyLoad`
(≥ 44) and `VeryHeavy` (≥ 121): one meld, two verdicts. The
five-kilometre test fires `HeavyLoad` through the shared
`load_scalar`, while `scalar capped above by the second threshold`
leaves `very_heavy()` NEITHER.
<details>
<summary>What LoadMax proves (and does not)</summary>
`LoadMax` is a separate clamped derivation: the `quantity clamp: max
yields scalar 120` test derives `load_max(120/1)` from `load_q(120
kW)`. It is consumed by no rule, so it proves the clamp runs — not
that any verdict reads it.
</details>
Custom tags cover non-physical dimensions: the depot counts permits
the way metres count length. `unit permit = 1` plus `with_unit(5,
"permit")` gives the paperwork its own quantity system, confirmed by
the two boundaries `tag resolves` tests above.
<details>
<summary>Why not a bare Integer with a comment?</summary>
A bare `Integer` fact plus a comment saying "metres" would pass every
suite — and would also let a kilometre figure walk into a metre
threshold unconverted. The suite cannot tell the comment is a lie.
The Quantity type can, because the conversion step is code, not
prose.
</details>
The evidence is the 42/42 suite, the 21/21 boundaries suite, and the
two `check OK` runs — each executed above, none asserted in prose.
What is not proven is that 44 is the right heaviness bar, or that
wire metres are a sane proxy for truck load. The machine proves the
declared arithmetic ran; Northbridge's thresholds are fictional data,
not engineering advice.
## Changed condition
Feed `load_q(5 km)`: `LoadScalar` melds it to `5000/1` and
`HeavyLoad` fires — TRUE_ONLY (`scalar of five kilometres in
metres`). Change the single fact to `load_q(22 kW)` and `heavy_load()`
becomes NEITHER (`load scalar below the threshold is not derived`).
Note what the suite does *not* tell you here: no suite test pins
`load_scalar` for a kW reading, so this NEITHER fits two stories —
"melded to 22/1, below 44" and "the metre-divisor meld accepted
nothing". A scratch probe outside the suite settles the pair:
`load_q(22 kW)` with the question `load_scalar(22/1)` returns
NEITHER, while `load_q(22 m)` returns TRUE_ONLY. The second story
wins — the silent-meld failure mode documented in Limits — so no
threshold comparison ever runs for a kW reading.
The trip pair shows conversion doing the work. `load_q(5 km)`
converts to 5000 m and clears the 1000 bar (`kilometres converted
to metres`, TRUE_ONLY); `load_q(0.5 km)` converts to 500 m and
stays NEITHER (`short trip fails the threshold`). Without
`unit_convert`, the raw 5 and 0.5 could never meet a metre
threshold honestly.
## Typical mistake
The mistake is reaching past the 0.2 shelf for a converter from a
newer profile — temperature conversion `temp_convert` (0.7) inside
a 0.2 package:
```sh
law engine check packs/examples/language-demo/boundaries/evidence/snippets/temp02.law.txt
```
Observed:
```text
packs/examples/language-demo/boundaries/evidence/snippets/temp02.law.txt:4:10: error LDC-E2403: COMPUTABILITY_NOT_PROVED (LDC-E2403): function "f" не доказана как PURE_DETERMINISTIC: вызов "temp_convert" не имеет доступного effect descriptor (imported/unknown dependency) (§46/§47.5)
packs/examples/language-demo/boundaries/evidence/snippets/temp02.law.txt:4:39: error LDC-E2105: функция "temp_convert" не объявлена (ни в файле, ни в std v1-списке)
```
The snippet is a four-line probe (`function f(x: Rational) ->
Rational = temp_convert(x, "absolute", "C", "K");`); the engine
refuses it twice over — unknown name (`LDC-E2105`, "not declared")
and unprovable purity (`LDC-E2403`, "not proved
PURE_DETERMINISTIC"). The angle converter fails identically
(`angle02.law.txt`: `angle_convert`, same two codes).
The fix is to model the quantity with the tools that execute
(`unit_convert`, `convert`, `with_unit`), and to treat anything
else as a job for [nb-17: Numeric families and support boundaries](/tutorials/northbridge/nb-17-numeric-families/)' profiles,
not a silent approximation here. Rule of thumb: if the conversion
is not in the 0.2 executable subset, the honest answer is a refusal
at check time.
## Limits
SI resolution needs explicit world membership. Importing `units.si`
is not enough: it must also be pinned in the test world (the suite
header shows it). The package source documents the failure mode —
without it, `magnitude()`/`unit_convert()` hit UNIT_UNKNOWN and the
rules go silently NEITHER. That silence is a recorded open issue of
this build, not a verdict on the data.
Computation runs in heads only. `magnitude()`, `scalar_of()` and
`unit_convert()` run in rule heads and conditions (the meld pattern);
the std catalog marks them not callable from pure functions
(`function_callable=false`, `LDC-E2403`). Per the package source
comment, that is a refusal of this implementation's purity checker,
never a language-wide inability claim.
The boundaries are profile facts. `LDC-E2105`/`LDC-E2403` on
`temp_convert`, `angle_convert` (0.7), `exact_sqrt` (0.4),
`fx_convert` and `solve_linear` describe this implementation
(`law 0.1.0`, semantics `law.core/0.2`), never the language in
general. What refuses here may execute under its own profile in
[nb-17: Numeric families and support boundaries](/tutorials/northbridge/nb-17-numeric-families/).
Derived equality is derivation-sensitive. `with_unit(5, "permit") ==
with_unit(5, "permit")` holds for identical constructions; equality
of computed quantities follows the same derivation rules as bounds
([nb-16: Exact computation and proven bounds](/tutorials/northbridge/nb-16-exact-bounds/)).
This article proves local construction, not a general quantity
algebra.
## Exercise
Without running the engine, predict, then check with the commands
above:
1. `load_q(5 km)` versus `load_q(22 kW)`: which truth status does
`heavy_load()` get for each, and which melded scalar feeds the
comparison in each case, if any?
2. `load_q(5 km)` versus `load_q(0.5 km)`: which clears `long_trip()`,
and which explicit call performs the kilometre-to-metre step?
3. What does `convert(with_unit(1, "km"), 1000, 1, "m") ==
with_unit(1000, "m")` establish, and why must the factor appear in
the call?
4. What do the two boundaries `tag resolves` tests prove that the SI
tests do not?
5. What does `law engine check` report for the `temp02` snippet, with
which two codes — and what must a 0.2 modeller use instead?
Write down each prediction first; run the commands; explain any miss
in one sentence. Check your work against the
[full solution: melded scalars, conversions, tags and refusal codes](/tutorials/northbridge/solutions/nb-15-solutions/).
## Sources
- Source: `packs/examples/language-demo/math02/package.law` (rules
`LoadScalar`, `HeavyLoad`, `VeryHeavy`, `TripLength`, `LongTrip`,
`LoadMax`, `ConvOk`, `QBackOk`, `ExpoOk`)
- Tests: `packs/examples/language-demo/math02/tests/math02.lawtest`
(42 tests, including the meld/scalar, conversion and clamp cases)
- Source: `packs/examples/language-demo/boundaries/package.law`
(unit/derived [§49.2](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#492-объявление-единиц-errata-e-0136-e-0150): `unit permit`, `permit_rate`, rules
`PermitTagged`, `RateTagged`)
- Refusals: `packs/examples/language-demo/boundaries/evidence/snippets/temp02.law.txt`
(`temp_convert`, 0.7), `angle02.law.txt` (`angle_convert`, 0.7)
- Suite tour: `packs/examples/language-demo/README.md`
- 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-16: Exact computation and proven bounds](/tutorials/northbridge/nb-16-exact-bounds/)
Three levels:
1. **Northbridge use** (this article): the depot scale reduces every
reading to a scalar in a named unit before any threshold applies
— 5 km melds to 5000 and counts as heavy and long, while 22 kW
leaves `heavy_load()` NEITHER with no melded scalar pinned by the
suite (see Changed condition) — verified by the 42/42 math02 suite
header and the named ok lines above.
2. **Domain template:** whenever a regime gates on measured values,
keep number and unit glued until the last step; convert with an
explicit target and factor; compute the scalar in one rule and
judge it in another so several thresholds share one meld; declare
local tags for countable non-physical things. Never compare a raw
number against a threshold that has a unit.
3. **Confirmed example elsewhere:** the boundaries package replays
the same `with_unit` mechanism over locally declared tags
(`permit`, `permit_rate`) — the 21/21 suite with both `tag
resolves` lines green — proving tag resolution is a property of
the construct, not of the SI registry. And the frozen
`temp02`/`angle02` refusal slices prove the same boundary from the
other side: converters outside the 0.2 subset are refused loudly
at check time rather than approximated silently.
4. **Confirmed external formalization (corpus):** GloBE Pillar Two
thresholds and entity summary (OECD, international) — package
`oecd.globe_etr`,
`corpus/laws/org/oecd/globe-etr/package.law:45-52`: three act
thresholds as argument-free functions — the rate is `Decimal`,
the thresholds are `Money` of the same kind as the compared sums
(comparison requires kind agreement) — with the charge aggregate
below as `sum all amount: Money for ce ...`, always `collect
all`, never `collect`. Evidence:
`docs/research/constructs/21-expressions-quantities/corpus-forms.en.md`
[§2](/tutorials/northbridge/nb-01-first-permit/#2-prerequisites) (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.