Markdown for LLMs

nb-16 solutions — 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 solutions — Exact computation and proven bounds

*Checkable against `law test packs/examples/language-demo/math02`
(42 checked, 42 passed). Identifiers and code as written.*

## 1. `load_scalar(5/1)` given `load_q(5 m)` — status, and why fraction form?

**Answer: TRUE_ONLY. The fraction form is the exact value, not a
terminating-decimal approximation.**

`LoadScalar` computes `scalar_of(magnitude(5 m) / magnitude(1 m))`, which
is exactly the rational `5/1`. The test `exact scalar value (5 m)` asks
`truth(load_scalar(5/1))` and expects TRUE_ONLY. Writing `5.0` would ask
about a `Decimal` literal — a different value family — while `(5/1)`-form
Rational literals are the exact, irreducible-fraction serialization the
rule actually derives.

## 2. `heavy_load()` given `load_q(22 kW)` — status? Which condition fails?

**Answer: NEITHER. No `load_scalar` is derived at all, so the
`load_scalar(v)` premise of `HeavyLoad` never matches and the threshold
comparison is never reached.**

The metre-divisor meld accepts nothing for a kW reading: scratch probes
on a temporary copy of the package (2026-10-03, repo untouched) return
NEITHER for `truth(load_scalar(22/1))` given `load_q(22 kW)`, and
`heavy_load()` is NEITHER even for `load_q(120 kW)` — while the
controls `load_q(5 m)` → `load_scalar(5/1)` and `load_q(22 m)` →
`load_scalar(22/1)` both give TRUE_ONLY. This is the test `load scalar
below the threshold is not derived`: the fact is present, but the head
computation derives nothing — silence (NEITHER), not refusal, exactly
as in nb-02.

## 3. `bounds_same()` — status? What about `bounds_ok()`, and what differs?

**Answer: TRUE_ONLY. `bounds_ok()` for the same arithmetic is NEITHER.
The single differing property is derivation identity.**

Both sides compute `[5/6, 5/6]`, but `bounds_same` compares the
`bounds_add(...)` call against itself (one shared derivation), while
`bounds_ok` compares it against the separately written literal
`bounds_const(5, 6)` (a foreign derivation). `==` on bounds checks the
derivation as well as the endpoints, so identical arithmetic gives
opposite verdicts. The tests `determinism: the same addition equals
itself` (TRUE_ONLY) and `bounds carry derivation: foreign derivation is
unequal` (NEITHER) pin the pair.

## 4. `cert_cross()` — status? What does it say about the profile?

**Answer: NEITHER. The precision profile is part of the derivation.**

`cert_cross` compares `sin_bounds(0, "p8/0.1")` against
`sin_bounds(0, "p16/0.1")`: same function, same argument, different
certified precision profiles — and the comparison stays NEITHER (`foreign
profile is unequal`). Against itself each profile is deterministic
(`certified functions are deterministic`: TRUE_ONLY). So a certified
bounds value is identified by (function, argument, profile) together;
changing any of the three yields a foreign derivation.

## How to verify

```sh
law test packs/examples/language-demo/math02
```

Expected: `итого: 42 проверено, 42 прошли, 0 не прошли, 0 не исполнены`.
The deciding tests are `exact scalar value (5 m)` (`load_scalar(5/1)`
TRUE_ONLY), `load scalar below the threshold is not derived`
(`heavy_load()` NEITHER for `22 kW`), `determinism: the same addition
equals itself` (TRUE_ONLY) against `bounds carry derivation: foreign
derivation is unequal` (NEITHER), and `foreign profile is unequal`
(NEITHER) against `certified functions are deterministic` (TRUE_ONLY).