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?
Section titled “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?
Section titled “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?
Section titled “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?
Section titled “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
Section titled “How to verify”law test packs/examples/language-demo/math02Expected: итого: 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).
Documentation for Arxo. Writings — blog.arxo.io.
Anonymous visit counts on stats.arxo.io, no cookies.