Markdown for LLMs
nb-15 solutions — Quantities and dimensions
The source Markdown for this article. Copy it into your assistant or download it as a text file.
# nb-15 solutions — Quantities and dimensions *Checkable against `law test packs/examples/language-demo/math02` (42 checked, 42 passed), `law test packs/examples/language-demo/boundaries` (21 checked, 21 passed), `law engine check` on the math02 package and on the frozen refusal snippets. Identifiers and code as written.* ## 1. `load_q(5 km)` versus `load_q(22 kW)` for `heavy_load()` **Answer: 5 km gives TRUE_ONLY (melded scalar `5000/1`); 22 kW gives NEITHER — no scalar is melded at all.** `LoadScalar` divides each reading's magnitude by `magnitude(1 m)` and applies `scalar_of`: 5 km becomes the Rational `5000/1`, which clears the `(44/1)` bar in `HeavyLoad` — the rule fires. For 22 kW the suite shows `heavy_load()` NEITHER but pins no `load_scalar` value itself; a scratch probe outside the suite settles it — `truth(load_scalar(22/1))` given `load_q(22 kW)` returns NEITHER while `load_q(22 m)` returns TRUE_ONLY — so the metre-divisor meld accepted nothing (the silent `UNIT_UNKNOWN` mode from the article's Limits). No rule derives `heavy_load()` and the status is NEITHER, not false. The suite's test names say exactly this: `scalar of five kilometres in metres` versus `load scalar below the threshold is not derived`. ## 2. `load_q(5 km)` versus `load_q(0.5 km)` for `long_trip()` **Answer: 5 km clears it (5000 m ≥ 1000); 0.5 km does not (500 m < 1000). The explicit step is `unit_convert(magnitude(q), "m")` in `TripLength`.** The target unit `"m"` is written in the call — kilometres never meet the metre threshold until converted. 5 km converts to 5000 m (`kilometres converted to metres`, TRUE_ONLY); 0.5 km converts to 500 m (`short trip fails the threshold`, NEITHER). The judging rule `LongTrip` is identical in both cases; only the converted scalar differs. ## 3. The `convert` equality and its explicit factor **Answer: it establishes `conv_ok()` (TRUE_ONLY) — 1 km equals 1000 m — and the factor 1000/1 must appear because the engine performs no silent coercion.** `convert(with_unit(1, "km"), 1000, 1, "m")` re-expresses the value with a stated numerator and denominator; the equality against `with_unit(1000, "m")` then checks two explicitly constructed quantities. A bare `1 == 1000` comparison would be meaningless (and dimensionless); the factor in the call is what makes the claim checkable rather than assumed. Suite witness: the `unit conversion by value` ok line. ## 4. What the `tag resolves` tests add **Answer: they prove tag resolution works for locally declared units, not just the SI registry.** `declared unit tag resolves` (`with_unit(5, "permit")`) and `derived tag resolves` (`with_unit(2, "permit_rate")`, where `permit_rate = permit / permit`) run over `unit permit = 1` declared in the boundaries package itself — no SI import involved. The SI-side tests prove registry conversion; these two prove the construct is general: any package can coin countable tags for non-physical things (permits, rates) and compare them the same way. ## 5. The `temp02` refusal and the 0.2 alternative **Answer: refused with `LDC-E2105` (undeclared) plus `LDC-E2403` (computability not proved); a 0.2 modeller uses `unit_convert`, `convert`, `quantity_of` and `with_unit`.** `temp_convert` belongs to the 0.7 temperature profile, which this implementation (`law 0.1.0`, `law.core/0.2`) does not execute — so the checker reports the name unknown and the purity unprovable. `angle_convert` fails identically. The refusal is a fact about this profile, not about the language: stay inside the executable subset (the `ConvOk`/`QBackOk`/`ExpoOk` rules are the positive pattern) and leave newer-profile converters to nb-17. ## How to verify ```sh law test packs/examples/language-demo/math02 ``` Expected: `мир demo.northbridge.math02, units.si`, ok lines for `scalar of five kilometres in metres`, `load scalar below the threshold is not derived`, `kilometres converted to metres`, `short trip fails the threshold`, `unit conversion by value`; total `42 проверено, 42 прошли, 0 не прошли`. ```sh law test packs/examples/language-demo/boundaries ``` Expected: ok lines `declared unit tag resolves` and `derived tag resolves`; total `21 проверено, 21 прошли, 0 не прошли`. ```sh law engine check packs/examples/language-demo/math02/package.law ``` Expected: `check OK`. ```sh law engine check packs/examples/language-demo/boundaries/evidence/snippets/temp02.law.txt ``` Expected: `LDC-E2105` and `LDC-E2403` (likewise for `angle02.law.txt` with `angle_convert`).