Skip to content
docs
Arxo ↗

nb-17 — Numeric families and support boundaries

For LLMs10 sections
← Course mapChapter 17 / 25 · Mathematics branch

Northbridge course, math branch (needs beginner only: nb-01: First permit: facts, a rule and a question → nb-04: The permit fee). All law is fictional; every resident, report, invoice and certificate is synthetic and unofficial. No real municipal deployment or legal-validity claims. Tool law 0.1.0, language version 0.2, semantics law.core/0.2, std 0.2.0 (from law --version, quoted below).

Situation

Section titled “Situation”

Mira, the Northbridge permits clerk, receives two numbers she is asked to certify. A footbridge inspection report states that a load factor stays inside a proven square-root bound. A foreign contractor submits an invoice in USD and asks the office to convert it to KZT at the day rate, and a second contractor asks the office to solve a tariff equation for him. The auditor’s question is blunt: which of these numbers can our pinned machine prove, and which must it refuse — and is each refusal a property of our build or of the language itself?

You will run the certified calls the pinned build does prove, then watch it refuse the rest — each refusal naming the exact layer that rejected it. The answer is never “the language cannot do this”; it is always “this build, at this layer, for this version.” Each new term is introduced where it is first used.

Prerequisites

Section titled “Prerequisites”

nb-01: First permit: facts, a rule and a question: facts, strict rules, the four 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: Money arithmetic and rounding — the everyday numbers this article contrasts with the gated families.

New here: certified bounds calls that execute only with an explicit profile argument, names outside the 0.2 support list, and three refusal codes at three different layers — each introduced where it first appears below.

Minimal example

Section titled “Minimal example”

Excerpts 1–2 are from packs/examples/language-demo/math02/package.law (identifiers as written; relations, imports and unrelated rules cut). Standalones A–C are complete probe files from packs/examples/language-demo/boundaries/evidence/snippets/ (checked with law engine check; the .law.txt suffix only keeps the package scanner from picking them up).

Excerpt 1 — self-determinism under one profile (lines 172–175). A rule that compares a certified root bound with itself.

Arxo Law
rule SqrtSelf strict {
    when sqrt_bounds(4, "p8/0.1") == sqrt_bounds(4, "p8/0.1");
    then sqrt_self();
}

Look at the when line: the same certified call (sqrt_bounds(4, "p8/0.1")) on both sides of ==. The quoted "p8/0.1" is the cert profile — the name of the exact proven certificate the result carries. A derivation is the recorded history of how a value was computed; the same derivation under the same certificate is equal to itself, and this self-equality is what 0.2 guarantees.

Excerpt 2 — the same call under two profiles (lines 186–189). Only the profile name changes.

Arxo Law
rule CertCross strict {
    when sin_bounds(0, "p8/0.1") == sin_bounds(0, "p16/0.1");
    then cert_cross();
}

Look at what changed: only the right-hand profile, "p8/0.1" → "p16/0.1". The profile name is part of the derivation’s history — so a different certificate means a different derivation, and the equality does not hold. The suite expects NEITHER for this rule.

Standalone A — full content of sqrt02.law.txt: exact root without a certificate, in language 0.2.

Arxo Law
language "law.core" version "0.2";
package probe version "0.1.0";
namespace "urn:probe";
function f(x: Rational) -> Rational = exact_sqrt(x);

Look at the last line: a bare exact_sqrt with no profile. The name is simply not in the 0.2 support list, so the file is refused with two codes, not executed. This tiny frozen probe is a refusal slice: its only job is to show one boundary loudly. It is checked, never executed.

Standalone B — full content of solve02.law.txt: a solver call, same shape, same fate.

Arxo Law
language "law.core" version "0.2";
package probe version "0.1.0";
namespace "urn:probe";
function f(x: Rational) -> Rational = solve_linear(x, 1);

Look at the last line again: same four-line shape, different forbidden name. Solver terms (solve_linear, the 0.6 family) and the Number answer domain (0.4) live behind the same boundary as exact algebra — refused in this profile.

Standalone C — full content of v04.law.txt: a newer language version than the tool implements.

Arxo Law
language "law.core" version "0.4";
package probe version "0.1.0";
namespace "urn:probe";
relation r(x: Integer) kind empirical;

Look at the first line: the header declares language 0.4. The refusal happens at the version layer, before any name is even looked up — the content below the header is never examined.

Command and result

Section titled “Command and result”

The tool, language and semantics versions are five separate facts, and every refusal below names exactly one of them. The tool version is what is installed; the language version is what the file header declares; the exact semantics is the law.core/0.2 revision plus the std release; implementation support is the std v1-list of declared names plus effect descriptors; the observed run is what the commands below printed:

Terminal
law --version

Observed:

Output
law 0.1.0
семантика: law.core/0.2
std для языка 0.2: 0.2.0

The Russian lines pin the semantics (семантика: law.core/0.2) and the std release for language 0.2 (std для языка 0.2: 0.2.0). A numeric family is a group of number-like types and functions that are versioned and supported together — integers and rationals in one family, certified real functions in another, solvers and conversions in further ones. The executable side — every family 0.2 supports — is green:

Terminal
law test packs/examples/language-demo/math02

Observed (last lines; engine law 0.1.0):

Output
  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 (итого: 42 проверено, 42 прошли, 0 не прошли, 0 не исполнены; код 0 — 42 checked, 42 passed, 0 failed, 0 unexecuted, exit code 0). The neighbouring boundaries package is green too:

Terminal
law test packs/examples/language-demo/boundaries

Observed: итого: 21 проверено, 21 прошли, 0 не прошли, 0 не исполнены; код 0 — 21 checked, 21 passed, 0 failed, 0 unexecuted, exit code 0.

Output
итого: 21 проверено, 21 прошли, 0 не прошли, 0 не исполнены; код 0

Both suites passing means every supported call behaved as declared. Now the refusals, each naming its layer. The version refusal first:

Terminal
law engine check packs/examples/language-demo/boundaries/evidence/snippets/v04.law.txt

Observed: error LDC-E1401: версия языка "0.4" не поддерживается (“language version 0.4 is not supported”), followed by the migration report (§266.1: 0.1 [withdrawn], 0.2 [supported], revisions 0.2.1–0.2.4). The machine refuses the version, not the content: this build reads 0.2 and will not read 0.4 headers at all.

The exact-algebra refusal carries two codes at once:

Terminal
law engine check packs/examples/language-demo/boundaries/evidence/snippets/sqrt02.law.txt

Observed, in full — two codes, hence two layers rejected the file:

Output
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 first code (LDC-E2403) says the function is not proved PURE_DETERMINISTIC — the call has no available effect descriptor. The second (LDC-E2105) says the name is not declared, neither in the file nor in the std v1-list. Support and semantics each said no.

The solver refusal is the identical pair for a different name:

Terminal
law engine check packs/examples/language-demo/boundaries/evidence/snippets/solve02.law.txt

Observed: error LDC-E2403 ... вызов "solve_linear" не имеет доступного effect descriptor ... (“the call has no available effect descriptor”) plus error LDC-E2105: функция "solve_linear" не объявлена (ни в файле, ни в std v1-списке) (“the function is not declared, neither in the file nor in the std v1-list”). fx_convert, pi, temp_convert, angle_convert and ln2 report the same pair (verified per snippet); a query used as a term (query02.law.txt) reports E2105 alone — one layer, not two (see nb-14: Why this answer and what would change it).

Why this construct

Section titled “Why this construct”

Mira’s auditor question — which numbers can the pinned machine prove? — is answered by knowing the usable surface without guessing. Integers, Rationals, Decimals, Money, Quantities, date/time spans, HALF_UP rounding, unit_convert with the pinned units.si, and certified bounds calls with an explicit profile all execute — 42 of 42 in the suite above.

Read "p8/0.1" as a certificate identity, not a precision wish. SqrtSelf (same derivation, same profile) is TRUE_ONLY; SqrtX (sqrt_bounds(4, "p8/0.1") == bounds_const(2, 1), lines 167–170 of the package) is NEITHER. A foreign derivation is never equal, however plausible its digits look.

Cross-profile equality fails to keep parallel certificates apart. CertCross (p8 vs p16) is NEITHER with COMPUTED: both sides computed, and the comparison honestly reports inequality of derivations. The mirror image — any profile equals itself — replays with the p32 probe in Changed condition below (TRUE_ONLY, 43 of 43).

Each refusal sits at its layer. E2105 (not declared in the file or the std v1-list) is an implementation-support fact; E2403 (computability not proved, no effect descriptor) is an exact semantics fact. Both gates must pass, and the probes fail both. query02 fails only the first gate, which is why it carries one code instead of two.

The version refusal separates the tool from the language. E1401 says tool law 0.1.0 implements no 0.4 semantics; the attached migration report names the supported branch (0.2, revisions 0.2.1–0.2.4). It never says 0.4 content is meaningless — only that this build will not read it.

Why not hand-written digits or a bare exact call?

Hand-writing the digits (bounds_const(2, 1) where the root belongs) looks equal and is not — the suite keeps BoundsOk/SqrtX at NEITHER precisely to catch that substitution. Reading a bare exact_sqrt where a certified call belongs is caught louder, at check time.

The evidence is the 42/42 and 21/21 suites, the TRUE_ONLY / NEITHER / NEITHER triple (sqrt_self, sqrt_x, cert_cross), and the five quoted refusal outputs — each executed above, none asserted in prose. What is not proven is that any certificate is mathematically correct, or that p16 is “better” than p8. The machine proves which comparisons hold under which certificate; choosing a profile for a real bridge report is engineering judgment, and Northbridge’s bridge is fiction.

Changed condition

Section titled “Changed condition”

SqrtSelf derives sqrt_self() as TRUE_ONLY — the identical call with the identical profile on both sides. Change exactly one token, the right-hand profile "p8/0.1" → "p16/0.1" (CertCross), and the same shape of question becomes NEITHER: both bounds computed (COMPUTED), the equality of derivations gone. Change the profile consistently on both sides instead and the status returns to TRUE_ONLY. One name changed asymmetrically flips the answer; changed symmetrically it changes nothing — because equality here compares derivations, not digits.

Replay recipe (standalone scratch copy; the repo suite is untouched):

Terminal
cp -r packs/examples/language-demo/math02 /tmp/nb17-p32

Append after SqrtSelf in /tmp/nb17-p32/package.law:

Arxo Law
relation sqrt_self32() kind institutional;


rule SqrtSelf32 strict {
    when sqrt_bounds(4, "p32/0.1") == sqrt_bounds(4, "p32/0.1");
    then sqrt_self32();
}

Add /tmp/nb17-p32/tests/p32.lawtest:

Arxo Law
language "law.core" version "0.2";
package demo.northbridge.math02 version "0.1.0";
namespace "urn:law:demo:northbridge:math02";


test "p32 self equals itself" {
    given {
        context { legal_time @2026-03-01; decision_time @2026-03-01T09:00:00Z; knowledge_time @2026-03-01T09:00:00Z; timezone "UTC"; }
    }
    evaluate truth(sqrt_self32());
    expect truth_status == TRUE_ONLY;
}

Register tests/p32.lawtest in /tmp/nb17-p32/law.toml suites and run:

Terminal
law test /tmp/nb17-p32

Observed: p32 self equals itself ok, 43 проверено, 43 прошли, 0 не прошли — 43 checked, 43 passed, 0 failed. The fresh profile behaves exactly like p8: equal to itself, silent toward others.

Typical mistake

Section titled “Typical mistake”

The mistake is asserting a certified result against a hand-written constant:

Excerpt — SqrtX from packs/examples/language-demo/math02/package.law lines 167–170 (the rule is real; the mistake is the author’s TRUE_ONLY expectation).

Arxo Law
rule SqrtX strict {
    when sqrt_bounds(4, "p8/0.1") == bounds_const(2, 1);
    then sqrt_x();
}

The author reads “root of four is two” and expects TRUE_ONLY. The observed consequence (bounds root: foreign derivation is unequal) is truth_status == NEITHER. The constant on the right carries a different derivation from the certified call on the left, so the comparison fails — determinism (BoundsSame, SqrtSelf, DivSelf: identical expression against itself, all TRUE_ONLY) is the only equality the bounds surface offers.

The fix: never compare a certified call with anything except the textually identical call. If the digits must appear, recompute them through the same call on both sides.

Limits

Section titled “Limits”

Every status above holds for the verified profile only: tool law 0.1.0, language 0.2, semantics law.core/0.2, std 0.2.0. Newer tool builds, other language versions and other std releases have their own support lists; re-run, do not assume.

Refusals are profile facts. E1401/E2105/E2403 describe this build’s version support, std v1-list and effect descriptors. None states that Number, Algebraic, RealExpr, solvers or conversions are inexpressible in general — the audit records all three families as normative_boundary.

Certificates pin identity, not truth. A TRUE_ONLY on sqrt_self() certifies that one derivation equals itself, not that the certificate’s mathematics is right.

One observed extra boundary: a query declaration used as a term is refused with E2105 alone (nb-14: Why this answer and what would change it) — same code, one layer, no computability complaint.

Exercise

Section titled “Exercise”

Without running the engine, predict, then check with the commands above:

  1. sqrt_self() versus sqrt_x(): which truth status each, and what distinguishes the two comparisons?
  2. cert_cross() (p8 vs p16): which truth status, which evaluation status, and what does that pair mean?
  3. law engine check over sqrt02.law.txt: which two codes, in which order, and which layer (version / support / semantics) does each name?
  4. law engine check over v04.law.txt: which code, and does it claim anything about the 0.4 language in general?
  5. fx_convert (fx02.law.txt) and DoubleIt-in-condition (query02.law.txt): which codes each, and what would have to change — and at which of the five version layers — before either could execute?

Write down each prediction first; run the commands; explain any miss in one sentence. Check your work against the full solution: self-equality, cross-profile silence and refusal layers.

Sources

Section titled “Sources”
  • Source: packs/examples/language-demo/math02/package.law (certified rules SqrtX, SqrtSelf, CertAll, CertCross, rounding RoundHalf, unit rules ConvOk, QBackOk, ExpoOk)
  • Tests: packs/examples/language-demo/math02/tests/math02.lawtest (42 tests: spans, bounds, aggregates, derivation-sensitive comparisons, determinism probes)
  • Refusal slices: packs/examples/language-demo/boundaries/evidence/snippets/v04.law.txt (E1401), sqrt02.law.txt, solve02.law.txt, fx02.law.txt, pi02.law.txt, ln02.law.txt, temp02.law.txt, angle02.law.txt (E2105 + E2403), query02.law.txt (E2105 alone); frozen outputs evidence/ev-*.txt
  • Audit: packs/examples/language-demo/matrix-audit-P11.json (types: Number, Algebraic, RealExpr — normative_boundary)
  • Suite tour: packs/examples/language-demo/README.md (math02 §, boundaries § with the full frozen-refusal table)
  • Prerequisite: nb-01: First permit: facts, a rule and a question, nb-04: The permit fee; next: nb-15: Quantities and dimensions

Three levels:

  1. Northbridge use (this article): the clerk certifies only what the pinned build proves — self-identical certified bounds (TRUE_ONLY), honest silence on cross-profile and foreign-derivation comparisons (NEITHER), and loud, layer-named refusals for solvers, conversions and newer versions — verified by the 42/42 plus 21/21 suites and the quoted E1401 / E2105 + E2403 outputs above.
  2. Domain template: whenever a regime gates numeric methods by version, separate the five layers (tool, language, exact semantics, implementation support, observed run); execute only under explicit certificate profiles; compare certified values solely with textually identical calls; freeze every refusal as a replayable slice with its codes; never read a profile refusal as a language-wide inability.
  3. Confirmed example elsewhere: the same E2105 + E2403 pair fires for seven unrelated names (exact_sqrt, solve_linear, fx_convert, pi, ln2, temp_convert, angle_convert) and E1401 for the 0.4 header — the boundary machinery is uniform across families, per the boundaries README table and the frozen ev-*.txt exhibits, not a quirk of one square root.
  4. Confirmed external formalization (corpus): VIN check digit via Euclidean remainder (US, 49 CFR) — package us.cfr.vin, corpus/laws/us/vin/02-check-digit.law:282-287: then vin_check_remainder(vin, total mod 11) — the remainder is taken of a whole total as Integer mod Integer (0 <= r < |b| for any signs), never of an inexact magnitude (Decimal has no remainder). A family boundary in live law: this computation belongs to the Integer family and is refused elsewhere. Evidence: docs/research/constructs/21-expressions-quantities/corpus-forms.en.md §9 (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.

Documentation for Arxo. Writings — blog.arxo.io.

Anonymous visit counts on stats.arxo.io, no cookies.