What would have to be true.

Backward chaining answers *is this provable?*  Abduction answers the complementary
question — *what would have to be true for it to be provable?* — and mints the answer
as a **hypothesis**: an ordinary premise, in a context of its own, at `:default`
strength, assumed rather than derived.

The hard parts of abduction are containment, arbitration and cleanup, and this engine
already had all three, built for other reasons:

- **Containment is the context lattice.**  A hypothesis goes into a fresh microtheory
  hung *below* the asking context, so it sees everything the question could see and
  nothing that existed before it can see the hypothesis.  A shipped rule firing over a
  hypothesis places its conclusion **in** that microtheory, because placement is the
  maximal common descendant (docs/contexts.md) — so the consequences land inside the
  thing that gets discarded, with nothing arranging for it.  That is the sandbox's
  shape (`vaelii.impl.sandbox`), for the same reason.
- **Arbitration is strengths.**  A hypothesis is asserted `:default`, so it is
  defeasible by construction: a `:monotonic` fact that contradicts it wins through the
  ordinary defeat path, with no abduction-specific rule anywhere.
- **Cleanup is retraction.**  A hypothesis is a premise, so `retract!` and the
  dependency-directed sweep remove it and everything it supported.

So the new code here is the **search** — finding the dead end and deciding what may be
assumed — and not the belief plumbing.

Two things the caller is owed, and they are the contract:

1. **An ignored `abduce` leaves the KB as it found it.**  The lifecycle tears the
   context down before returning unless `:keep?` says otherwise, and it tears it down
   on the way out of an exception too.
2. **Every answer names its assumptions.**  Solutions come back beside the hypothesis
   set that licensed them, never as if they had been proved.  An empty `:hypotheses` is
   the claim that nothing was assumed.

See docs/abduction.md.

How a *read* client reaches a KB — directly in-process, or over the daemon HTTP API
(`vaelii.impl.serve`).  It re-exports the slice of the `vaelii.core` read surface the
browser uses, so the browser is written once against these names and runs unchanged
against a local KB or a remote daemon.

A **target** is either a real KB (treated as local) or an access value from `local` /
`remote`.  A KB-read op dispatches on it:

  :remote  → the client (`vaelii.impl.client/call`) — one HTTP round-trip
  :local   → `vaelii.core`, via `serve/ops` (the very allowlist the daemon serves, so
             local and remote answer through the same table and cannot drift)
  a raw KB → the same local path (so a caller holding a plain KB needs no wrapper)

The pure display fns (`term-role`, `reified-term?`, `readable-sentence`,
`indexable-terms`, `levels`)
and the bootstrap fns (`open-kb`, `clear!`) take no target and just delegate to
`vaelii.core` — they are here only so a caller can require this one namespace and
reach the whole surface it needs.

Reads — including `check` / `check-edit`, which answer what `assert` would refuse
and write nothing — plus the three writes the browser performs: `edit` (an
assert/retract batch in one settle), `forward-chain`, and `preview` (which stores
nothing but applies a batch and rolls it back, so it holds the single writer).  A remote result is already
EDN-clean (the daemon projects sentex records to maps); a local result is the raw
record, and both answer to the same keys, so a caller handles them identically.

Pure ASPIF text emitter. No vaelii deps, no I/O.

ASPIF is the Potassco Answer Set Programming Intermediate Format, the
ground-program protocol between gringo and clasp. We emit the full set
of ground statement types: facts, normal rules, single- and multi-head
choice atoms/rules, disjunctive heads, integrity constraints,
weight/cardinality bodies, minimize (weak constraints), show output,
projection (type 3), externals (type 5), assumptions (type 6),
heuristics (type 7), and acyclicity edges (type 8).

Wire format (line-oriented, space-separated):
  Line 1: `asp 1 0 0`
  Rule:     1 <head_type> <head_size> <head...> <body_type> <body_size> <lits...>
              head_type = 0 disjunctive | 1 choice
              head_size may exceed 1 (disjunction `a|b`, choice `{a;b;c}`)
              body_type = 0 normal (list of signed literals)
                         = 1 weight body — see below
              body literal: +atom for positive, -atom for default-negated
  Weight rule:
            1 <head_type> <head_size> <head...> 1 <lower_bound> <body_size>
                                               <lit_1> <w_1> ... <lit_n> <w_n>
              head fires when the sum of weights of satisfied body
              literals is at least <lower_bound>. Cardinality is
              the all-weights-equal-1 special case.
  Minimize: 2 <priority> <n> <lit_1> <w_1> ... <lit_n> <w_n>
  Project:  3 <n> <atoms...>
  Output:   4 <str_len> <str> <n_conditions> <atoms...>
  External: 5 <atom> <init>   init = 0 free | 1 true | 2 false | 3 release
  Assume:   6 <n> <signed_lits...>   (static assumption block)
  Heuristic:7 <modifier> <atom> <value> <priority> <body_size> <lits...>
              modifier = 0 level | 1 sign | 2 factor | 3 init | 4 true | 5 false
  Edge:     8 <u> <v> <body_size> <lits...>   (acyclicity edge u→v)
  End:      0

ASPIF has no native *bound* on a choice head (`lb {…} ub`); a bound is
expressed by putting weight-rule + integrity-constraint cardinality
enforcement beside a multi-head choice, the same way gringo does.

Atom ids are positive integers; 0 is the terminator and must not
appear as an atom. String lengths in show statements count bytes
(equal to character count for ASCII); non-ASCII names need UTF-8
byte counting which we do not currently handle.

The public API has two halves:

  (1) Statement constructors (`fact`, `choice`, `rule`, `choice-rule`,
      `constraint`, `minimize`, `show`) that return plain data maps.
      Data form is inspectable, easy to assemble programmatically,
      and trivial to unit-test.

  (2) `render` turns a sequence of statements into the full ASPIF
      text with header and terminator.

Bidirectional atom id table for ASPIF translation.

ASPIF atoms are positive integers; every entity referenced in the
emitted program — sentex or contradiction marker — needs a unique id.
Atom 0 is reserved as the ASPIF terminator and is never allocated.

The table maps three kinds of source values to atom ids, sharing a
single counter so ids are unique across kinds:

  (1) sentex ids — the :id field of a vaelii sentex record. These
      become the atoms the ASP solver reasons about.

  (2) contradiction descriptors — nested sentence-shaped Clojure
      values of the form
        (contradiction <head> :involved [[:sentex H1] [:sentex H2] …])
      where `<head>` is a sentence-shaped tag (e.g. `(negation S)`,
      `(disjointTypes ent t-a t-b)`, or a user-named head emitted by
      a grounding rule like `(wrongBulbCount 3 4)`) and `:involved`
      lists the sentex handles that participated. Atoms backed by
      contradiction descriptors get weight in the minimize statement;
      the solver avoids models in which they are true.

  (3) aux descriptors — auxiliary atoms used by translators (e.g. the
      `count ≥ N` heads of cardinality weight rules). They are
      distinct from contradictions: the minimize statement does not
      weight them, and clasp witnesses ignore them when reconstructing
      contradictions for callers.

Labels are short string identifiers that appear in clasp's witness
output; we read them back during result parsing to recover the
originating sentex or contradiction. Format:

  s<sentex-id>   — sentex-backed atoms
  c<atom-id>     — contradiction-backed atoms
  a<atom-id>     — aux-backed atoms

Using `s`/`c` prefixes keeps the two namespaces distinct even if a
sentex id happens to numerically match a contradiction atom id.

The table is a clojure.core/atom wrapping a plain map. Intern
operations use swap! for atomicity; lookups are pure derefs. All
intern operations are idempotent.

Subprocess wrapper around the clasp ASP solver.

Consumes ASPIF text on stdin, returns parsed results as Clojure maps.
clasp exit codes encode the solve outcome (10=sat, 20=unsat, 30=optimum,
bitmask combinations) and are NOT error codes — we rely on the JSON
`Result` field from `--outf=2` and only throw when clasp itself fails
to run or produces no parseable output.

The four modes match the user-facing reason API in vaelii.impl.asp.reason:
:label, :all-optima, :classify-true, :classify-supportable.

In-process ASP solver: a JNA binding to the native clingo C API (which
embeds clasp). Drop-in for `vaelii.impl.asp.clasp/solve` — same
`(solve aspif-text mode)` contract and return shape — but without the
subprocess + JSON round-trip.

Why in-process: it drops the per-solve fork and JSON round-trip the
subprocess pays, which is the whole win on the small programs
`vaelii.impl.asp.solver` routes here.

The four modes map to clingo configuration passed as command-line arguments
to clingo_control_new (clingo accepts clasp's flags): --opt-mode=optN so
brave/cautious enumerate over optimal models only, --enum-mode=brave|cautious,
--models=0|1. Shown atoms come back as the s/c/a label strings vaelii emits
via ASPIF type-4 show statements; the lexicographic cost vector comes from
clingo_model_cost.

Native lib: a system libclingo (brew install clingo) reachable via
jna.library.path, or an absolute path in -Dvaelii.clingo.lib. Crash isolation
is lost vs the subprocess — every native return is checked and every Control
is freed in a finally; a malformed program throws rather than segfaults.

v :- a_h1, a_h2, ...

:- a_h1, a_h2, ...

The real ASP backend behind `vaelii.impl.solve/Solver` — the edge solver.

`solve.clj` describes *what* an edge solve is: most of the KB is monotonic or
default-true with no conflict, so only the contested defeasible nodes are sent,
known-true content is fixed background, and contradictions are soft and
prioritized so a solve never fails.  This namespace renders that `Program` to
ASPIF and reads an answer set back.

## The encoding

Each contested assumption is a **choice atom**: true means believed, false means
defeated.  Known-true (`:fixed`) members of a contradiction are *not* atoms —
they hold by assumption, which is exactly what makes them background.

A contradiction `#{h1 h2 ...}` becomes a violation atom derived from its
contested members:

    v :- a_h1, a_h2, ...

and a **weak** constraint minimizing `v`.  Weak rather than hard is the whole
point: an unsatisfiable contradiction costs, it does not make the program UNSAT,
so it comes back in `:violated` instead of throwing.

A nogood carrying `:hard true` (a `set/hardConstraint` rule ground by
`solve-context`) is instead a **hard integrity constraint**

    :- a_h1, a_h2, ...

with no violation atom and no minimize term: a model satisfying its whole body is
excluded outright.  That is what makes graph 3-coloring plain satisfaction rather
than optimality-proving over soft violations — an adjacency clash is never
tradeable.  Soft nogoods (the default) keep the minimize path above.

In practice `:violated` comes back empty, and that is correct rather than a gap.
An irreducible known-true clash never reaches a solver: `core/settle`'s
`decide-nogood` classifies it as *hard* and reports it directly, and
`solve/program` drops any nogood with no contested member.  What does arrive
always has a contested member, and defeating that member always satisfies it.
The `:doomed` path below is therefore defensive — it costs nothing and stays
correct if nogoods ever grow beyond today's `S` vs `(not S)` pairs.

## The objective, most significant first

Higher ASPIF minimize priorities dominate lower ones, so the levels are:

| level | minimizes | why |
|---|---|---|
| `2 + rank(p)` | violation atoms | satisfy contradictions, caller priority first |
| `1` | defeated assumptions | give up as little belief as possible |
| `0` | a content-keyed weight | break remaining ties *stably* |

Caller priorities are mapped through their ascending rank rather than used as
levels directly, so any integers work and none can collide with the two levels
below.

## Determinism

A tie between equally-good answer sets has no principled winner, but it must not
depend on assertion order — the engine-wide invariant in docs/nmtms.md.  Atom ids
are allocated in `solve/content-key` order, and level 0 weights defeating the
greatest content-key most cheaply, mirroring the stub's choice.  Same knowledge
in any order, same answer set.

## Availability

`edge-solver` degrades rather than fails: with no clingo and no clasp reachable
it delegates to `solve/local-solver`, so installing it is always safe.

:true        ⊆ believed        (cautious holds in the committed model)
:false       ∩ believed = ∅    (excluded holds in no model, including that one)
:supportable — either way, by definition

Brave/cautious classification of a settled tie, and materializing one labeling as
a specialization context.

## What this adds over `in?`

The TMS answers *what do I believe*. After `settle` arbitrates a default/default
tie, one side is IN and the other OUT — but that answer flattens two very different
situations. A belief can be IN because every consistent way of resolving the
contradictions keeps it, or because the solver had two equally good options and
picked one. `in?` cannot tell them apart; both read as "believed".

Brave/cautious classification separates them by asking the solver for *all* optimal
answer sets rather than one:

| class | in every optimum | in some optimum | meaning |
|---|---|---|---|
| `:true` | yes | yes | forced — no consistent labeling gives it up |
| `:supportable` | no | yes | arbitrary — the current belief is one of several |
| `:false` | no | no | excluded — no consistent labeling holds it |

`:supportable` is the interesting one, and it is invisible from the TMS alone. In a
Nixon diamond both sides are `:supportable`: whichever the TMS committed to, the
other was equally available.

## Concert with the TMS

Two rules keep these from drifting apart from belief.

**Classification reads the recorded program, never a recomputed one.** Resolving a
tie erases its own evidence — the defeated side stops matching, so the nogood is no
longer derivable from the KB. `core/last-program` holds what the solver was
actually asked (see the KB record).

**Labeling reads the TMS, not a fresh solve.** `label-context` materializes the
labeling the engine *committed to*, taken from `jtms/in?`, rather than re-solving
and hoping for the same answer set back. A re-solve would usually agree, and
"usually" is not a property worth building on.

So the invariants hold by construction, and `asp_label_test` pins them:

    :true        ⊆ believed        (cautious holds in the committed model)
    :false       ∩ believed = ∅    (excluded holds in no model, including that one)
    :supportable — either way, by definition

## Requirements

Classification needs a real ASP backend; `local-solver` produces one labeling and
cannot enumerate optima. With no backend reachable, `classify` reports every
contested assumption as `:supportable` — honest (each *is* one of several options)
and never overclaims `:true`.

Solving as a **persistent, inert** artifact: `assumptionRules` define choices, a
solve grounds them (scoped to a base context), enumerates the optimal answer sets,
and materializes **each one as its own labeling context** — a `genlContext` child of
the base holding the chosen truth values as inert sentexes.  `classify` then gathers
brave/cautious over those labelings.

The two imperatives `(do/label Base Into)` and `(do/classify Into)` route here.

## Why inert, and why per-answer-set

Belief in this KB is global (one JTMS, not an ATMS): a *believed* `(not head)` in a
context that sees the base would defeat the base's `head` everywhere — so only one
labeling could ever exist (the `do/labeling` global-commit).  Materializing the truth
values **inert** (`core/assert-inert` — stored and indexed but not a JTMS premise)
sidesteps that entirely: an inert sentex is never IN, so it is invisible to the
belief-filtered nogood scan, forms no contradiction, and moves no belief.  Every
answer set therefore coexists as its own context, the base KB is untouched, and the
result **persists in the records** for inspection.

## What persists, and what does not

The **answer** persists: the labeling contexts and the classification, as inert
sentexes in the records.  The **grounding** — the menu of candidate choice heads —
never does.  A grounding is derived solver working state, recomputable from the
assumptionRules and the base's believed facts; an inert copy would carry no
justification linking it back to what produced it, so it would rot silently the
moment the base moved.  The Program keys on program-local ids (see `build`), and
`label` returns the menu as `:choices` for a caller who wants to see it.

And what persists is **replaced on re-run**, never accreted: `label` clears a
previous run's artifacts under the same `Into` before writing (see `clear-run!`),
and `classify` clears its own previous classification.  Truth values from two
different groundings unioned into one context assert nothing at all.

## MVP scope (docs/solving.md)

Constraints are the engine's own contradictions among the **direct** ground choice
heads — a `(not X)`/`X` pair, a `functional` predicate given two values, or a
`disjoint` type clash.  Choices do **not** propagate through ordinary rules yet
(that is provenance-propagation / full clingo grounding, the named follow-ups).

Backend selector for vaelii's ASP solver. Callers (reason.clj) use
`solver/solve`/`solver/available?` so the engine can run the in-process
clingo backend (default, when libclingo + JNA are present) or fall back to
the clasp subprocess — without any caller change.

The clingo backend is loaded LAZILY via requiring-resolve so JNA/libclingo
stay optional: a plain build (without the `:with-clingo` profile) has no JNA
on the classpath, the resolve fails cleanly, and the facade falls back to
clasp. clasp is also the deliberate fallback for long-running daemons, since
an in-process native crash takes down the whole JVM.

Select explicitly with -Dvaelii.asp.solver or VAELII_ASP_SOLVER = clingo|clasp.
Default is auto: prefer in-process clingo when it loads, else clasp.

Resource-bounded / anytime realization of an answer stream.

The engine's query paths are **lazy** — `ask`, `query`, and the level stack
all yield one solution at a time, paying per result consumed.  Resource-bounding
is therefore the *consumer-side* discipline of realizing that stream under a
bound and reporting whether it ran dry or was cut short — and resumption falls
out of laziness for free, because the unrealized tail **is** the continuation.

A **budget** is a map of optional bounds (any subset; nil / {} means unbounded):

  :max-ms       wall-clock milliseconds — a soft deadline, checked *between*
                yielded results (a single blocking pull is not interrupted, so
                the granularity is one solution — the honest limit, matching a
                closure that has no partial answer)
  :max-results  stop after this many solutions
  :max-cost     a qualitative prover-cost ceiling — a tier keyword (see
                `vaelii.impl.provers/cost-tiers`).  Honored by `ask-within`,
                which drops provers above the tier before the stream is built;
                ignored *here*, since it selects *which* work runs, not how much
                of a stream to realize.
  :max-depth    transformation (rule-expansion) depth — honored by `prove-within`

A **partial result** — the anytime contract returned by `collect` / `from-batch`
/ `resume`:

  :results      the solutions realized in *this* step (a vector)
  :status       :complete  the source ran dry — the answer is exhaustive
                :timeout   :max-ms elapsed with work remaining
                :capped    :max-results reached with work remaining
  :count        (count :results)
  :elapsed-ms   wall-clock spent in this step
  :resume       nil when :complete; otherwise a 1-arg fn (budget -> partial
                result) that continues exactly where this step stopped

`:results` are per-step, **not cumulative**: concatenate across steps for the
whole answer.  The resume continuation captures an in-memory lazy tail (or, for
`prove-within`, the DFS goal stack), so resumption is **in-process only** — it
does not survive a restart, and holding one pins its captured state in the heap
(see the single-writer contract in docs/storage.md).

What knowledge bases this process can load, and the lifecycle of loading one.

Everything above the engine assumes it is holding *the* KB.  A browser that lists the
KBs available, loads one while you watch, and switches to it needs two things the
engine does not have: a description of a KB that has not been loaded yet, and somewhere
for a load that takes minutes to run while the pages keep answering.  Those are the two
halves here.

**A source** is a KB you could load, as data — a kind, a name, and wherever the content
comes from.  Six kinds:

| kind         | content                                             | loader |
|--------------|-----------------------------------------------------|--------|
| `:core`      | the CoreContext vocabulary head alone               | `vaelii.impl.core-context` |
| `:starter`   | the shipped schema-only ontology                    | `vaelii.impl.starter` |
| `:generated` | synthesized from numbers — types, rules, a fwd mix  | `vaelii.impl.io.generate` |
| `:corpus`    | a translated sentence corpus (OpenCyc)              | a foreign reader, `:cyc-corpus` |
| `:dump`      | a vaelii export dump                                | `vaelii.impl.io.import` |
| `:store`     | an on-disk KB already in vaelii's own format        | opened in place |

The first three ship in this repo and are always offered.  The last three are **found**:
each directory on the search path (`VAELII_KB_PATH`, else `./kbs` and `~/.vaelii/kbs`)
is probed, and what marks it — a corpus `meta.edn`, a dump `meta.edn`, a `records/` +
`index/` pair — decides its kind.  A `catalog.edn` (`VAELII_KB_CATALOG`, else
`~/.vaelii/catalog.edn`) names sources outside the search path.  Nothing about a
machine's paths is baked into the repo.

**An entry** is a source that has been loaded, or is loading: a KB, a status, and a
progress reading the loaders report into (`:on-progress`, reported by every loader —
the corpus reader, `io.import/import-dump` and `io.generate/load-into`).  One load runs at a time, on its
own thread, and is cancelled by a flag the progress callback throws on — the loaders
have no other safe interruption point, and an import is not a transaction, so a
cancelled load leaves the KB holding what had already landed.

**A KB is readable before it is finished.**  `activate` asks only that an entry hold a
KB, so the one arriving can be the one every page reads — a corpus is browsable from
its first thousand sentexes, and a store that opens in seconds is browsable while
belief is still being rebuilt behind it.  What that costs a reader is completeness, not
correctness, and `active-caveat` is what says so.

**And a KB can go back out.**  `export-entry!` writes a loaded one as an export dump on
the same thread discipline a load runs on, which closes the loop: a dump written under
the search path is a `:dump` source the moment its `meta.edn` lands, so exporting and
reloading needs nothing outside this namespace.

**Unloading never deletes an on-disk KB.**  A memory-backed entry has its stores
cleared (they would otherwise hold the corpus for the life of the JVM); a disk-backed
one is *closed* — the file lock released, the directory left exactly as it was.  The
same directory can then be loaded again, or opened by another process.

Forward chaining: the semi-naive fixpoint, one agenda for bare and defeasible
rules alike, with the definitional checks re-run on the derivation path and the
`exceptWhen` guard consulted before a conclusion is placed.

Fifth layer of the engine stack (kb <- checks <- special <- integrate <- chain
<- settle): a firing joins antecedents against stored facts (kb), checks its
conclusion (checks), and reflects what it places into the caches through the
derivation-path choke point (special).  Belief settling happens *after* a run,
in `vaelii.impl.settle` — nothing here defeats or arbitrates.

The definitional checks — argIsa argument types, disjointness, functionality —
plus ground-ness and the stratification glue over the rule index.

Second layer of the engine stack (kb <- checks <- special <- integrate <- chain
<- settle):
every check reads the KB (taxonomy, index, believed matches) and returns a value
or throws — nothing here writes.  Both mutation paths consume these: `assert`
(vaelii.core) throws the value, the derivation path (vaelii.impl.chain) records
it in the violations ledger.

A command-line driver for a KB — the shell dual of the in-process API, launched with
`lein run -m vaelii.impl.cli <cmd> <args…>`.  It runs the engine in-process (no
daemon); to talk to a running daemon use `vaelii.impl.client` instead.

  lein run -m vaelii.impl.cli assert  '(dog Fido)'  NaturalWorldContext --dir /tmp/kb
  lein run -m vaelii.impl.cli query   '(dog ?x)'    NaturalWorldContext --dir /tmp/kb
  lein run -m vaelii.impl.cli why     3                                 --dir /tmp/kb
  lein run -m vaelii.impl.cli export  /tmp/dump                         --dir /tmp/kb
  lein run -m vaelii.impl.cli repl --starter          # interactive, starter schema

**Backend.**  `--dir <path>` uses the durable `:disk` backend (recovered on open, so
a fact asserted in one invocation is there in the next); with no `--dir` the KB is
in-memory and lives only for the process — useful for `repl` or a single compound
session, pointless across one-shot commands.  `--starter` loads the shipped schema
(types, contexts, relation rules) so you can explore the ontology.  `--strength
monotonic` marks an `assert` known-true.  `export` takes `--variant
records|records+index` and `--compression gzip|xz|none`.

**One writer.**  A `--dir` KB takes the single-writer file lock (docs/storage.md), so
the CLI and a daemon cannot own the same directory at once — by design.

A thin EDN-over-HTTP client for the vaelii daemon (`vaelii.impl.serve`).  Runs no
engine: it POSTs `{:op :args}` and reads the result back, over JDK `java.net.http`
(no dependency — JDK 21 ships it).

Every call threads an **explicit connection handle** as its first argument —
`(query conn '(dog ?x) 'Ctx)` — the network mirror of `vaelii.core`'s explicit-`kb`
API.  A `conn` from `client` holds a reusable `HttpClient`; no socket opens until a
call.  A daemon reply of `{:ok false}` becomes an `ex-info` carrying the daemon's
`:error` and `:type`, so a remote naming/disjointness refusal surfaces like a local
one.

The dense **columnar trie** index — the `:memory-columnar` backend, off by default.

The flat-map index (`vaelii.impl.kv`) stores each trie node as three entries keyed by
a boxed **vector of the full path prefix**; a path's every prefix is a separate object,
so the structure is redundant boxed keys + HAMT overhead — `bench/…/densetrie.clj`
measured that at ~487 MB of the 592 MB index (300k real facts), and it is the index's
dominant cost.  The bench also found the win is the *layout*, not interning: a
fastutil-map-per-node recovers only 1.28×, a columnar layout ~15–20×.

So here the trie is a real node graph, not a map of prefixes:

  * nodes are `int` ids; node data lives in **grow-on-demand parallel arrays** indexed
    by id — `counts` (primitive `int[]`), `toks`/`tgts` (a node's child edges: a
    **sorted `int[]`** of tokens and the parallel `int[]` of child node ids while the
    node is narrow, one primitive `Int2IntOpenHashMap` once it is wide), `leaves` (an
    `IntPostings`, the same tiered `int[]`/Roaring set Phase 1 uses — this is where the
    two phases unify);
  * edges carry **interned `int` tokens** from a `vaelii.impl.tokens` dictionary, not
    boxed symbols/markers/lists; the dictionary's inverse decodes them for `children`.

**Mutable, not a static CSR.**  A compressed-sparse-row trie is the densest a trie
gets, but it is *static* — the index mutates on every assert/retract.  A per-node
sorted `int[]` supports incremental add/remove (binary-search + array splice) while
still dropping the boxed prefixes and the per-node hashmap slack; the node ids of a
pruned subtree are recycled through a free list.  Freezing the cold majority to a true
CSR is a later compaction pass (the mutable-head / compacted-tail pattern the record
store already uses), justified by measuring where this lands.

**A node's child structure is tiered on its width, and that is a measurement.**  The
splice above costs O(children already there), and nothing bounds a node's width: the
level-2 node holds one child per distinct first argument of a predicate, so an
array-only node structure loads one broad relation — `(isa X T)`, `(genl S T)`, any hot
relation — in time quadratic in that relation's own extent.  It is the *node* that is
expensive, not the trie: holding 200k facts fixed and varying only the widest node's
fan-out, an array-only structure reads 4.2 s at 2,000 children, 9.0 s at 20,000 and
18.2 s at 200,000.  So past `promote-at` children a node's edges become one primitive
`Int2IntOpenHashMap` (O(1) insert, no splice) and drop back to the array pair below
half of it.  Blanket maps are the wrong answer in the other direction — the bench found
a fastutil map per node worth 1.28× against the columnar layout's ~15–20× — and the
tiering is what takes both, since the overwhelming majority of nodes are narrow and
never leave the dense pair.

**Composition keeps the new surface small.**  Only the trie families
(`index`/`unindex`/`lookup`/`count-at`/`children`) are native here; the secondary
roots, the rule / exception indexes, the inverted term index, and the term roster
beside it — all flat `key → set` maps — delegate to an embedded `KvIndexStore` over a
Phase-1 `TieredKvBackend` (int-dense postings already).  `index-sentex` writes those
root/term keys straight to the shared backend with `kv/root-keys` / `kv/sentex-terms`
(and the roster ops with `kv/roster-adds`), so both stores key identically and the
delegated reads stay consistent.

Single-writer, like every index: the arrays are mutated in place; `lookup`/`children`
/`leaves` materialize fresh Clojure collections at the boundary.  Proven set-equal to
`KvIndexStore` by `columnar_index_oracle_test`.

The CoreContext ontology — Vaelii's vocabulary microtheory.  It defines and
documents the core predicates the engine interprets, as sentexes in CoreContext:
the special-predicate surface (types/contexts, argIsa, disjoint, the `set/*Rule`
wrappers, the predicate metadata, negation, `ist`, the evaluables) and the
predicate meta-ontology.  Documentation rides on `comment` sentexes,
`(comment <term> "...")` — ordinary sentexes (stored, indexed, queryable) — so the
KB documents itself in its own representation.

The content is a KB file, `resources/kb/CoreContext.txt` (read by
vaelii.impl.seed); this namespace loads it and reads the docs back.

CoreContext is the spindle **head**: the root every context sees, and the only
layer a core-only KB has.  The layers below it — the definitional `upper`
contexts (between Core and Universe) and the theory `middle` contexts (between
Universe and Well) — are the starter's, not the core KB's, and each wires itself
into the spindle in its own KB file (see vaelii.impl.starter).

  nodes  71%   <- 310 B/node of it is the per-node MAP OBJECT and its HAMT slot
  in     13%   <- 100% dense; RoaringBitmap measured 384x here
  groundable 13%

  nodes / premises / in / groundable / defeated / blocked
  touched / touched-in                                       RoaringBitmap
  depths                                    Int2IntOpenHashMap  (absent => 0)
  supports / consequences   Int2ObjectOpenHashMap<IntPostings>  (absent => empty)
  a justification            columns keyed by id, never an object  (see below)
  superseded                             atom of a persistent map  (sparse)

The dense truth-maintenance network — the `:tms :dense` option, off by default.

The JTMS is **always resident**, so its footprint is a wall in its own right
(measured: ~467 B/node, which is ~43 GB at 100M nodes), and the decomposition
(`lein bench-jtms`) says exactly where the bytes are:

```
  nodes  71%   <- 310 B/node of it is the per-node MAP OBJECT and its HAMT slot
  in     13%   <- 100% dense; RoaringBitmap measured 384x here
  groundable 13%
```

Two findings shape everything below.  **The per-node scalars are already free** —
stripping `:depth`, `:premise?` or `:datum` from the reference releases *nothing*,
because they are shared cached objects (small `Long`s, keywords, booleans).  So the
lever is not "shrink the fields", it is "stop having a map per node": a node here
is a bit in a bitmap and, where it has one, an entry in a primitive-keyed map.  And
**belief sets are the opposite regime from the index's postings** — `bench-postings`
found RoaringBitmap a *loss* (1.07-1.45x) on the index's millions of tiny postings,
while `:in` holds nearly every node and compresses 384x.  Both measurements are
right; density is the variable.

```
  nodes / premises / in / groundable / defeated / blocked
  touched / touched-in                                       RoaringBitmap
  depths                                    Int2IntOpenHashMap  (absent => 0)
  supports / consequences   Int2ObjectOpenHashMap<IntPostings>  (absent => empty)
  a justification            columns keyed by id, never an object  (see below)
  superseded                             atom of a persistent map  (sparse)
```

Two of those deserve their reasons.  **The defeat-classes are one bitmap** because
the lattice has exactly two elements (`vaelii.impl.strength` — monotonic > default,
and the reference already stores only the entries *above* the bottom), so "the
class map" is precisely "the set of monotonic datums".  **Adjacency reuses Phase
1's `IntPostings`** (a sorted `int[]` promoted to a bitmap past 128) rather than a
bare `int[]`: a node's supports are usually one or two, but the *consequences* of a
much-used premise — a rule handle is an antecedent of every justification it
licensed — grow without bound, and an array-copy insert would make loading such a
rule quadratic.

## Why this is a second implementation and not a swap

`RoaringBitmap` is mutable, and the reference is an atom over one persistent map
whose all-or-nothing mutation `jtms_atomicity_test` pins.  A mutable bitmap inside
that value would break `swap!`'s retry semantics and let a reader observe a
half-applied relabel — so the dense structures cannot be dropped into the reference,
and the two ship side by side behind `vaelii.impl.jtms/Tms`.  That is the same shape
the index took (`:memory-columnar` is a whole second trie beside `KvIndexStore`),
and it carries the same obligation: the algorithms are duplicated here against the
dense structures, so `jtms_dense_oracle_test` proves the two answer identically
under randomized operation streams before either is trusted.

**Concurrency.** Writers are serialized on a monitor, so concurrent mutations
compose exactly as the reference's `swap!` retry does.  Readers are *not* locked:
under the engine's one-writer contract (docs/storage.md) there is no reader to
protect, and locking `in?` — the single hottest call in the engine — to buy a
guarantee nothing relies on would be a poor trade.  A reader racing a writer may
therefore see a partially-applied relabel, which is the same latitude the mutable
index backends take.

**Precondition.** `ensure-node` precedes `add-justification`, and a justification's
antecedents already have nodes — which every engine path does.  (The reference
tolerates the violation by growing a malformed phantom node; neither implementation
is specified there.)

A dense in-memory `KvBackend` (`vaelii.impl.kv`) — the `:dense` index axis, under either
record store (`:memory-dense`, `:disk-dense`).

The index's handle-set families (trie leaves, the context / functor / argument roots, the
rule and exception indexes) are the bulk of its RAM, and a bake-off across candidate
encodings found a **packed sorted `int[]`** ~5.6× denser than the
`PersistentHashSet<Long>` the memory backend stores, with `RoaringBitmap` winning only the
few large/hot postings.  So a handle set here is an `IntPostings`: an exact sorted `int[]`
while small, promoted to a `RoaringBitmap` once it crosses a threshold (dense for large,
O(log) add, fast intersect).  The trie's child-*label* set (`[:trie :children …]`) holds tokens —
including numbers — not handles, so it stays an ordinary set; counters stay `Long`s.  The
backend dispatches on the key tag.

`kv-intersect` narrows **in that representation** rather than in the sets it would make:
`RoaringBitmap/and` where both sides are hot, a sorted merge where both are cold, and a
probe of the cold side into the bitmap where the tiers differ, and a binary search of the
short run into the long one where neither is a bitmap.  Smallest posting first, and one
Clojure set built at the end at the size of the answer.  What that buys is not mainly
speed on the big case (hot ∩ hot at 32k: 29.2 → 0.56 ms) but the *shape* of the common
one: a query pins a rare argument on a hot predicate, and 4 handles against a root of n
went from 4.73 ms at n=32,000 to 0.0015 ms at any n — flat in the extent the argument
roots exist to avoid scanning.  `lein perf --only intersect-selectivity` is the gate on
that, and what cost is left tracks the answer rather than the columns, which is the
boundary contract and not the narrowing.

Off by default (`:index :dense`); proven set-equal to `MemoryKvBackend` by
`dense_kv_oracle_test`.  Single-writer: the int structures are mutated in place, and
`kv-members` / `kv-intersect` materialize a fresh Clojure set at the boundary so a caller
never holds the mutable structure.  Handles fit `int` through 2³¹ (≫ 100M).

A key-interning `KvBackend` (`vaelii.impl.kv`) for the columnar index's non-trie
families — the secondary roots, the rule / exception indexes, and the inverted term
index.

Those families are flat `structured-vector-key → handle-set` maps, and the columnar
measurement (`bench/…/densetrie.clj`) found their **boxed vector keys** (`[:argument-root pos
term]`, `[:term-index term]`, …) to be ~150 MB — the majority of the columnar index once the
trie went native.  This backend keeps the *values* as `IntPostings` (Phase 1's tiered
`int[]`/Roaring set) but collapses the keys: the term is interned to an `int` through
the **shared trie dictionary** (`vaelii.impl.tokens`) — so a predicate/individual gets
the same id the trie edges use — and the whole key becomes one packed `long`
(`family | pos | term-id`) into a single primitive `Long2ObjectOpenHashMap`.  No boxed
vectors, no HAMT nodes, one map.

It stays a full `KvBackend` so the existing composition (an embedded `KvIndexStore`
over it) is unchanged: only the recognized index families are int-routed; any other key
— the term roster (term *names*, not handles), a scalar, a counter, the contract test's
synthetic keys — falls back to a plain in-memory backend (in the columnar store the trie
is native, so no `[:trie …]` key ever reaches here).  Single-writer, like every index;
`kv-members` / `kv-intersect` materialize a fresh Clojure set at the boundary — but
`kv-intersect` builds it at the size of the *answer*, narrowing through
`dense/intersect-postings` in whichever representation each posting is in, a mapped run
included.  Proven set-equal to `MemoryKvBackend` on the index families by
`dense_roots_oracle_test` —
which, like every behavioural check, cannot see a family that falls back when it should
route, since the fallback answers identically; `dense_routing_test` reads the
representation and covers that.

The durable-store entry point: open (once per directory) a `DiskRecordStore` and/or a
`KvIndexStore` over a `DiskKvBackend`, take the single-writer lock, and wire what was
opened to the durability daemon.

**The two halves open independently.**  A KB's records and its index are chosen on
separate axes (`vaelii.impl.kb`), and only one of the combinations that reach here
wants both: `:disk` is durable records *and* a durable index, while `:disk-memory` /
`:disk-dense` / `:disk-columnar` keep the derived index in RAM and want the record store
alone — no index log, no index WAL, nothing written to the directory but the records.  So each
component is opened on first use rather than as a pair, and the registry records which
ones a directory actually has.  A directory opened both ways in one JVM therefore
shares its record store across both KBs and hands the RAM-index one no durable index
at all.

A process-global registry keyed by canonical directory mirrors the memory backend's
space registry: two KBs constructed over the same directory share one set of
stores — so a KB "restarted" over the same directory in one JVM (the recovery
tests) sees the durable records the first wrote, with its own fresh taxonomy/TMS, and
the file handles + durability registration + lock are taken once rather than leaking
across the suite's hundreds of KB constructions.  A true cross-JVM restart opens the
directory fresh and rebuilds the RAM state from the durable logs.

How a record is shaped on its way into a log frame, and back.

nippy freezes a Clojure record by writing its **type tag and every field name** into
the frame — so a store of 100M sentexes writes `vaelii.impl.sentex.AtomicSentex` and
`:sentence :context :id :truth :strength` 100M times.  Measured on the real corpus,
that scaffolding is **56% of the store** (87 of 155 B/record) and it says nothing a
frame needs to carry: the field layout is a property of the code, identical in every
frame.

So a frame holds the fields **positionally** — a plain vector, the shape known here —
which is 1.85× smaller and needs no dictionary, no id allocation, and no new durable
ground truth (`lein bench-records`).  The codec is per *kind*, because each kind has
one known set of shapes: a sentex frame is tagged `atomic`/`rule`, a justification frame
is a bare vector (there is only one shape), and provenance is an open application map
that passes through untouched.

**Reading is backward-compatible in both directions.**  `decode` dispatches on the
thawed frame: a vector is positional, anything else is returned as it thawed.  So a
store written before this codec reads exactly as it did (its frames are records), and
a plain map handed to `put-sentex` — which the tests do, and which is not an `AtomicSentex`
— round-trips as the map it is.

Decoding also **interns** the symbols it rebuilds (`sentex/intern-deep`), so a record
paged off disk shares the one vocabulary object per name with every other record and
with the in-memory store, rather than minting its own copy per fetch.  That matters
most for the records the hot cache retains.

**Tokenized bodies** are the second, opt-in step (`vaelii.disk.tokens`): the positional
frame still spells its sentence out in full, and the vocabulary — the same few hundred
thousand predicate and individual names — is written into every one of the frames.  A
tokenized frame replaces the s-expression fields with a varint byte string of ids from
the durable dictionary (`vaelii.impl.disk.tokens`), 2.6× smaller again.  It is a
*fourth and fifth frame tag*, not a format change: a store can hold plain and tokenized
frames side by side, so enabling it costs no rewrite and disabling it leaves what is
already written readable.

Durability management for the disk backend.  Each disk store/kv registers itself
here on open; one daemon fsyncs every registrant on a tick (default 3 s), and one
JVM shutdown hook closes them all on exit.  Without it, a crash between manual
fsyncs loses everything since the last one.

Registration is capability-based — callers hand in `{:fsync :close :label}` (plus an
optional `{:compact :dead-ratio}` for background compaction), so this namespace does
not depend on the stores it drives (which would cycle).

Config (system properties): `vaelii.disk.sync-ms` (tick interval, 0 disables the
daemon), `vaelii.disk.auto-compact` (off with `false`/`0`/`off`),
`vaelii.disk.compact-dead-ratio` (default 0.5),
`vaelii.disk.compact-min-interval-ms` (default 300000).

Low-level file primitives for the on-disk backend.

- Append-only `.log` files hold length-prefixed nippy frames.
  Frame layout: `[len: i32 big-endian][nippy-bytes]`.  The offset returned from
  `append-record!` points at the len prefix.
- `.idx` files are fixed-width arrays of 24-byte slots, indexed by id.
  Slot layout:
    bytes  0..7  offset (i64, -1 = empty, -2 = tombstone)
    bytes  8..15 length (i64)
    bytes 16..19 flags  (u32; bit 0 = the premise bit is meaningful, bit 1 = premise)
    bytes 20..23 gen    (u32, per-write increment)
  Reads rely on the OS page cache; writes overwrite the slot in place.
  A slot is read in **one positional channel read**, not a seek plus four primitive
  `readLong`/`readInt` calls — a `RandomAccessFile` is unbuffered, so each of those is
  its own syscall and moving 24 bytes cost six of them (measured: 52% of a warm
  record fetch, `lein bench-records`).
- `.nippy` files hold whole-blob metadata (counters, the premise set).  Callers
  rewrite them atomically via `write-nippy-atomic!`.

**Shared-pointer invariant.**  A seek→read/write pair on a `RandomAccessFile` uses that
object's single shared file pointer, so any access to a store's live RAF must hold the
owning kind lock; the disk adapters take a per-kind lock around every such touch (write,
`force!`) for exactly this reason.  The *read* primitives here (`read-slot`,
`read-record`, `read-record-sized`) are positional `FileChannel` reads instead — they
name the file offset in the call and never touch the pointer, so they neither disturb a
concurrent seek nor need one of their own.

Compression: frames freeze under the nippy compressor named by the
`vaelii.disk.compress` system property (`lz4` | `zstd` | `none`); default none.
nippy reads the compressor id from each frame header, so mixed frames thaw
correctly.  Durability: `vaelii.disk.fsync=dsync` opens logs `rwd` (O_DSYNC) so
every append is synchronous — off by default (the durability daemon fsyncs on a
tick instead).

A **mapped snapshot** of the columnar index, which pages its cold tail to disk
instead of holding all of it in heap.

`:disk-columnar` keeps durable records and rebuilds the derived index on every open.
That rebuild is O(records) — measured at 5.6 s for 313k, ~30 min at 100M — and the
rebuilt structure is then wholly resident, which is the wall the scale plan names.
This writes the compacted index to disk once and maps it back, so an open reads bytes
and the fact-scaled postings live in the page cache rather than the heap.

## The design is a snapshot, not a store

The index is **derived state**: `reindex` rebuilds every entry from the records.  That
is what makes this cheap — no write-ahead log, no op log, no crash-consistent mutation
protocol, no bucket directory.  It needs a *snapshot* that can be thrown away and
rebuilt whenever it is in doubt, and "in doubt" resolves to `reindex` in every case.

It is also why there is no directory to page.  A flat-map index keys every trie node by
a boxed vector of its whole path prefix, so an out-of-core design over it has to page
the keys themselves; the columnar trie has no keys at all — a node's identity is its
`int` id and its position in the parallel arrays *is* the directory.  `columnar/compact!`
already produces exactly the arrays this writes.

## What is written

Under `<dir>/index/`, four things:

* `trie.csr` — the trie's six CSR sections (`fcounts` `foffsets` `fedge-tok`
  `fedge-tgt` `fleaf-off` `fhandles`), each a raw little-endian `int` run behind a
  header naming the counts.
* `roots.csr` — the secondary roots / term / rule / exception postings as the same CSR
  shape over `dense-roots`' packed `long` keys: sorted keys, an offset column, one
  shared handle run.
* `roots-fallback.nippy` — the term roster and anything else the routed families do not
  claim.  Vocabulary-scaled and irregularly shaped, so it is a blob rather than a
  column.
* `tokens.log` — the durable token dictionary the `int` edges cite, in
  `vaelii.impl.disk.tokens`' format (append-only, id = append position, content-keyed,
  first-writer-wins, never reused).  That module is reused rather than a second
  dictionary format minted: persisting the trie's `int` edges is precisely the seam
  `vaelii.impl.tokens` names as its durable variant.

**One file per structure**, not one per section.  A structure is mapped or discarded as
a unit, so per-section files would multiply the crash window by six for nothing; the
section table in the header already names the offsets `map` needs.

## The residency split

`scale-100m.md`'s rule is *never page the walk* — the worst measured index pathology was
the leading-variable trie fan, 18,512 lookups for one query, and a disk seek is worse
than the round trip that pathology was made of.  So the load is deliberately asymmetric:

* **resident** — the CSR skeleton (`fcounts` `foffsets` `fedge-tok` `fedge-tgt`), the
  roots' key and offset columns, and the token dictionary.  Read into heap on open.
* **mapped** — `fleaf-off` / `fhandles` and the roots' handle run.  These are the
  fact-scaled mass (the roots alone are 69 MB of a 186 MB compacted 300k-fact index) and
  each posting is touched only when its own term is queried.  Cold by construction.

With `mmap` the OS page cache is the residency policy, which is the point — but only
because the skeleton stays hot.

## Validity is the whole design

The failure to fear is a stale snapshot that passes its check: one can be perfectly
self-consistent and describe a KB that no longer exists.  So the stamp covers the
**records**, not the snapshot's own bytes, and it is checked on **every** open — never
behind a flag.  Three things must agree or the snapshot is discarded and `reindex` runs:
the format and `kv/index-layout-version`, the byte-order tag (an image whose endianness
differs is refused rather than read wrong), and `record-store/slot-fingerprint`.  The
decision carries a reason from `import`'s vocabulary — `:absent` `:layout-changed`
`:records-differ` `:entries-truncated` — because a rebuild nobody can explain is a
rebuild nobody notices.

A commit is one atomic step: the sections are written to temps and fsynced, the meta is
**deleted**, the temps are renamed into place, and the meta is written last.  Its
presence is the commit point, so a crash anywhere leaves no meta, and no meta means
reindex.

## What it measured

1.72–1.84× off the index's resident heap and a 1.5× faster open, on a corpus whose
vocabulary is fixed — and resident heap that still grows with the facts, because the
token dictionary is fact-scaled and the CSR skeleton is path-scaled.  The acceptance
property it was built for does **not** hold, which is why it is off by default.

The index store on disk — a `KvBackend` (`vaelii.impl.kv`) over a durable
write-ahead log.

The index is derived state (small next to the records, and `reindex` can rebuild it
from the records alone), so the disk KV keeps the whole key→value map in RAM — a `Long` at
each counter key, a set at each set key, exactly the shape `MemoryKvBackend` holds —
and durably logs every mutation to a `kv.log` of length-prefixed nippy frames.  Reads
are the in-RAM map, so `kv-members` / `kv-intersect` are the same reference /
`set-intersection` operations the memory backend does — the disk only buys durability.

**Logical (op) logging.**  A frame is the write op itself — `[:add-to-set k m]`, `[:remove-from-set k
m]`, `[:put k v]`, `[:delete k]`, `[:increment k]`, `[:decrement k]` — not the resulting value.  A
set-add logs the one added member, O(1), so a bulk load of N members into one root
writes O(N) WAL bytes; new-value logging re-serialized the size-i set on the i-th add
and cost O(N²).  On open the log replays by folding each frame through `apply-op`, the
same function that applies a live op.  `compact!` rewrites the log as one `[:put k v]`
op per live key, so every frame — ordinary or post-compaction — is a uniform op and
the reader needs no snapshot-vs-delta discrimination; it also bounds replay length and
reclaims the delta frames (compaction is this store's snapshot cadence).

Crash-safety: `scan-log` truncates a torn tail on open (a partial op frame is dropped
whole, never half-applied), and compaction rewrites the log crash-safely
(`files/recover-log-compaction!`).  All log writes hold the backend lock (the RAF file
pointer is shared).

Single-writer guard for the on-disk KB.

The disk record store and the disk KV index have no cross-process file locking:
two JVMs appending to the same logs tear them.  This namespace takes an OS advisory
`FileLock` on `<dir>/.vaelii.lock` when a disk backend opens, and fails fast if
another live JVM already holds it.  This matches pure's single-writer contract
(docs/storage.md) — one process holds the KB.

The lock is exclusive and ref-counted per canonical directory (the record store and
the index share one dir, so both acquire and the last release drops it).  The OS
releases it when the JVM exits, so a crash leaves no stale lock to reap.  Set
`vaelii.disk.lock=false` (system property) to disable in a trusted single-host
scenario.

The record store on disk — an implementation of `RecordStore` over per-kind
log/idx pairs (`vaelii.impl.disk.files`).

Three int-keyed kinds — sentexes, justifications, provenance — each a `.log` of
length-prefixed nippy frames plus a `.idx` of fixed 24-byte slots mapping handle →
log offset.  A frame holds its record's fields **positionally**
(`vaelii.impl.disk.codec`), so the type tag and field names are not rewritten into
every one of them; a frame written before that codec still reads, as its own shape.  A record is **paged** from disk on `get`: read the slot, read the frame
it points at, thaw it — two positional reads, no seek, and the records do not sit in
RAM.  What does sit in RAM per kind is the small set of live handles (so enumeration
is O(1)), rebuilt from the idx on open, and a **bounded LRU of hot records** in front
of the read (`vaelii.disk.cache`, 0 to disable).

`next-id` is a monotonic counter recovered as `max(the counters blob, 1 + the
highest slot id across the record kinds)` — the highest slot id is stable across
deletes (a tombstone keeps its slot) and across compaction (slot ids are preserved),
so a handle is never reused even if the counters blob is stale after a crash.  Within
a session every write holds the same bound (`clear-counter!`), because a record can
arrive carrying its own `:id` and nothing re-reads the slots until the next open.

A premise is exactly a sentex whose `:strength` is non-nil (the strength lives on
the record, as on every backend), so the premise set is derived from the durable
records — rebuilt on open, maintained in lockstep by mark/unmark — rather than
stored separately.  Rebuilding it does not mean *reading* them: every write records
the answer in its idx slot's flags, so the open reads the set off the slot walk it
already makes.  A slot that does not carry the bit sends that one handle to its
record, and the record is authoritative wherever both speak (`rebuild-premises!`).

Recovery on open: finish any interrupted compaction, truncate a torn log tail, then
tombstone any slot whose frame now extends past the log (`validate-idx-tail!`).
Crash-safety rests on the write ordering (append the frame, then point the slot at it)
and on `files`' crash-safe compaction.  The tail is located from the frame *lengths*
(`files/log-tail-offset`) and nothing is decoded to find it — and a clean `close!`
records each log's length, so an open whose log is still that long skips even the walk.
The marker is consumed here, so it never describes a store in use; every disagreement
falls back to the walk.

Every RAF touch holds the owning kind's lock.  A write or `force!` must, because the
file pointer is shared (see `files`' shared-pointer invariant); a read no longer has
to — the read primitives are positional — but still does, because that is what
serializes it against a concurrent append and its slot write.

A **durable** token dictionary for a disk store: `symbol/keyword ↔ int`, append-only,
ids assigned in append order and never reused.  It is what lets a record frame spell
its sentence as ids rather than names (`vaelii.impl.disk.codec`), which is 2.6× smaller
than the positional frame it replaces — the vocabulary is written once here instead of
once per frame in all 100M of them.

**The ordering that makes it safe.**  A frame referencing an id the dictionary cannot
decode is unreadable data, so the dictionary must never lag the records that cite it.
Two rules give that, and neither costs a write:

- a token is appended **before** the record frame citing it (`emit!` interns as it
  encodes, which happens before the frame is written), so the token log leads the
  record log in *write* order at all times;
- `fsync` fsyncs this log **first, holding the sentexes kind lock**, so nothing is
  appended between the two fsyncs.  Every record durable after a tick therefore has
  its tokens durable too.

fsyncing *per new token* would also give the ordering, and is what this did first —
but it makes a cold load fsync-bound (measured: ~217 records/s, since a new token is
not rare during one).  Between ticks the two logs can still skew on a machine crash,
exactly as the record log and its idx can; `open-record-store` repairs it the same way
it repairs those, by tombstoning a record whose ids the dictionary does not hold.

**Only symbols and keywords are interned.**  Those are bounded by the ontology.
Numbers and strings are not — a KB of measurements would mint a dictionary entry per
distinct value — so `codec` carries them beside the id stream as literals instead.

Ids are **content-keyed and first-writer-wins**, so they are stable for the life of the
store; the id *value* depends on first-encounter order, which nothing above this reads.
Tokens are never deleted (an id must keep decoding), so the log has no dead frames and
needs no compaction; only a whole-store `clear-records!` empties it.

Writes take the log's lock (there is one writer, and the append must not interleave);
the *reverse* map is an atom holding a vector, so a decode — which runs on every fetch,
under a different lock — reads it without one and still sees a safely published entry.

Qualitative distance — how far apart two things are, said in classes rather than in
numbers: co-located, very close, close, near, moderately far, far, very far.  A relation
algebra over the generic constraint network in `vaelii.impl.qcn`, beside the RCC-8
topology of `vaelii.impl.space`, the compass of `vaelii.impl.orientation`, the frame of
reference of `vaelii.impl.relative` and Allen's intervals in `vaelii.impl.interval`.
Those say *where* or *when*; this says *how far*, which is the third of the three
standard qualitative-spatial questions — topology, orientation, distance.

The seven classes are an ordered chain, each denoting a half-open interval `(lo, hi]` of
the non-negative reals.  They tile `[0, ∞)` exactly, so they are jointly exhaustive and
pairwise disjoint and exactly one holds of any two things.  The bounds are the **one**
thing here that is transcribed rather than computed, and they are a *scale* rather than
a unit: multiplying every bound by one factor leaves the composition table unchanged, so
what the numbers fix is the ratio between neighbouring classes, not a length in metres.

**Composition is computed from the bounds by the triangle inequality**, not transcribed.
If d(A,B) ∈ (l1, h1] and d(B,C) ∈ (l2, h2] then

  max(l1 - h2, l2 - h1)  <  d(A,C)  <=  h1 + h2

— the lower bound strict because a lower bound is, the upper attained when the two legs
are laid out in a line — and the composed class set is every class whose own interval
meets that range.  Distance being non-negative, a lower bound below zero simply means
zero is reachable, which is exactly the co-located class's interval `(-∞, 0]`, so the
arithmetic needs no special case for it.  That makes composition **exact**: the range is
the set of distances the geometry actually admits, and the table is the set of classes
that meet it.  A different chain of bounds gives a different, still-correct table, which
is what a transcribed table could never promise.

**This composes weakly, and that is the honest reading of it.**  Composing two mid-range
classes usually leaves several classes possible — close-then-close spans everything from
co-located to near — because a class is an interval and the triangle inequality relates
intervals loosely.  So the payoff is **refutation and consistency-checking** rather than
pinpoint entailment: it will tell you that two things very close to a third cannot be
very far from each other, and it will catch a set of distance claims that no arrangement
satisfies.  Pinning a pair down takes either a chain through the co-located class, which
is the identity, or several facts about the same pair intersecting.

**Distance is symmetric**, so the converse of every class set is itself and `converse` is
the identity function — the one place this algebra differs structurally from the four
beside it, whose converse maps each base relation to a different one.  The symmetry lives
in the algebra and deliberately *not* in a `(symmetric P)` declaration: that metadata
would hand these predicates to the generic symmetric-relation prover as well, where the
entailment prover means to claim them alone.

Distances are **stored as ordinary sentexes** — the seven named binary predicates
(`coLocatedWith`, `closeTo`, `veryFarFrom`, …), plus three derived predicates
(`withinNearDistanceOf`, `beyondFarDistanceFrom`, `atSomeDistanceFrom`) that each name a
*range* of them.  The things related are ordinary individuals; nothing about them is
special.

The calculus reads every asserted distance visible from a context into a
qualitative constraint network — `{[a b] → #{possible classes}}`, an unrecorded pair
meaning "unknown", i.e. all seven — and `qcn/path-consistent` tightens it to a
fixpoint.  The prover then answers a goal `(P a b)` by **entailment**: it holds iff every
class still possible between a and b satisfies P, `possible ⊆ denotation(P)`.

An emptied constraint anywhere means the asserted distances are unsatisfiable, and then
*no* goal of this calculus is answered in that context — an inconsistent theory should
not be mined for conclusions.

**Soundness.** Path consistency is sound but not in general complete, so an entailment
reported here is real while a *non*-entailment means "not provable", never "provably
false" — the same open-world reading `argIsa` and `exceptWhen` take.

The vocabulary ships in `kb/upper/SpaceContext.txt` beside the topology, the compass and
the frames of reference — all of them are *about* space, so CoreContext keeps only the
grammar they are declared in.  The prover is **opt-in** on top of it: register it with
`vaelii.core/add-prover`, and until then a KB stores and retrieves distances as ordinary
facts without paying for the network.

Interval duration arithmetic — the quantitative half of `vaelii.impl.interval`, which
is qualitative.  Allen's algebra says *that* two intervals overlap; this says *how
long* for, in real units, and adds up the lengths of several.

Two computed predicates, neither ever stored:

  (totalDuration (list I1 I2 …) D)   D is the sum of the components' lengths
  (overlapDuration I1 I2 D)          D is how long I1 and I2 overlap

An interval's own duration is an ordinary stored fact, `(length I M)`, whose measure
`M` is a NAUT — `(QuantityFn N Unit)` or `(QuantityIntervalFn Lo Hi Unit)`.  The index
answers those; this prover only reads them, normalizes each through
`provers/normalize-quantity` against the KB's `dimensionOf` / `conversionFactor` table,
does the arithmetic on `[lo hi]` magnitude bounds, and renders the result back as a
measure.

**Bounds throughout, not points.** A stored length may itself be an interval measure,
and an overlap is often only bounded rather than known, so every computation carries
`[lo hi]` and the render decides the shape: `lo` and `hi` within tolerance give a point
`(QuantityFn …)`, anything wider gives `(QuantityIntervalFn lo hi …)`.  That is what
keeps the answer honest — an over-approximation renders as an interval and says so,
rather than as a point that would claim more than the KB knows.

**The result is rendered in the dimension's base unit**, which is read back out of the
same `conversionFactor` table the normalization used — `(conversionFactor U Base F)`
names the base, and a unit that declares no factor is its own base.  So no separate
declaration says which unit to render in, and none can disagree with the one the
arithmetic actually happened in.  Every unit of a dimension converts to a single base
(the direct-to-base contract), so which component the base is read from cannot change
the answer.  A caller who wants another unit asks the *check* form instead — a ground
`D` is compared after normalization, so `(totalDuration (list A B) (QuantityFn 2.5
Hour))` is answered whatever unit the components were stated in.

**Bind or check**, like `EvaluateProver`: a variable `D` is bound to the rendered
measure; a ground `D` succeeds iff it names the same dimension and the same bounds
within `provers/*quantity-tolerance*`, the same epsilon policy the measure comparisons
use.  A magnitude is snapped to that same grid before rendering, so cross-unit
normalization's last-bit noise never reaches the answer.

**The metric network sharpens an overlap when there is one.**  The qualitative relation
set alone cannot say how much of a partial overlap is shared, so it falls back to the
sound `[0, min(len1, len2)]`.  When `vaelii.impl.stp` has numeric bounds on both
intervals' endpoints it computes a real one instead, and the two are *intersected*: both
are sound, so the tighter of them is.  A KB stating no `temporalDistance` gets exactly the
qualitative answer, unchanged.

The prover is **opt-in** — register it with `vaelii.core/add-prover`.  It needs no
other prover registered: `overlapDuration` reads the qualitative relation set straight
off `interval/possible-allen-relations` and the metric bound straight off
`stp/overlap-window`, both functions of the believed facts rather than queries.  See
docs/duration.md.

Worked examples of the reasoning the shipped ontology actually does — the data, and
the one function that runs one.

**Nothing here is a story about the engine.**  Each example names the sentexes it
rests on, and those are looked up in the live KB before anything is claimed: an
example whose `rests-on` sentences are not stored is reported *unavailable* rather
than answered, so switching to another corpus greys the examples out instead of
silently showing a verdict computed from vocabulary that is not there.  The verdict
itself is an ordinary `ask` / `escalate` / `check`, and the proof is `why`.

Two kinds, and the split is about what the KB ships rather than about presentation:

  **read-only** — no premises.  The shipped schema is types, taxonomy, metadata and
  rules, so everything asked *of kinds* is answerable with no write at all, and the
  page computes it on render.  This is where the taxonomy, `argPreserving`,
  disjointness and the predicate meta-ontology live.

  **sandboxed** — premises naming individuals.  The starter ships no cast (the
  fables and their casts live in the test-world), so an example about defaults,
  joins or refusals has to bring its own, and it writes them into the reader's own
  sandbox microtheory.  Nothing shipped can see in, and the sandbox reset takes the
  whole thing away.

`:expect` is what the ontology is supposed to answer, and `examples_test` asserts
every one of them — so the page cannot drift away from the KB it describes.

The change feed's registry and its accumulator — the leaf seam a settle files its
relabelled region into, and the one place a listener list lives.

An application driving the KB otherwise learns that belief changed only by asking
again, which misses whatever happened between two asks and costs the most on the KBs
where the least is moving.  Everything a feed needs is already computed: a settle
knows the **region** it relabelled and which of that region was believed when it
first touched it (`jtms/touched` / `jtms/touched-in`), and it throws both away.  This
namespace catches them.

**Why here.**  `vaelii.impl.observe` is the precedent and the shape is the same: a
choke point deep in the stack has to reach a consumer defined above it, so the
indirection is a leaf both can see.  What differs is the altitude.  `observe`'s
observers fire on *storage*, which is what an alpha memory mirrors; a feed is about
**belief**, and belief is decided at settle time — an `assert` can store a sentex whose
label several later justifications settle.  So nothing here is notified from
`kb/create-sentex`, and the region is the unit rather than the record.

**What is split where.**  The registry, the accumulator and the reentrancy guard are
here, on the KB's `:feed` atom.  Turning a region into the `{:believed-added
:believed-removed}` entries a listener receives is `vaelii.core`'s job — those are
`preview`'s entry shapes, built from `why-not` and the supporting justifications, and
they belong beside the code that already renders them.  `core` installs that renderer
with `install-dispatch!` when it loads, and `deliver!` calls it.

**What a KB with no listener pays.**  `note-region!` is one deref and a `seq` on the
listener vector, and nothing accumulates.  A KB *with* one pays per relabelled region
— the same region a `preview` diffs — and never per stored sentex; see
`lein perf`'s `feed-listener-scaling`.  See docs/feed.md.

{:engine-dump vaelii.foreign.engine/reader
 :cyc-corpus  vaelii.foreign.cyc/reader}

(when-let [r (foreign/reader :engine-dump)] ((:decode-frame r) frame))
((:load-dir! (foreign/reader! :cyc-corpus)) kb path opts)

Formats vaelii **reads and does not write**, and the plugin seam they arrive through.

A foreign reader is a bridge, not a feature: an engine-dialect dump and a translated
OpenCyc corpus are how knowledge that predates this build gets in, and each one is
finished the day its corpus has been converted once into the format we do write
(`vaelii.impl.io.export`).  Carried in-tree it would be code that must keep compiling,
keep passing tests, and keep being read by whoever changes a record shape, in exchange
for nothing.  So no reader ships here.  This engine reads its own dump format and
nothing else, and the bridges are **separate artifacts** that teach it a format when
they are on the classpath — `vaelii-foreign` is the one we publish.

## What a plugin does

It ships a namespace holding a `reader` var and one resource, `vaelii/foreign.edn`,
which is a map of `kind -> the var holding its reader map`:

    {:engine-dump vaelii.foreign.engine/reader
     :cyc-corpus  vaelii.foreign.cyc/reader}

Every copy of that resource on the classpath is read and merged, so a build reads the
union of the bridges it was given and several plugins compose without knowing about
each other.  A manifest is **edn**, so it declares a name and can never run code, and
the symbols in it are resolved with `requiring-resolve` **on use** — a plugin's
namespaces are loaded when something actually asks for its format, and no reference to
one exists in this build's compile-time graph.  `register` is the same registration
done in code, for an embedding application that has the reader in hand.

Nothing else in this repo names a reader namespace, and nothing here has to change to
add or drop a format.  A build with no plugin refuses a foreign dump or corpus **by
name** instead of half-reading it, which is this file's job.
`foreign_contract_test` is what keeps all of that true.

## Asking for a reader

A caller asks by kind and gets a map of functions, or nil:

    (when-let [r (foreign/reader :engine-dump)] ((:decode-frame r) frame))
    ((:load-dir! (foreign/reader! :cyc-corpus)) kb path opts)

`reader` for a path that has a fallback (the importer reads its own dialect either
way), `reader!` for one that does not (there is no other way to load a corpus).  What
a reader map holds is the reader's own business — the seam carries capability, not a
protocol, because two foreign formats have nothing in common but being on the way
out.

(comment eats "(eats ?animal ?food) means that ?animal takes ?food as nourishment. …")
(comment genl "(genl ?subtype ?supertype) means that every ?subtype is a ?supertype. …")

A sentence in English, **composed** from what the KB already says about its own
vocabulary rather than generated.

The read path is the one with no verifier.  Nothing in the engine can say that an
English sentence describing `(genl penguin bird)` is wrong, so a fluent gloss is a way
to teach a reader something false through their only window onto the formal content —
which makes reading the more dangerous direction here, not the safer one.  The defence
is to not write prose at all where the KB has already written it.

## The comment is the template

The vocabulary documents itself: every shipped predicate carries a `comment` sentex,
and those comments are written in a shape that is already a template —

    (comment eats "(eats ?animal ?food) means that ?animal takes ?food as nourishment. …")
    (comment genl "(genl ?subtype ?supertype) means that every ?subtype is a ?supertype. …")

a **signature** naming the argument positions with variables, then a clause saying what
the predicate means *in those names*.  So glossing `(eats Fido kibble)` is not a
generation problem: read `eats`'s comment, take its first clause, substitute the actual
arguments for the signature's variables.

The variables are why it reads: a parameter spelled `?animal` cannot be mistaken for an
individual the way `Animal` can, and because the *name* carries the sort, the clause
after it needs no sortal noun to lean on — so what substitutes is the sentence a reader
wants rather than one with `place Paris` in it.  Everything past that first clause is
documentation for a reader, not template: how the predicate is used, what it is not,
and what the KB does with it.

A signature written with plain capitalized words and a colon — `(eats Animal Food):
Animal eats Food` — is read the same way, since an imported vocabulary spells its own
comments and they are not ours to rewrite.

This is why the composer is a lookup and a substitution rather than a table of
hand-written patterns: adding a predicate with a documented signature gives it a gloss
for free, and a comment edited to say something else changes the gloss with it.  Of the
277 shipped comments, 175 carry a signature; the 102 that do not are nouns — 86 types
and 16 unit individuals — which need none, because a type gloss is "X is a dog" and
the comment is the apposition after it.

What the composition rate does **not** measure is whether a gloss is worth reading.  It
earns its place where the predicate name is opaque — `genl` glossed as "Every dog is an
animal" teaches a reader what `genl` means — and adds nothing where the predicate is
already an English verb.

## What it will not do

A term with no comment **degrades to naming the term**.  It does not invent a
description, because an invented description is exactly the failure this exists to
prevent, and a reader who sees the bare name has lost nothing they were entitled to.
Every result carries `:source` saying which it got:

  :composed   every literal came from a comment
  :partial    some did; the rest are named
  :named      nothing to compose from — the terms, in a frame
  :generated  a model wrote it (`gloss` never does this; see `with-model`)

The formal sentence is never replaced by the gloss — that is the caller's contract, and
`docs/web.md` states it for the browser.

The `do/` imperatives — the one shape given to `assert` that is neither a fact nor
a rule but an *instruction*: run a labeling / classification and return its result,
storing nothing.  `assert` dispatches a `do/` form here (`run`) before any naming or
well-formedness check, since those expect a sentence.

This is not part of the assertion write-path — it is a separate feature (answer-set
labeling, docs/labeling.md) routed through `assert` for one entry point — so it lives
outside `vaelii.core`.  The backing functions live under `vaelii.impl.asp.*`, which
requires the engine, so they are resolved **lazily**: a static require would be
circular, and the resolve keeps ASP optional (a build without a backend still loads,
and the backend choice is made inside the resolved fn).  An unavailable build throws a
legible error rather than failing to load the engine.

node:   [ L₁ … Lᵢ … Lₙ ]                        σ
rule:   A₁…Aₖ ⟹ C,  with  b = unify(Lᵢ, C)
child:  [ b(L₁) … b(Aᵢ…) … b(Lₙ) ]              σ ∪ b

A **backward** chainer whose state is a set of nodes ordered by cost — not
`vaelii.impl.chain`'s *forward* agenda, which is a queue of newly believed data
waiting to be matched against rules.  This one runs from a query towards the facts,
and what its agenda holds is unfinished proofs.

The other backward chainer is path-structured, walking an explicit goal stack
(`res/prove-from`).  Here
the unit is a **node** — a whole conjunction plus everything accumulated to reach it —
and expanding one is a single rewrite:

    node:   [ L₁ … Lᵢ … Lₙ ]                        σ
    rule:   A₁…Aₖ ⟹ C,  with  b = unify(Lᵢ, C)
    child:  [ b(L₁) … b(Aᵢ…) … b(Lₙ) ]              σ ∪ b

The rule's antecedents under the head unifier are the **residual** — what is left to
prove if this rule is the one that fires — spliced in where `Lᵢ` was.  Applied
repeatedly, that transformation is the whole search: every node is the query rewritten
through some sequence of rules, and a node whose conjunction solves against facts
alone is a completed proof.

Two things follow from the state being a value rather than a call stack.  A stop
between two expansions leaves an **agenda**, not a continuation closure, so a bounded
run is `budget/collect` over the result stream and nothing else.  And the tree is an
artifact that outlives the search, which is where dead ends and "why did this cost so
much" answers come from.

A third follows from the frontier being a priority queue: **which** node pops next is a
policy rather than a structure, and it lives in `vaelii.impl.tactics` — one additive
estimate whose signs the caller picks.  Every tactician returns the same answer set;
what differs is when.

**What it is good at, measured.**  The residual stays *symbolic* — `(anc ?y ?z)` is
not re-asked once per binding of `?y`, it is rewritten once — so the node count is a
function of the rule graph and the depth bound, not of the data.  Over a kinship DAG
the same seven nodes answer 16 leaves and 64 of them, and an open query runs 2-6x
faster than the DFS because each node's conjunction is one planned join rather than a
tuple-at-a-time walk.  A **bound** query is the other way round (2-4x slower): the
rewrite ignores what the caller already knows and computes the relation, then filters.
A conjunctive query is 2-3x slower still, because a k-literal conjunction has more
ways to be rewritten than a single goal does.

**What it cannot do.**  Termination here is the depth bound, and nothing else.  The
DFS is data-driven — it substitutes as it goes, so a chain of length n terminates
after n steps whatever bound it was given — while a symbolic residual grows a conjunct
per rewrite and would grow forever.  So `*max-depth*` is a real ceiling: a derivation
deeper than it is not found, and the depth a query needs is a property of the *data*.
Answer-set parity with `prove` therefore holds up to the bound and not past it, which
is why the selector defaults to `:dfs` (`core/*query-engine*`).  Iterative deepening
is what would close that, and it is not built.

See docs/inference.md.

(argPreserving        P n R)   ; a stored (P … w …) licenses (P … a …) when (R a w)
(argPreservingInverse P n R)   ; …licenses it when (R w a)

**Argument-position preservation** — when a claim about one term licenses the same
claim about another.

`(largerThan dog cat)` says something about two *kinds*.  Whether it also says
something about a golden retriever and a maine coon is not decidable from the
sentence: it depends on whether the relation distributes over the kinds' members.
Some relations do (`disjoint` — subtypes of disjoint types are disjoint) and some
emphatically do not (a chihuahua is a dog, a maine coon is a cat, and the maine coon
is bigger).  So it is **declared**, per predicate, per argument position:

    (argPreserving        P n R)   ; a stored (P … w …) licenses (P … a …) when (R a w)
    (argPreservingInverse P n R)   ; …licenses it when (R w a)

`R` is any **transitive** relation — `genl` and `genlContext` through their cached
closures, or a predicate declared `(transitive R)` walked over stored facts.  A
declaration over anything else is refused at assert
(`wff/arg-preserving-problems`): the reach is walked to a fixpoint, so a relation
that was never said to compose would have transitivity *manufactured* for it, and
`(argIsa argPreserving 3 transitivePredicate)` cannot say so — argIsa is
open-world, and an untyped relation cannot violate it.  Naming the relation is what
keeps this from being a `genl` special case: an argument can equally be preserved
along `partOf`, `connectedTo`, or anything else transitive.  The inverse form exists
so the *other* direction never requires declaring an inverse predicate that has no
other purpose.

Several declarations may name one argument position; their reaches **union**, since
each independently licenses the claim.

## Preservation stays on one side of the type/instance line

`genl` relates **types**, so `(largerThan dog cat)` preserved along `genl` reaches
`golden_retriever` and `maine_coon` and stops there.  It says nothing about Rex and
Whiskers, and that is not a gap here to fill: `relationKind` is a `disjointMetatype`
over `typeRelationPredicate` and `instanceRelationPredicate`, so one predicate
symbol relates kinds *or* instances and never both.  A `largerThan` that inherited
across the line would be a predicate of both kinds at once, which the KB's own
meta-ontology refuses.

Preservation moves an argument along a relation, leaving the predicate and the level
it lives at alone.  Crossing the line is a *different* claim — it links two
predicates and has a quantifier reading to pin down (every member? some member?) —
and the vocabulary for it is `(typeToInstancePred TypePred InstancePred)`, which the
engine does not yet act on.

## Specificity, and why it is not the deleted axis

The interesting case is a claim that inherits *and* a more specific claim that
disagrees.  `(typicallyLargerThan dog cat)` reaches `[chihuahua maine_coon]`;
`(typicallyLargerThan maine_coon chihuahua)` is stated directly.  The stated one
wins, and the general one simply **does not fire for that pair** — undercutting, not
defeat.  Nothing is derived, so there is nothing to arbitrate.

That matters, because `docs/nmtms.md` deleted genl-based specificity as an
arbitration axis on the grounds that it was inference *about* the knowledge rather
than *from* it: it scored a type by the size of its up-closure, a numeric proxy that
tied silently whenever the exception was not keyed on a narrower type.  Nothing here
reconstructs an ordering.  Two claims are compared along the **very relation the
inheritance travels down** — `[maine_coon chihuahua]` is below `[cat dog]` because
`(genl maine_coon cat)` and `(genl chihuahua dog)` are edges the KB holds.  Claims
that are genuinely incomparable are not ranked at all; they come back `:ambiguous`,
which is the same answer the engine gives every other unresolvable clash.

## Strict versus typical, for free

A `:monotonic` claim is **never** undercut.  Strength already propagates from a
justification's antecedents, so `(largerThan dog cat)` asserted `{:strength
:monotonic}` inherits as known-true and a contrary specific claim is a
contradiction — `checks/asymmetry-problem` refuses it — while `(typicallyLargerThan
dog cat)` at the default `:default` inherits defeasibly and yields to the specific
claim.  One declaration, both behaviours, and the difference is stated where it
belongs: on the claim, not on the vocabulary.

Ground goals only.  An open argument is left to the fact and rule provers, in the
shape `different` and the NAF operators already use — enumerating it would mean
walking the inverse reach of every stored witness, which is a different and much
larger question than the one a closed goal asks.

Store mutation is the seam: the two choke points everything that stores or
removes a sentex must pass through.

Fourth layer of the engine stack (kb <- checks <- special <- integrate <- chain
<- settle): the table of what each special predicate *means* lives below in
`vaelii.impl.special`; what lives here is the guarantee that its arms — and the
exception re-check queue they feed — are never skipped.  exceptWhen correctness
depends on every mutation path posting a re-check.  Scattering that call across the
mutation sites makes a missed one invisible — the failure mode is stale excepted
conclusions, silently, and the next mutation path (a bulk load, a new merge) is one
forgotten call from that bug.  So the sequence is stated once per direction:

  sentex-added     integrate through the table + queue the re-check — the assert
                   path's reflection of a sentex that just landed (storage and
                   indexing having happened in `kb/create-sentex`, which is the
                   store-side half of the same seam)
  sentex-removed!  disintegrate + unindex + delete the record + queue the
                   re-check — the one teardown, shared by `retract!` and the
                   excepted-conclusion sweep

The derivation path's twin (`special/derived-sentex-added`) sits beside the table
instead, because the equality arms are themselves derivation sites and must reach
it from below.  The triggers that are *not* store mutations stay explicit at
their own sites: a taxonomy edge change (posted inside the genl / genlContext
arms — the trigger is the closure moving, not the sentex), rule indexing (posted
in `special/index-rule-sentex` — the trigger is the rule gaining an exception to
evaluate), and `recover` (nothing about blocking survives a restart, so it
re-queues everything wholesale).

Allen's interval algebra — a relation algebra over the generic constraint network in
`vaelii.impl.qcn`, and the third alongside the RCC-8 topology of `vaelii.impl.space`
and the cardinal directions of `vaelii.impl.orientation`.  Those two say where things
are; this one says *when* they are, and about intervals rather than instants: an
interval has extent, so two of them can meet, overlap, or nest, and not merely precede
one another.

The thirteen base relations are jointly exhaustive and pairwise disjoint, so exactly
one holds of any two intervals.  Each is a claim about the four ways their endpoints
can compare — writing an interval as `[start end]` with `start < end`:

  :before        a-end   < b-start
  :meets         a-end   = b-start
  :overlaps      a-start < b-start < a-end < b-end
  :finished-by   a-start < b-start,  a-end = b-end
  :contains      a-start < b-start,  a-end > b-end
  :starts        a-start = b-start,  a-end < b-end
  :equal         a-start = b-start,  a-end = b-end
  :started-by    a-start = b-start,  a-end > b-end
  :during        a-start > b-start,  a-end < b-end
  :finishes      a-start > b-start,  a-end = b-end
  :overlapped-by b-start < a-start < b-end < a-end
  :met-by        a-start = b-end
  :after         a-start > b-end

Six of them pair off with their converses (`:before`/`:after`, `:meets`/`:met-by`,
`:overlaps`/`:overlapped-by`, `:starts`/`:started-by`, `:during`/`:contains`,
`:finishes`/`:finished-by`); `:equal` is its own converse and the algebra's identity.

Intervals are **stored as ordinary sentexes** — the thirteen named binary predicates
(`before`, `meets`, `during`, …), plus seven derived predicates (`precedes`,
`subintervalOf`, `sharesTimeWith`, …) that each name a *disjunction* of them.
Intervals are ordinary individuals; nothing about them is special, and nothing here
reasons about clocks, dates or durations — only about order and containment.

The calculus reads every asserted interval relation visible from a context into a
qualitative constraint network — `{[i j] → #{possible base relations}}`, an unrecorded
pair meaning "unknown", i.e. all thirteen — and `qcn/path-consistent` tightens it to a
fixpoint.  the prover then answers a goal `(P i j)` by **entailment**: it holds iff
every relation still possible between i and j satisfies P, `possible ⊆ denotation(P)`.
So `(before A B)` and `(before B C)` entail `(before A C)`, and `(during A B)` with
`(during B C)` entails `(during A C)` and the weaker `(subintervalOf A C)` with it.

An emptied constraint anywhere means the asserted relations are unsatisfiable, and then
*no* interval goal is answered — an inconsistent theory should not be mined for
conclusions.

**Soundness.** Path consistency is sound but not in general complete: it decides the
maximal tractable subclass of the interval algebra and no more, so an entailment
reported here is real while a *non*-entailment means "not provable", never "provably
false" — the same open-world reading `argIsa` and `exceptWhen` take.

The vocabulary ships as `kb/upper/TimeContext.txt`, an *upper* context rather than the
vocabulary head: these twenty predicates are *about* time, so CoreContext keeps only the
grammar they are declared in.  The prover is **opt-in** on top of it: register it with
`vaelii.core/add-prover`, and until then a KB stores and retrieves interval relations as
ordinary facts without paying for the network.

<dump>/
  meta.edn                     the marker, the schema, and the counts
  sentexes.nippy.stream        one frame per sentex
  justifications.nippy.stream  one frame per justification
  provenance.nippy.stream      [handle provenance-map] per frame (omitted when none)
  index/entries.nippy.stream   [key value] per frame — only in :records+index
  index/index.edn              the layout version + the records fingerprint

Write a KB out as a portable **export dump** — a directory holding the record
store's three streams, in a format that survives a backend change, an
index-representation change, and a record class rename.

The `:disk` store directory looks like an archive and is not one: it holds frozen
*records*, so renaming a record class makes every frame in it thaw to a
`{:nippy/unthawable …}` placeholder — silently, because a placeholder is a perfectly
good map.  Hence the one non-negotiable rule of this format:

> **A frame never carries a class name.**

A frame is the record's **field map** — `(into {} record)`, a plain map — so a rename
changes nothing a dump holds, and `vaelii.impl.io.import`'s `field-map` already
accepts one.

What a dump holds is what the record store holds, because everything else the KB has
is derived from it: sentexes, justifications, and per-handle provenance.  A premise
needs no stream of its own — a premise *is* a sentex whose `:strength` is non-nil, a
field on the record in both backends, so the mark rides along with it.  The index is
a cache (`reindex`), the taxonomy and the TMS labels are recomputed (`recover`).

    <dump>/
      meta.edn                     the marker, the schema, and the counts
      sentexes.nippy.stream        one frame per sentex
      justifications.nippy.stream  one frame per justification
      provenance.nippy.stream      [handle provenance-map] per frame (omitted when none)
      index/entries.nippy.stream   [key value] per frame — only in :records+index
      index/index.edn              the layout version + the records fingerprint

**The index is optional and always discardable.**  `:variant :records+index` writes it
as well, in the `[structured-key value]` projection every index backend shares
(`p/index-entries`), so an index written by one backend loads into another.  It is a
*cache*: a reader replays it only when it can prove the entries were derived from
exactly the records beside them (`vaelii.impl.io.fingerprint`), and rebuilds otherwise.
That is what makes writing it safe — an index that does not match its records is worse
than no index, because every lookup then answers confidently and short.

**Framing** is the chunked layout `vaelii.impl.io.import/read-chunked-seq` reads: a
run of `[int32 length][compressed chunk]`, each chunk an independent compression
window over back-to-back nippy frames.  Constant memory on both sides — the writer
holds one chunk, never the corpus.  `meta.edn` *states* the framing rather than
implying it through a version number, because the engine's dumps number their own
format and a reader must never have to guess.

**`meta.edn` is written last**, which makes it double as the completion marker:
`vaelii.impl.catalog/classify` keys on it, so a half-written or cancelled export is
not offered as loadable.  That is the one ordering constraint in the whole format.

Export from a KB nobody is writing: the walk fetches record by record, and pure's
single-writer contract offers no snapshot to walk instead.

What makes a dumped index and a dumped set of records provably the same KB.

The index is derived from the records, so an index dump is only valid *against the
records it was derived from*.  Nothing downstream can notice when it is not: a stale
trie node simply reports fewer handles and a query returns fewer results — no
exception, no warning, just a KB that quietly knows less.  So the writer records a
fingerprint over the records and the reader recomputes it while storing them; a
mismatch discards the index and rebuilds.

**A sum, not a chain.**  The digest is the sum (mod 2⁶⁴) of a per-record hash, so it is
commutative — the reader accumulates it in whatever order the frames arrive, which is
not the order the writer walked — and *additive* rather than xor, so two identical
records cannot cancel each other out.

**What is hashed is what the index is a function of**: the handle, `:sentence`,
`:context`, `:truth`, and a rule's `:antecedent` / `:consequent`.  `sentex/path`,
`kv/root-keys`, `kv/sentex-terms` and the rule index read exactly those, and the handle
because a posting *is* a set of handles — the same content at a different handle makes
every posting naming it wrong.  Deliberately **not** hashed: `:strength`, `:varmap`,
`:direction`, `:defeasible`.  None of them changes a single index entry, so a dump
differing in one of them still has a valid index, and hashing them would make the cache
go unused for a reason that is not a reason.  (`:strength` also arrives after the
storing pass — a premise mark is applied once every record is down — so hashing it
would cost the second pass over the records this exists to avoid.)

The hash is FNV-1a over the fields' own `hash` values: cheap, deterministic across
runs, and strong enough for the question being asked, which is whether two sets of
records are *the same* — not whether an adversary can forge one.  A dump is not a
trust boundary; if it were, this would be a real digest and signed.

**Two granularities, one rule.**  `of-records` hashes what a record *says*, and needs
the record — which is what a dump's reader has in hand anyway.  `of-slots` hashes
where each record *is*: `(id, offset, length)` off the idx, no frame decoded and no
record fetched.  The mapped index snapshot (`vaelii.impl.disk.index-snapshot`) is
checked with that one, because an image exists to make an open cost bytes read rather
than records read, and a content digest would put every record back on the open path.
It is the coarser hash in one direction and the finer one in the other: it cannot see
a record rewritten to the same bytes at the same offset (nothing can produce that),
and it *does* see a rewrite the index does not care about — a premise mark, or a
compaction moving every frame — so a snapshot is discarded and rebuilt after one.
Both directions are safe, because a discard is always legal for derived state.

Synthesize a knowledge base of a chosen **shape**.

The two other kinds of KB are given: a shipped ontology (`vaelii.impl.starter`) is
fixed content, and an imported corpus (`vaelii.impl.io.import`, or a translated one)
is whatever the source says.  Neither lets you ask *what happens at ten times the
rules*, and that is the question a scale or behaviour measurement is made of.  So this
namespace generates a KB from a handful of numbers — how many types, individuals,
predicates, facts and rules, how the rules split forward/backward, how many of them are
defeasible — and each number is a knob the browser renders as a slider (`knobs`).

Two properties make a generated KB usable as a measurement rather than as noise:

* **Deterministic.**  Everything is drawn from one seeded `java.util.Random` in a fixed
  order, so the same parameters give the same KB — a shape can be reproduced from the
  numbers alone, and a run compared against a rerun.
* **Stratified.**  Predicates are split into layers: facts populate layer 0, and a rule
  concluding a layer-k predicate draws its antecedents only from layers below k.  The
  rule set is therefore acyclic, so forward chaining cascades base → derived →
  further-derived and terminates, instead of the runaway recursion a rule set wired at
  random produces.  Individuals and predicates are Zipf-sampled, so the corpus has hot
  terms and a long tail like a real one rather than a uniform smear.

`plan` is pure — the whole KB as data, nothing asserted.  `load-into` asserts it,
reporting progress through an optional `:on-progress` callback (which may throw to
cancel the load, the seam `vaelii.impl.catalog` cancels on).

sentexes.nippy.stream        one field-map frame per sentex
justifications.nippy.stream  one per justification
provenance.nippy.stream      [sentex-handle map] per frame — optional

Import a vaelii **export dump** — a directory of record streams — into a pure KB,
landing in exactly the state pure's own restart path (`reindex` / `recover`) already
knows how to produce.

A dump is a directory whose `meta.edn` is the marker and schema; every other file is
a nippy stream:

    sentexes.nippy.stream        one field-map frame per sentex
    justifications.nippy.stream  one per justification
    provenance.nippy.stream      [sentex-handle map] per frame — optional

A `:records+index` dump also carries the index, as a **cache** that is used only when
it can be proved to describe the records that were just stored (see *the index* below);
otherwise the index is rebuilt, and the summary says which happened and why.

**Framing.**  A chunked stream is a run of `[int32 length][compressed chunk]`, each
chunk a compression window over back-to-back nippy frames; a window stream is one
compression window over the lot.  Our own dumps **state** which (`:framing`); a
foreign dump's is inferred from its own version line.  Both are constant-memory lazy
seqs.

**A frame of our own dialect is a plain field map** whose `:sentence` is already
there — but a rule's `set/*Rule` wrappers and its variable names canonicalized *into*
the record (`:direction` / `:defeasible` / `:varmap`), so both are written back around
it before the constructor sees it.  A frame that is *not* ours goes to a foreign
reader (`vaelii.impl.foreign`), which is resolved at runtime and may not be in the
build at all.  The discrimination is on the **frame**, never on `meta.edn`'s
`:dialect`: a declaration is not an authority over the bytes beside it, and keying off
the frame keeps a mixed dump readable.

Whatever the dialect, **every sentence is re-canonicalized** through this build's own
constructor (`res/kb-sentex`).  A stored canonical form is never trusted, not even
our own: variable numbering, symmetric argument order and comparison folding belong to
the *reading* build, and a record indexed under a key this build's `lookup` never
reproduces would be silently unfindable.

**Handles are preserved** for a dump of ours: every record is stored at the handle the
dump gave it, so a handle means the same thing either side of an export.  Safe because
the destination must be empty and because a store's counter clears any handle written
that way (`p/next-id`) — without which the next `assert` would mint handle 1 again and
overwrite the first imported record.  Two things can still stop a handle landing as
given, and neither is silent: a frame with no `:id`, and a frame whose canonical form
is one already stored, which **collapses** onto that handle (a dedup this build is
right to perform — two engine forms can canonicalize to one pure record — and the
dump's numbering cannot survive it).  Either makes the import `:remapped`, and then one
`old->new` map carries the dump's ids across: justification references, and the
`(sentexHandle H)` a meta-sentex embeds *inside stored content*, which
`rewrite-embedded-handles!` rewrites in the sentence.

**The index is replayed only when it can be proved to fit**, and discarding it is
always safe — which is what makes a cache out of what would otherwise be a risk.  An
index that does not match its records is *worse* than no index: every lookup then
answers confidently and short, and nothing in the engine is positioned to notice.  So
all three of these must hold (`index-decision`):

* the entries are keyed in the layout this build reads (`kv/index-layout-version`);
* the fingerprint accumulated **while storing** equals the one written beside the
  entries (`vaelii.impl.io.fingerprint`) — accumulated, not recomputed, since a second
  pass over the records to validate a cache would cost more than the cache saves;
* the handles were preserved, so a posting names the record it named in the source.

Anything else rebuilds, at `:info`, with the reason named.  A cache that silently
stops being used is a cache nobody maintains.

The store-facing replay is written against pure's real seams: populate the record
store with the re-canonicalized records + justifications + premise marks, then either
install the dumped index (`p/index-load`) or rebuild it (`reindex`), then
`core/recover` — which rebuilds the JTMS and the taxonomy **from the records**, so a
replayed index shortcuts the index and nothing else.  Out of scope: the `:pg-memory`
variant.

A non-monotonic truth-maintenance system.

Each TMS *node* corresponds to a datum (a sentex handle) and records: its label
(IN/OUT), whether it is a premise (and at what assumption *strength*), its
derivation depth, the justifications that conclude it (:supports), and the
justifications that use it as an antecedent (:consequences).

A node holds **no reference to the sentex it labels** — only its handle.  The record
store is where a sentex lives, so a copy here would be a second one to keep in step;
and because this graph is always resident, a strong reference from it would hold every
record in RAM, which on a paging backend defeats the paging entirely (measured: the
nodes reached 50% of the record store).  A caller that needs the sentence fetches it
by handle.

Belief is a least fixpoint: a node is IN when it is a premise or has a valid
justification (all antecedents IN) — EXCEPT that a node in the *defeated* set is
forced OUT.  Because labels are computed from the current justification set and
the current defeated set rather than accumulated as events arrive, belief is
order-independent: asserting a defeater later withdraws a previously-drawn
conclusion, and removing the defeater revives it.  That is the non-monotonic
behaviour a plain monotone JTMS lacked.

## Two invariants

**Order independence.** The same knowledge, given in any order, yields the same
beliefs.  Every operation here recomputes labels from current state, so nothing
depends on arrival order.  (The one place this can leak is a *tie-break* between
two equally-strong beliefs: keying it on handle id would smuggle assertion order
back in, so the contradiction layer keys it on content — see
`vaelii.impl.solve/content-key`.)

**Locality.** No operation recomputes the whole graph.  A change can only affect
nodes downstream of it, so every relabel is scoped to the *affected region* — the
forward consequence closure of whatever changed — with the rest of the graph held
fixed as the boundary.  Cost is proportional to the region, not to the size of the
KB, which is what lets belief maintenance scale.

These two pull against each other, and the reconciliation is the whole design:
a local fixpoint over the region, with boundary labels fixed, has a *unique*
solution, and it is the same one a global fixpoint would produce.  See
`relabel-region*`.

  * strength — every premise carries a strength (:monotonic / :default); every
    justification carries a *strength* too (:monotonic for a bare rule, :default for
    a defeasible one), capping the class it confers.  From these, `relabel` derives
    each IN node's *defeat-class* (monotonic > default, see
    vaelii.impl.strength).  Strength **propagates**: a justification confers no more
    than the weakest of its antecedents' classes, so a conclusion is never stronger
    than what it rests on.  That makes the class equation recursive, and
    `region-classes` solves it as a least fixpoint inside the region relabel.
    The class decides who loses a soft contradiction; the caller
    (core) owns the contradiction layer and pushes the losers into the defeated set
    with `defeat`.

  * defeated — a set of datums forced OUT by contradiction resolution.  It is
    *derived* (recomputed each settle by core), so `clear-defeats!` resets it and
    revival is automatic.

  * superseded — a *map* `datum -> reason` of datums displaced by an equality
    merge: the stale spelling of a fact whose terms have been rewritten to their
    class representative (docs/equality.md).  Three things make it its own state
    rather than a reuse of `defeated` or `blocked`:

    - `blocked` names *justifications*, and a directly asserted `(bornIn Dep
      Chicago)` is a **premise with no justification at all** — `region-fixpoint`
      seeds every premise IN unconditionally, so there is nothing for a block to
      invalidate.  Superseding has to act on the datum.
    - `defeated` would be the wrong reason.  A superseded spelling lost no
      argument; it was restated, and `why-not` must be able to say so — hence the
      map carries the displacing representative rather than being a bare set.
    - It is **not** a forced OUT inside the fixpoint.  A superseded datum stays in
      `:in` for the purposes of `valid?`, because its rewritten twin is justified
      *by it*: forcing it OUT structurally would invalidate the twin's own
      justification and the merge would believe neither spelling.  What
      supersession removes is *reported* belief — `in?` and `in-datums` subtract
      it — so the stale spelling stops matching, stops answering queries and stops
      entering nogoods, while everything derived from it stands.

    Retention is the point: the spelling is the **caller's premise**, so unlike an
    excepted conclusion it is never swept, and dropping the equality gives it back.
    Like `defeated` and `blocked` the map is *derived* — core recomputes it each
    settle from the equality closure — so belief stays order independent.

  * blocked — a set of *justification* ids whose rule's exception currently holds
    (`exceptWhen`, see docs/exceptions.md).  A blocked justification is not a
    defeated conclusion: it is simply **invalid**, so it supports nothing, confers
    no defeat-class, and does not make its consequence groundable — which is what
    lets the ordinary dependency-directed sweep garbage-collect an excepted
    conclusion instead of retaining it for revival.  This module is pure and has no
    KB, so it cannot run the exception query itself: the caller evaluates the
    exception and hands the answer in with `set-blocked`, which relabels only the
    region the change reaches.  Like `defeated`, the set is *derived* — computed
    from current state each settle, never accumulated — so belief stays order
    independent.

Retraction is dependency-directed: drop the premise, relabel, then SWEEP the
affected closure — datums that end up OUT with no valid support and are not
defeated are solely supported by the retraction, so they (and their non-premise
justifications) are returned for the caller to delete from the stores.  A datum that
is merely *defeated* keeps its support and is retained for later revival.

This module owns the in-memory graph; the caller owns physical deletion, since
only it holds the stores.

The KB record, its constructor, and the ground floor of retrieval:
find/create sentexes, the belief-filtered `sentexes-matching`, and the equality-closure
goal rewriting that keeps a retired spelling usable as a question.

Bottom of the engine stack (kb <- checks <- special <- integrate <- chain <-
settle <- vaelii.core): everything here reads the storage protocols, the taxonomy, the
JTMS and the matchers — never assertion, chaining, or settling.  `sentexes-matching`
lives here rather than in core because the layers above it (`integrate-sentex`,
`negation-nogoods`) need *querying*, not asserting — moving it down is what
unties the old `declare assert query settle` knot.

The key-value substrate the index rests on, and the one `IndexStore`
implementation written over it.

The index — the trie, the secondary roots, the rule predicate index, the exception
re-check index, and the inverted term index — is *all* sets and counters keyed
by structured vectors.  `KvIndexStore` encodes that structure once, in terms of a
small `KvBackend` protocol; a backend is then just an adapter that says how a
scalar, a counter, and a set live in some store.  An in-memory map
(`vaelii.impl.memory`) and an on-disk WAL (`vaelii.impl.disk.kv`) are two such
adapters; a SQL or overlay backend is another.

## The flattened count-aware trie

A sentex is indexed by its trie path.  The trie is flattened — every node,
identified by its path prefix, is exactly three keys:

  count-key  [:trie :count prefix]  ->  integer: how many sentexes live at the leaves
                                   under this prefix (selectivity without walking).
  set-key    [:trie :children prefix]  ->  a SET: the next possible token labels (the
                                   node's child edges).
  leaf-key   [:trie :handles prefix]  ->  a SET: the handles of the sentexes whose path
                                   ends exactly here.

**Child edges and leaf handles are separate keys because the trie is ragged.**
Paths differ in length with arity, so one sentex's *full* path can be a proper
prefix of another's: `(rel A B)` in `CeeContext` keys as `[rel A B CeeContext]`,
and `(rel A B CeeContext X)` in `DeeContext` keys as `[rel A B CeeContext X
DeeContext]` — the first path is an interior node of the second.  Storing both
handles and child labels in one set therefore mixed them, and a caller could not
tell them apart by type (a handle is an integer, and so is the token `1970`).  Two
keys make the distinction structural: `lookup` reads only the leaf key at its
terminus, so it can never return a token as a handle, and `children` reads only
the child set, so `plan`'s fan-out divisor can never count a handle as a branch.

Alongside the trie sit the secondary roots, the rule predicate index, the
exception re-check index, and the inverted term index — all flat sets whose
cardinality is their own size.  One more flat set, the **term roster**
`[:term-roster]`, holds the term index's *names* rather than handles, so the
vocabulary can be listed and counted in O(terms) instead of a walk over every record.

Contract: lookup expects a *full* path (sentence tokens + a context slot; the
context may itself be a variable).  A short pattern terminates on an interior
node, whose leaf key is empty, so it yields nothing rather than that node's child
labels dressed up as handles.

## The `KvBackend`

Logical keys are structured vectors and set members are bare values; a backend
turns those into whatever its store wants (an in-memory map uses them directly; the
on-disk backend nippy-frames them into its log).  The load-bearing ops are
`kv-batch` (the whole index write for one sentex lands as one unit — one batched
write) and `kv-intersect` (the multi-column narrowing `sentexes-with-args` needs, one
set intersection rather than N fetch-and-filter reads).  A batch op is a vector
`[op key & args]` with `op` one of `:put`, `:delete`, `:increment`,
`:decrement`, `:add-to-set`, `:remove-from-set`; `kv-batch`
returns one reply per op in order (only `:increment`/`:decrement` replies — the post-op
counter value — are read; the rest are placeholders that keep the vector aligned).

**`kv-member?` is a membership test, not a fetch**, and it is its own op because on
several backends those cost different orders.  `exception-rule?` is the gate
`chain/rule-view-of` takes once per candidate rule per new datum, so answering it by
materializing the roster and testing the result makes forward chaining a product of
two KB-sized quantities.  A flat-map backend hands the stored set back by reference
and hides the distinction entirely; a dense one holds the roster as an `IntPostings`,
where 1e5 gate calls against a roster of 1,000 cost 15,926 ms built-then-tested
against 87 ms on the flat map — so the op exists to let each backend answer with the
probe it already has (a hash lookup, a binary search, a bitmap test).

The lookup-to-query stack: eight levels of escalating interpretive machinery over
the same goal, from a raw index read to full backward chaining.

Every layer the engine already has is a *point on a ladder* — the trie knows
nothing but paths, `raw-match` adds unification, `matches-visible` adds context
inheritance, the prover engine adds closures and rules.  Naming those points and
giving them one call shape makes the cost of an answer legible: you can ask what
the cheapest machinery that answers a goal is (`escalate`), or watch an answer
appear as machinery is switched on (`explain`).

  0 :raw      handles at an index location — no sentence semantics at all
  1 :extent   one literal context, narrowed by functor; no unification
  2 :local    + unification and the symmetric mirror, one literal context
  3 :visible  + context inheritance (the genlContext up-closure)
  4 :typed    + predicate inheritance (the genl spec walk)
  5 :closed   + transitive closure for transitive predicates
  6 :solved   the whole prover registry — no member of it expands a rule
  7 :proved   + rule expansion (the recursive chainer, registry as its leaf)

Each level adds **exactly one** mechanism to the one below it, so a result that
appears at level n and not at n-1 is attributable to that mechanism alone.

**Monotonicity, and the two joints where it is not free.**  Levels 3-5 are wider
calls to the same matcher, and level 5 is literally `level 4 ∪ the closure`, so an
answer reachable at one of them is reachable at the next.  Two joints are not like
that, and naming them is half of what naming the levels is for:

  1 -> 2 **narrows**.  Level 1 is candidate retrieval and never looks at the goal's
  arguments; level 2 unifies.  So for any goal that pins an argument level 2 is a
  *subset* of level 1 — which is one of the two reasons `escalate` floors at 2.

  3 -> 4 can **drop** an answer.  Level 4 is `res/matches-visible`, which reads the
  `except` visibility filter that `res/raw-match` does not, so a sentex a believed
  `(except (sentexHandle H))` hides from the view context is matched at levels 2 and
  3 and gone from level 4 up.  Level 4 is right and the engine agrees — `ask` denies
  that goal too.  What it costs is `escalate`, which will name level 2 as the
  machinery sufficient for a goal the engine does not answer.  No floor fixes that:
  whether a level over-reports is a property of the KB, not of the level.

Level 6 delegates to the real engine (`provers/solve-goal-with`) and therefore
inherits its behaviour, including the short-circuit where a prover claiming
completeness 100 runs *alone*: for a `genl` goal, level 6 returns the taxonomy
closure rather than the union of closure and stored facts, which is why level 6
answers may carry no handle where level 4's did.

What does **not** bend is the content.  Completeness 100 claims a superset of what
every other applicable prover would answer for that goal (`provers`, the contract at
the head of the file), and a prover bearing on a channel it cannot read reports below
100 for the goal so the union runs.  So from level 4 up an answer climbing the stack
can lose its handle and never its existence.

**Laziness.** Every level returns a lazy seq, and each is lazy as deep as the
layer under it allows, so taking one result is strictly cheaper than taking all.
Where that is impossible it is inherent, not an oversight, and is noted at the
site: reading a stored set is one operation whether you take one member or all of
them, and a transitive closure has no partial answer.  The property that does
hold everywhere is that per-result work — a record fetch, an expensive prover, a
rule expansion — is paid per result consumed.

Canonical variable names for a **solution** cache keyed by a literal, and the
translation back into the caller's names.

A backward proof asks the same question many times.  Two sibling branches that both
need `(parentOf Tom ?y)` each solve it in full, and a diamond-shaped rule set pays for
the shared literal once per path through the diamond — the per-path `:seen` guards in
`res/prove-from`'s per-path guard stops a goal from re-*expanding* itself on one
path, and say nothing about the same goal being re-*solved* on another.  Keying an
answer by the literal is what collects that sharing, and the key has to be blind to
what the caller happened to name its variables: `(P ?x)` and `(P ?y)` are one question.

**Why `res/goal-key` is not that key.**  It collapses *every* variable to `?`, so
`(P ?x ?x)` and `(P ?x ?y)` share a key.  That is sound for a loop guard, which only
has to be conservative — over-matching prunes a branch that was going to be pruned —
and unsound for a solution cache, where the second goal's answers include the pairs
the first excludes.  Serving one for the other invents solutions.  So the renaming
here is **repetition-preserving**: distinct variables get distinct names and a
repeated variable keeps its repetition.

**Why `sentex/alpha-rename` is not it either.**  That one builds an *index* key, where
a variable means "anything in this position" and each anonymous `_` is therefore
fresh and unshared.  `unify` does not read `_` that way — `variable?` admits it and
`unify-var` chases its binding, so `(P _ _)` fails against `(P A B)` exactly as
`(P ?x ?x)` does.  A cache keyed on retrieval semantics would hand `(P _ _)` the
answers of `(P ?0 ?1)`, so `_` is renamed here as the ordinary variable it is.

**What is cached, and why there.**  The unit is one literal's *visible matches*
(`res/matches-visible`), not one literal's *solutions* (`provers/solve-goal`).  That
is where the repetition measurably is — a rule-heavy query re-asks a handful of
metadata literals (`(argIsa P n ?t)`, read per believed sentex per argument position
by `provers/inferred-types`) hundreds of times, while its rule subgoals arrive
already substituted and so are mostly distinct.  It is also the only layer at which
the answer is a function of the KB alone.  `solve-goal` is **tier**-dependent, because
`ask-capped` drops provers above a cost tier, and **scope**-dependent, because provers
underneath it read the taxonomy closures and the resident networks through
`observe/cached` — so inside a pinned scope they answer from the view that scope froze.
An answer cached at that layer would therefore have to carry the tier and the scope
that produced it.  `matches-visible` carries neither and reads nothing through
`observe/cached`, so a pinned scope cannot hand it a view the clock has left.

There is **one layer, not two**.  A per-query memo would be redundant: a query
performs no mutation, so the change clock cannot move while one runs, and every
repeat a per-query memo would catch is a repeat this cache already serves under an
unmoved stamp.

The real backend: the Anthropic Messages API over raw HTTP.

There is no official Anthropic SDK for Clojure, so raw HTTP is the supported path —
and it costs nothing here, because the repo already carries both halves: `cheshire`
for JSON and JDK `java.net.http`, which `vaelii.impl.client` already speaks to the
vaelii daemon.  This namespace mirrors that one: an explicit connection handle, no
global state, **no new dependency**.

Reached only when a caller installs it (`vaelii.impl.llm.stub` is the default), so a
build with no credential and no network never loads a socket.

Request shape notes, because several of them are load-bearing:

* **`temperature` / `top_p` / `top_k` are rejected** on this model family — they are
  never sent, and steering happens in the prompt instead.
* **Thinking is on by default** and takes no token budget; depth is set with
  `output_config.effort`.  `:thinking-display "summarized"` opts into a readable
  summary (the default omits the text).
* A **refusal is HTTP 200** with `stop_reason: "refusal"` and empty or partial
  content, so `parse-response` never fabricates a text block and the session loop
  branches on `:stop-reason` before touching `:content`.
* The generated system prompt is a large stable prefix, so its last block carries a
  `cache_control` breakpoint; the user's turn sits after it.  The minimum cacheable
  prefix on `claude-opus-5` is 512 tokens — a short prompt simply will not cache,
  with no error.
* `fallbacks` is sent by default so a policy decline is re-served rather than
  returned as a dead turn.  It rides a beta header; pass `{:fallbacks nil}` to drop
  both if the org has not enabled it.

**Credentials are resolved from the environment, never hardcoded and never logged**
— see `credentials`.

Type-level corrections: a proposal that says the right thing in the wrong shape.

Every model asked about a *type* writes facts **about the type symbol** —
`(eats penguin fish)`, `(mortal penguin)` — where the KB's idiom quantifies over the
type's instances.  Measured across eight models on the shipped schema this is the
dominant remaining error class, and nothing else catches it: `naming/problems` passes
it (the names are all well-formed), `wff` passes it, the argIsa constraints pass it
(open-world — a type symbol carries no type membership, and an untyped argument cannot
violate), and it stores.  The claim is *usually right*; only its shape is wrong.

So this rewrites rather than rejects.  Each correction carries the sentence it came
from, the one to store instead, the **alternatives** where more than one shape is
defensible, and why — because for the most common case the choice between shapes is a
semantic judgement no engine can make for the author:

| claim | shape | inference | exception possible? |
|---|---|---|---|
| definitional — what a penguin *is* | `(genl penguin mortal)` | free, off the cached closure | no |
| defeasible — what a penguin *usually does* | `(set/defaultRule (implies (penguin ?x) (mortal ?x)))` | forward chaining | yes, via `exceptWhen` |

**The defeasible shape is the default, on asymmetric risk.**  A defeasible claim that
should have been definitional costs only the chaining it did not need.  A definitional
claim that should have been defeasible cannot take an `exceptWhen` at all — a `genl`
edge admits no exception — so the only repair is retracting it and rebuilding the
closure.  Guessing wrong in that direction is the expensive one, so it is not guessed.

Nothing here mutates: a correction is a proposal about a proposal.  What to do with it
— show both shapes, show only the rewrite, let the author edit it — is the caller's.

(implies (penguin ?x) (lives_in_antarctica ?x))
(implies (penguin ?x) (capable_of_swimming ?x))
(implies (penguin ?x) (thermoregulates_via_blubber_and_feathers ?x))

The KB's own vocabulary, put in front of the model — and the flag for when the model
invents vocabulary anyway.

**Measured failure mode.**  Asked to write type-level common sense about a term, every
local model that writes usable s-expressions at all encodes structure into the
*predicate name* rather than into arguments:

    (implies (penguin ?x) (lives_in_antarctica ?x))
    (implies (penguin ?x) (capable_of_swimming ?x))
    (implies (penguin ?x) (thermoregulates_via_blubber_and_feathers ?x))

Each is admissible, novel, and useless: a one-off unary predicate joins no rule and
matches no other sentence.  `(livesIn ?x Antarctica)` is the same claim in vocabulary
the KB can reason with.  Swapping models does not fix it — the strongest model
produces the *most* of it, because it produces the most output.

**The check chain cannot catch it.**  A unary snake_case functor is a well-formed type
name by the naming invariants, so `(has_black_and_white_feathers ?x)` passes naming,
groundness, well-formedness, argIsa, disjointness and functionality alike — and it
should, since coining a type is a legitimate thing to do.  So there are exactly two
guards, and they are both here:

1. **Prevention** — `inventory` / `render` put the *relevant available* vocabulary in
   the prompt with each predicate's arity and argument types, and the prompt tells the
   model to reuse it.  A model that can see `livesIn` with `args 1:animal 2:place`
   writes `(livesIn ?x Antarctica)`.
2. **Detection** — `coined` reports every functor in a proposal the KB has never seen,
   with its arity and naming role, plus a reuse-versus-coin count over the proposal's
   literals.  It **reports, never rejects**: a reviewer decides, because a genuinely
   new type is how an ontology grows.

**Selection is by relevance, bounded by tokens.**  Nothing enumerates the KB: the
inventory is seeded from the page's term, walks its `genl` neighbourhood (supertypes
nearest first, subtypes, siblings), and takes the predicates that neighbourhood
*licenses* — the `argIsa`-declared ones whose argument types the term satisfies, plus
the ones already used in facts with those terms.  Every read is pinned by a term
(a cached closure lookup, an `argIsa` query on a fixed argument, a bounded argument-root
walk), so the cost tracks the neighbourhood rather than the knowledge base.

A local backend: Ollama's chat API over raw HTTP.

Same shape as `vaelii.impl.llm.anthropic` — the neutral request/response maps of
`vaelii.impl.llm.protocol`, an explicit connection handle, no global state, **no new
dependency** (`cheshire` for JSON, JDK `java.net.http`).  What differs is everything
the transport does:

* **No credential.**  Ollama serves on a host, not behind an API key, so
  `available?` is a reachability probe rather than a credential lookup.  That is what
  makes this backend testable end to end.
* **The context window is the caller's to set** — `options.num_ctx`, per request.
  Ollama **silently truncates** a prompt longer than it, which would quietly drop the
  user's selection, so the caller sizes the prompt against `num-ctx` *before* sending
  (`vaelii.impl.llm.selection/budget-problem`); nothing here truncates.
* **Constrained decoding instead of tool calls.**  `:format` carries a JSON schema
  that the sampler is restricted to, so a model with no `tools` capability still
  answers in an exact shape.  `capabilities` reads what a model can actually do, and
  `supports-tools?` is the gate — sending 42 tool schemas to a completion-only model
  spends the whole window on something it will never emit.
* **Streaming is newline-delimited JSON**, not SSE: one object per token-ish chunk,
  the last carrying `done: true` and the run's counts.

Counts come back on every response — `prompt_eval_count` is the **measured** prompt
size, which is what a budget is checked against after the fact.

An outside judge over what the knowledge base concluded: every claim glossed into one
English line, handed to a model, and answered *agree / disagree / unsure*.

## This is the other direction, and the trust runs the other way

`vaelii.impl.llm.text` reads English **into** the KB, where the danger is a model
writing something false into the store and the defence is a reviewer between the two.
Here the KB is the one making claims and the model is the one being asked, so nothing
a model says can reach the store: this namespace calls no writer, and a verdict is a
line in a report.  A disagreement is a **finding for a person to read**, never a
retraction, never a defeat class, and never a test failure that edits the KB to make
the number go up.

That is the whole of why the judge is worth having.  The engine can check that a
conclusion follows and that a sentence is well formed; nothing in it can check that
the knowledge is *true*, and a KB full of well-formed nonsense passes every gate this
repo has.  An outside reader is the only instrument for that, and a model is a reader
who will do it for two hundred claims without getting bored.

## The claim is glossed, and a claim the KB cannot gloss is not sent

A model handed `(genl penguin bird)` is judging our notation.  `vaelii.impl.gloss`
composes the English from the KB's **own** comments — the vocabulary documents itself,
and the first clause of each comment is already a template — so what the judge sees is
the knowledge base's sentence rather than a paraphrase somebody wrote for the prompt.
A sentence the KB documents nothing about glosses to `:named`, which is barely more
than the s-expression, so it is left out and counted as skipped: an unanswerable
question dressed up as a low score measures the prompt and not the KB.

## A derived claim is shown its situation, and never its rule

*Fido is awake* is not judgeable on its own — nobody knows Fido.  *Given that Fido is
a dog, Fido is awake* is: it is the everyday question of whether that is a reasonable
thing to say about a dog you have just been told about.  So a derived claim carries
the facts its justification rests on, glossed the same way.

It does **not** carry the rule, and that omission is the design.  Show the rule and
the question becomes *does this follow*, which is validity — the one thing the engine
already guarantees and the one thing an outside judge is not needed for.

## Three verdicts, because two would make the number meaningless

Most of this KB is defaults, and a default is not a universal.  A judge forced to
answer yes or no about *an animal is awake* will pick one and the disagreement rate
will measure the coin.  `unsure` is where a claim that depends on particulars nobody
supplied belongs, and the counts are reported apart so a reader can see how much of
the answer was a shrug.

What the rate is **not** is an accuracy: a careful judge marking a default false is
telling you the default has exceptions, which the KB already knows and stores as a
default for exactly that reason.  So each disagreement carries the claim's strength,
and the disagreements — not the rate — are the output.

The page-scoped prompt: **the unit of work is the term the reader is looking at.**

`vaelii.impl.llm.selection` prompts about lines the reader picked and asks for them
back edited.  This namespace prompts about a *term page* — `/term?q=penguin` — and asks
for knowledge the KB does not have yet:

1. what the page already says about the term, as bare sentences,
2. the vocabulary that term's `genl` neighbourhood licenses
   (`vaelii.impl.llm.inventory`) — arity and argument types included,
3. the reader's free-text instruction ("flesh out the capabilities of this").

Three things differ from the edit path, each because it was measured:

* **The context is dropped.**  A page is already about one context, so the caller
  supplies it and the model writes bare sentences.  That removes a whole class of
  answer the model gets wrong for no gain — and it shortens every line it writes.
* **Decoding is constrained** (`output-schema`, Ollama's `format`).  On generation this
  *rescues* models that otherwise answer in markdown prose; on the edit path the same
  parameter silently drops lines, so the two contracts are deliberately different and
  are not unified.
* **The content is type-level.**  Common sense about a *kind* is a `genl` edge or a
  rule, not a fact about an individual, so the prompt asks for those shapes and shows
  them.

The prompt's one job beyond the shape is to stop the model coining vocabulary — see
`vaelii.impl.llm.inventory`, which is where both guards against that live.

The system prompt, **generated from the live KB**.

A hand-written copy of the ontology in a prompt string rots the moment someone
drops a new `<Context>.txt` into `resources/kb/`.  So every section here is read
back out of the KB it is about: the context topology from `contexts` /
`context-up`, the type hierarchy from `types` / `genls`, the predicate
documentation from the `(comment <term> "…")` sentexes the vocabulary documents
itself with (`vaelii.impl.core-context/comment-of`), the argument types from the stored
`argIsa` sentexes, the disjointness from `disjoint` / `disjointMetatype`, and the
algebraic metadata from `props`.  The naming invariants are the one static section,
because they are mechanical rules rather than content.

The result is a **large stable prefix**: byte-identical across turns for an
unchanged KB (every section is sorted, nothing carries a clock or an id), which is
what prompt caching needs.  The volatile part — the user's request — lives in the
message turn after the cache breakpoint, never in here.

{:model      "claude-opus-5"     ; provider-resolved when absent
 :system     [{:text "…" :cache? true} …]   ; blocks, in order
 :messages   [{:role "user"|"assistant" :content <string | [block …]}]
 :tools      [<tool schema> …]      ; vaelii.impl.llm.tools/schemas
 :max-tokens 8192
 :effort     "low"|"medium"|"high"|"xhigh"|"max"}

{:stop-reason  "end_turn"|"tool_use"|"refusal"|"max_tokens"|…
 :stop-details {…}                ; populated only on a refusal
 :content      [{:type :text     :text "…"}
                {:type :tool-use :id "…" :name "…" :input {…}}
                {:type :thinking :text "…"}]
 :model        "…"
 :usage        {…}}

The pluggable-model seam: one protocol, two methods, and a provider-neutral
request/response shape.

Mirrors `vaelii.impl.solve/Solver` — a protocol plus a deterministic stub as the
default, with the real backend reached only when a caller installs it.  So the
suite, and a build with no API key and no network, run the whole pipeline against
`vaelii.impl.llm.stub` and never open a socket.

**The shapes are the seam.**  A provider takes a `request` map and answers a
`response` map; neither mentions HTTP, JSON, or any vendor field, so the session
loop (`vaelii.impl.llm.session`) is written once and runs against either provider.

Request:

    {:model      "claude-opus-5"     ; provider-resolved when absent
     :system     [{:text "…" :cache? true} …]   ; blocks, in order
     :messages   [{:role "user"|"assistant" :content <string | [block …]}]
     :tools      [<tool schema> …]      ; vaelii.impl.llm.tools/schemas
     :max-tokens 8192
     :effort     "low"|"medium"|"high"|"xhigh"|"max"}

`:cache?` on a system block asks the provider to mark it as a cache breakpoint;
the generated system prompt is a large stable prefix and the user's turn is the
volatile part after it, which is exactly the shape prompt caching wants.

Response:

    {:stop-reason  "end_turn"|"tool_use"|"refusal"|"max_tokens"|…
     :stop-details {…}                ; populated only on a refusal
     :content      [{:type :text     :text "…"}
                    {:type :tool-use :id "…" :name "…" :input {…}}
                    {:type :thinking :text "…"}]
     :model        "…"
     :usage        {…}}

A **refusal is a successful answer with no content** — the caller must read
`:stop-reason` before reading `:content`, so a provider never fabricates a text
block to keep indexing code happy.  Assistant content is echoed back verbatim in
the next request's `:messages`, so a provider may carry vendor-specific blocks
through `:content` untouched as long as it can read its own back.

Which backend a turn runs against — the selection seam.

Stands where `vaelii.impl.asp.solver` stands for the ASP backends: a keyword names a
backend, the backend is **lazily resolved** so choosing one is what loads it, and an
unreachable backend falls back to the deterministic default rather than throwing.
`vaelii.impl.llm.stub` is that default, exactly as `vaelii.impl.solve/local-solver`
is for contradictions — so a build with no credential, no Ollama and no network runs
the whole pipeline and opens no socket.

Three kinds:

  :stub       deterministic, offline, scriptable — the default
  :ollama     a local Ollama (`vaelii.impl.llm.ollama`), no credential
  :anthropic  the Messages API (`vaelii.impl.llm.anthropic`), credential required

Select with `VAELII_LLM_PROVIDER` or `-Dvaelii.llm.provider`; a caller that already
knows what it wants passes the kind (or a built provider) directly.

Resolution is lazy for a reason beyond load time: `anthropic/available?` may shell
out to the `ant` CLI, and `ollama/available?` opens a socket.  Neither should happen
because a namespace was required.

Scoring a set of candidate entries against a hand-written one.

`vaelii.impl.llm.text` produces candidates and `vaelii.core/check-edit` says whether each
is *admissible*.  Neither says whether it is **right**, and nothing in the engine can:
the whole reason the reading direction needs a reviewer is that every check passes on a
well-formed translation of a claim the text did not make.  So the only honest measure is
against knowledge somebody wrote by hand, and this is the arithmetic for that.

## The gold set is read out of a KB, never transcribed

A second copy of the fables' sentexes in a scoring fixture would drift from the ones the
suite actually loads, and a score against a stale gold set is worse than no score.  So
the gold is a set of **handles** in a loaded KB, and a candidate matches when
`vaelii.core/handle-of` finds it under one of them.

That also means the comparison uses the engine's **own** canonical form rather than a
reimplementation of it: a rule whose variables are named differently, whose antecedents
arrive in another order, or whose symmetric arguments are the other way round is the same
sentence to `handle-of` and is therefore the same sentence here (docs/canonicalization.md).
Nothing about matching is this namespace's opinion.

## Two scores, because the constants are unrecoverable

A fable introduces its characters by kind — *a lion*, *a mouse* — so the names in the
formal version (`LionA`, `MouseA`) are the modeller's, and no reader of the text could
produce them.  A strict score therefore reads zero on stories whose structure was
recovered perfectly, which measures the naming convention rather than the reading.

So `score` reports both, and the pair is the finding:

* **strict** — the candidate matched a gold handle as written;
* **aligned** — the same comparison after renaming the candidate's *introduced*
  individuals onto the gold's, one-for-one, by the types each is asserted to have
  (`alignment`).  A renaming is a bijection or it is not applied, so alignment can never
  merge two characters into one to score better.

Nothing here writes: `handle-of` is find-only, and the alignment is arithmetic over
sentences.

The selection-scoped prompt: **the unit of work is a set of handles, not the KB.**

`vaelii.impl.llm.prompt` renders the whole vocabulary — every context, type and
predicate — and `vaelii.impl.llm.tools` renders every read as a tool schema.  Both
are fixed costs that grow with the KB, and against the schema-only starter (no
individuals, no facts) they already come to ~8,800 tokens before the user has said
anything.  A KB heading for 100M sentexes cannot pay that per request, and a model
with no `tools` capability cannot spend half of it at all.

So this namespace prompts about **what the reader selected**:

1. the selected sentexes as the editor's own `[sentence context]` lines,
2. a vocabulary card computed *only* from the terms those lines mention — each
   term's `comment`, its `argIsa` constraints, its place in the genl hierarchy, and
   its metadata,
3. the reader's instruction.

Every read is pinned by a term the selection actually contains (`comment-of`, an
`argIsa` query on a fixed predicate, a genl closure lookup), so the prompt is
**O(selection)** and flat in KB size.  Ten sentexes cost the same in a KB of ten as
in a KB of a hundred million.

**The model rewrites lines; it does not write.**  Its answer is the edited line set,
which `vaelii.impl.llm.session/propose-edit` diffs against the selection by content
to produce the `{:add … :remove …}` batch — the same diff the browser's editor does
on Save, so an unchanged line touches nothing.

**Nothing here truncates.**  A selection too big for the context window is a clean
refusal (`budget-problem`), because the alternative is Ollama silently dropping the
front of the reader's own selection.

The turn loop: propose → validate → repair → an edit batch.

**The model never writes.**  Its output is `{:add [[sentence context opts?] …]
:remove [handle …]}` — the exact shape `vaelii.core/edit` takes, and the exact shape
the browser's textarea editor already produces.  So a proposal lands in the existing
editor as a reviewable diff: no new write path, no new trust boundary, and no way
for a model turn to reach storage.  Applying is a separate, explicit call
(`apply-proposal!`), which is where the `!` lives.

**The well-formedness checker is the critic.**  `check-batch` is
`vaelii.core/check-edit` — `assert`'s own check chain run over each proposed entry
for its answer rather than its effect, storing nothing, reporting each failure with
the same `:type` keyword `assert` would have thrown (`:naming`, `:not-ground`,
`:not-range-restricted`, `:not-well-formed`, `:not-stratified`, `:arg-type`,
`:disjoint`, `:functional`).  That is a deterministic grader rather than a
model-judged one, which is what makes the repair loop terminate on a fact rather
than on an opinion — and sharing the writer's own chain is what keeps the two from
drifting, so the model is never graded more leniently than it will be applied.

**The loop is bounded twice.**  `:max-repairs` caps how many times a rejected batch
is fed back, and `:max-turns` caps total provider turns including tool calls, so
neither a stubborn model nor a tool-calling one can spin.  Running out of repairs is
a reported outcome (`:status :invalid` with the rejections), not an exception.

The default provider: deterministic, offline, no credential.

Standing in the same place `vaelii.impl.solve/local-solver` stands — the stub that
makes the seam usable before (and without) a real backend.  `lein test` runs the
whole pipeline against it, so the suite needs no API key and opens no socket, and a
deployment with no credential degrades to a provider that proposes nothing rather
than to an exception.

Behaviour is **scripted**, so a test drives the session loop exactly: `:script` is
the sequence of turns to hand back, one per `complete`/`stream` call, and `:default`
answers every call past the end of it.  Each entry is a full response map, or one of
three shorthands:

  "some text"                    a plain text answer
  {:batch {:add […] :remove […]}}  text holding that batch in a fenced `edn` block
  {:lines [[sentence context] …]}  the selection path's line set (`:json? true` for
                                   the JSON envelope shape instead)
  {:assertions [sentence …]}       the page path's bare sentences, in the JSON envelope
                                   it decodes under (`:lines? true` for the bare-line
                                   shape a model ignoring `format` writes)
  {:candidates [[sentence seg] …]} the reading path's candidates, each naming the
                                   document sentence it came from (`:untranslated`,
                                   `:notes`)
  {:verdicts [[item verdict] …]}   the judging path's answer, one verdict per numbered
                                   claim (`true` / `false` / `unsure`, optional note)
  {:tool "kb_sentexes_matching" :input {…}}  a tool-use turn (`:id` optional)

With no `:script` the provider answers every turn with an empty batch — valid,
applies to nothing, and never varies.  That default is the *whole-KB* path's answer;
on the selection path (`session/propose-edit`) it reads as unparseable, which is the
safe outcome — the only line set meaning "change nothing" is the reader's selection
itself, and a provider that never saw it cannot write one.

The document-scoped prompt: **text in, candidates out — never knowledge in.**

`vaelii.impl.gloss` composes English *out of* the KB and says why that direction is the
dangerous one: nothing in the engine can check that a sentence means what a text said.
This namespace is the other direction, and it has to answer that argument rather than
ignore it, because every check the engine has passes on a correct-looking translation of
the wrong claim — naming, well-formedness, argument types and disjointness all read the
*sentence*.  So what is built here is a **candidate generator with a reviewer between it
and the store**, and every decision below follows from that:

* a candidate is a `[sentence context opts]` entry, which is the shape
  `vaelii.core/edit` already takes and the browser's editor already parses — so a
  proposal lands as a reviewable diff and there is no second write path;
* a candidate carries the **span** of the text it came from, so an accepted sentence is
  auditable back to the sentence that produced it;
* a candidate is `:default`, never `:monotonic` unless the reader says so — a translated
  guess asserted as known-true would defeat hand-written defaults;
* what the pipeline **could not** translate is part of the answer (`coverage`), because a
  reader who is shown only the two-thirds that worked reads it as a reader that
  understood the document.

**Where the boundary is.**  Nothing here is in `vaelii.core`, and nothing here writes.
Like `web` / `serve` / `llm`, this is an application over the engine: the engine's
contribution is the critic (`check-edit`), the vocabulary (the taxonomy and the
declarations), the provenance side map, and the equality partition — all of them public
reads that existed already.  See docs/reading.md.

## Resolution is the problem; parsing is not

A pipeline that coins `has_black_and_white_feathers` for every sentence produces
fragmentation rather than knowledge, and no naming check refuses it (docs/naming.md says
so in as many words).  So the document's own words are resolved against the vocabulary
the KB already has **before** a model is asked anything:

* `spellings` turns each run of the document's words into the symbols a KB term could be
  spelled as — *prepared for winter* into `preparedForWinter` and `prepared_for_winter`,
  *Fido* into `Fido` — and `known` asks the KB which of them it has.  Generating and
  asking runs the *opposite* way from inverting the KB's vocabulary into the words each
  term is written with, which is the one read here that would grow with the KB;
* `resolve-in` walks the document longest-run-first and non-overlapping, so a compound
  predicate is not shredded into the words its name is made of;
* every resolved term is the equality partition's `representative`, so a word spelled at
  a retired name resolves to the term that name was merged into.

What resolves becomes the vocabulary card (`document-inventory`), which is the
prevention half of the fragmentation guard; the detection half is
`vaelii.impl.llm.inventory/coined`, unchanged and shared with the other three paths.

The model's read surface over a KB — **generated**, not hand-written.

`vaelii.impl.serve/ops` is already an allowlisted, EDN-typed map of `vaelii.core`
calls: the exact surface the browser and the daemon reach a KB through.  So the
tool schemas are derived from its **read subset** rather than transcribed, and the
tool calls are dispatched back through the same table.  A read added to `serve/ops`
becomes a tool with no edit here; a read renamed there cannot rot a copy here,
because there is no copy.

**The model never writes.**  `write-ops` names every mutating op, and anything
resolving to a `!` var is treated as one whatever the table says, so the exposed set
is reads only.  The model's *output* is a proposed batch, reviewed and applied by a
human (`vaelii.impl.llm.session`) — there is no write tool and no write path.

Argument shapes come from the `vaelii.core` var's own `:arglists` (minus the leading
`kb`) and its docstring, so a signature change is picked up on the next build.  JSON
carries no symbols, so a sentence / context / term argument is a **string holding an
EDN s-expression** — `"(dog ?x)"`, `"WellContext"` — read back with
`clojure.edn/read-string` (never `read-string`: EDN has no reader-eval, so a model's
output cannot evaluate code).

What a reviewer needs to know about one proposed line, gathered in one place.

A proposal is judged on **four independent axes**, and they are independent in the
strong sense: a line can be admissible and still wrong-shaped, refused and still worth
keeping once rewritten, admissible and shaped right and still quietly fragmenting the
vocabulary.  Prose about a batch buries all four; a reviewer reads a gutter.

  :problems    what the KB itself says — `vaelii.core/check-edit`, typed
  :correction  what shape it should have been in — `vaelii.impl.llm.correct`
  :coined      what vocabulary it invents — `vaelii.impl.llm.inventory/coined`
  :confidence  how sure the correction is, which is a fifth thing only in the sense
               that a rewrite the engine cannot decide is a decision handed back

Each already exists; what did not is one call that runs all of them over one batch and
lines the answers up **by entry**, so a caller renders a row rather than joining three
reports by index.  Nothing here stores, checks a rewrite, or applies one: this is a
reading of a proposal, and the proposal is still a proposal afterwards.

The default in-memory backends for the two storage protocols, selected at KB
construction.  The engine above the protocols never touches a concrete store, so a
KB built on these runs the whole engine with no external dependency; the on-disk
backend (`vaelii.impl.disk`) is the durable alternative.

The record store implements `RecordStore` directly over maps.  The index reuses
`vaelii.impl.kv/KvIndexStore` — the one trie/roots/index implementation — over a
`MemoryKvBackend`: one map keyed by the structured key vectors (equal vectors are
equal keys), holding a `Long` at each counter key and a set at each set key.
`kv-intersect` is a `clojure.set/intersection`; `kv-members` returns the stored set
by reference (no serialization, no copy).

**Durable-within-the-JVM semantics by space number.**  Two KBs constructed over the
same `:space` number must share state, or the persistence/recovery tests (a second KB
restarted over the same databases) would find an empty store.  A process-global
registry keyed by space number provides that: `(memory-record-store {:space 15})` twice
returns records backed by *one* state atom.  `clear-records!` / `clear-index!`
empty a space.  (State lives only for the life of the JVM; the on-disk backend is what
survives a process restart.)

**Single-writer.**  Pure runs one writer (docs/storage.md, "The single-writer
contract"), so each store is one atom mutated by `swap!`; reads deref a snapshot
and are lock-free.  Interleaved *writers* would not be serializable.

KB naming invariants, as predicates over symbols — and the walk that applies them to
every **literal** of a sentence rather than to its outermost functor alone.

  predicate    camelCase, lowercase-initial, no underscore   parentOf, genl, argIsa
  individual   CapitalCamelCase                               Fido, Tom
  type         snake_case, lowercase, unary predicate         dog, physical_object
  context      CapitalCamelCase ending in Context             UniverseContext, CoreContext

Single lowercase words (dog, genl, parentOf) satisfy both `predicate?` and
`type-symbol?`; role is disambiguated by position and arity, not the symbol alone.
A functor carrying an **underscore** is a type name and nothing else, and types are
used as *unary* predicates — `(dog Fido)`, not `(isa Fido Dog)` — so it is legal at
arity 1 and nowhere else.  `(lives_in penguin cold_place)` is a type name doing a
relation's job; admitting it fragments the vocabulary into one-off predicates
(`lives_in_antarctica`, `capable_of_swimming`) that can never join a rule or match
another sentence.

How hard these are enforced is the **KB's** to say, not this namespace's: `open-kb`'s
`:naming` selects `:strict` / `:warn` / `:off` (`policies`, below) and `assert` reads
it.  The predicates themselves do not move — `:off` stores a name nothing can classify,
not one classified differently.

`problems` checks the functor of every literal a sentence contains — a rule's
antecedents, its consequent, an `exceptWhen` query's conjuncts, a `not` body, an
`ist`-directed sentence, a negation-as-failure query — not only the outermost one.
A rule consequent is exactly where generated content lands, and the outermost
functor there is `implies`.

Non-atomic terms (NATs) via reification — Strategy A.

A NAT is a function-application term `(F arg…)` that denotes an entity —
`(FruitFn AppleTree)`, `(CapitalOf France)`.  A function splits by declaration
into two kinds:

  (reifiableFunction F)    object-denoting.  A ground `(F a…)` is a **NART**: it
                           reifies to an opaque `nat/`-namespaced constant `K`
                           *before* it reaches the index, so the NART autoindexes
                           exactly like a hand-minted symbol — no trie-key change,
                           no term-index change.
  (unreifiableFunction F)  evaluated/interpreted.  The NAT is a **NAUT** and stays
                           *structural* — `(QuantityFn 5 Meter)` keeps its magnitude
                           and unit readable for a downstream prover; it is never
                           minted.

The constant↔expression map is itself an ordinary stored fact, `(termOfUnit K E)`
in UniverseContext, so the inverted term index makes `E`'s constituents (and `K`)
discoverable natively — no KV side tables.  `K` stays STABLE across renames: a
rename rewrites the expression inside the one `termOfUnit` sentex in place, and
nested NATs referencing `K` need no cascade.

This namespace holds the detectors, the index-backed lookups, display expansion,
and the reify — **both** modes: the read-mode (dedup, never mint) and the
write-mode (mint a fresh constant, materialize its result types, merge rename
collisions).  The write-mode stores its `termOfUnit` and result-type facts through the
full assert path, reached by `vaelii.impl.wiring` — which is where the reason that is
not an ordinary require is written down.  So all NAT reification lives here.

What sits above this and *calls* the reify rather than reimplementing it:
`vaelii.impl.skolem` mints the witness an existential rule head fires to, and
`vaelii.core` drops an orphaned NART when its last use is retracted (it rides the
`retract!` sweep).

Reads the store, the taxonomy and belief directly (nat <- kb); reaches assertion only
through the seam above.

The leaf seam the engine's mutation choke points notify **without a require cycle**.
Two things ride on it, and they are independent: named observers of the stored fact
set, and one counter saying that *something* changed.

**Observers.**  The incremental rule-matcher (`vaelii.impl.rete`) keeps RAM alpha
memories that must mirror the stored fact set exactly.  The only structural mutations
to that set are `kb/create-sentex` (add) and `integrate/sentex-removed!` (remove), but
both of those namespaces sit *below* `rete` in the layering — `rete` needs `kb`,
`resolution`, and `plan` to match — so they cannot call it directly.  They call the atoms
here instead, and `rete` installs itself into them when it is engaged.

When nothing is engaged the atoms hold `nil` and `notify-*` is a single deref plus
a `nil?` check, so the reference forward chainer pays essentially nothing.  The
observer is global rather than per-KB (single-writer, like the rest of the engine);
the installed functions dispatch on `kb` themselves, so several KBs can be live at
once and each keeps its own alpha memories.

**The change clock** is the cheapest possible version of the same idea, for a cache
that has to notice a change nobody registered to hear about.  See `note-change`.

Cardinal-direction reasoning — a relation algebra over the generic constraint network
in `vaelii.impl.qcn`, and the companion to the RCC-8 topology in `vaelii.impl.space`
(`vaelii.impl.interval` is the third, over time).  RCC-8 says whether two regions touch
or nest; this says where one place lies *relative to* another.  (Orientation is the
standard qualitative-spatial
name for this family — topology, orientation, distance — and it keeps the namespace
clear of a rule's chaining `:direction`, which is an unrelated thing.)

The nine base relations are the projection-based cardinal direction calculus.  A
direction decomposes into two **independent** one-dimensional point relations, one per
axis — east-west on x, north-south on y — each `:lt` / `:eq` / `:gt`:

  :n  [:eq :gt]   :ne [:gt :gt]   :e [:gt :eq]   :se [:gt :lt]
  :s  [:eq :lt]   :sw [:lt :lt]   :w [:lt :eq]   :nw [:lt :gt]
  :eq [:eq :eq]   (the same place)

That decomposition is the whole trick, and it is why there is no 9×9 table here:
**composition is computed, not transcribed.**  Composing two directions is composing
their x projections and their y projections separately through the three-relation
point algebra, then reading the result pairs back as directions.  Since the nine
directions are exactly the nine `[x y]` combinations, that read-back is total and the
composition of any two base directions is a non-empty set — so the table nobody wrote
down cannot disagree with itself, and north-then-east *is* northeast because `:eq;:gt`
is `:gt` on x and `:gt;:eq` is `:gt` on y.

Directions are **stored as ordinary sentexes** — the nine named binary predicates
(`northOf`, `southeastOf`, `sameLocationAs`, …), plus four derived predicates
(`northwardOf`, `eastwardOf`, …) that each name a *disjunction* of them: a northerly
component, whatever the east-west one.  Places are ordinary individuals; nothing about
them is special.

The calculus reads every asserted direction visible from a context into a
qualitative constraint network — `{[a b] → #{possible base directions}}`, an
unrecorded pair meaning "unknown", i.e. all nine — and `qcn/path-consistent`
tightens it to a fixpoint.  the prover then answers a goal `(P a b)` by
**entailment**: it holds iff every direction still possible from a to b satisfies P,
`possible ⊆ denotation(P)`.  So `(northeastOf A B)` and `(northeastOf B D)` entail
`(northeastOf A D)`, and with it the weaker `(northwardOf A D)` and `(eastwardOf A D)`.

An emptied constraint anywhere means the asserted directions are unsatisfiable, and
then *no* direction goal is answered — an inconsistent theory should not be mined for
conclusions.

**Soundness.** Path consistency is sound but not in general complete, so an entailment
reported here is real while a *non*-entailment means "not provable", never "provably
false" — the same open-world reading `argIsa` and `exceptWhen` take.

The vocabulary ships in `kb/upper/SpaceContext.txt` beside the RCC-8 one — both are
*about* space, so CoreContext keeps only the grammar they are declared in.  The prover
is **opt-in** on top of it: register it with `vaelii.core/add-prover`, and until then a
KB stores and retrieves directions as ordinary facts without paying for the network.

The read-only mount: a `KvBackend` and a `RecordStore` that answer every read and
**refuse every write**.

A base shared by N forks is only shared if nothing can write it, and the honest way to
guarantee that is structurally rather than by review: an overlay composes over one of
these, so a write path that forgot to divert fails loudly at the seam instead of
silently mutating what every other fork is reading.  That is invariant 1 of
docs/overlay.md, held by construction.

Two calls are deliberately *not* refusals.

* `next-id` on the frozen record store.  It hands out a handle nobody holds and
  touches no stored record, and it is what the overlay's id watermark is seeded from
  (`vaelii.impl.overlay.store`) — the alternative, a `max` over the base's whole live-id
  set, is O(base) at every mount.  Two JVMs mounting one base each bump their own
  in-RAM counter to the same value and then diverge into their own overlays, which is
  exactly what independent forks are.
* `kv-entries` / `sentex-ids` and friends.  Enumeration is a read.

This is a decorator, not a file mode: it says nothing about how the underlying store
was opened.  Opening the base's files read-only at the OS level is the disk backend's
business and orthogonal — this is what makes the *composition* safe whatever the base
is (memory, disk, or a later SQL store).

`OverlayKv` — a composite `KvBackend` layering a private **writable** overlay over a
shared **read-only** base.  Reads resolve overlay-first and fall through to the base;
writes land only in the overlay; the base is never mutated, so N JVMs can share one
frozen base index while each keeps its own fork.

This is the index half of the `:overlay` backend (the record half is
`vaelii.impl.overlay.store`), and it is the whole of it.  `KvIndexStore`
(`vaelii.impl.kv`) writes *every* index family — the count-aware trie, the context /
functor / argument roots, the rule index, the exception re-check index, the inverted
term index and the term roster — in terms of this protocol and holds no state of its
own, so one decorator here forks the entire index and the trie walker, the matcher, the
planner and the query layers above it are unchanged.  That is what the `KvBackend` seam
was extracted for.

## The merge model, per key

* **Sets.**  `members(K) = (base(K) ∪ overlay(K)) − removed(K)`, where `base(K)` is
  empty if `K` carries a tombstone, and `removed(K)` records the base members this
  overlay removed (a base set cannot be edited, so a removal is recorded rather than
  applied).
* **Scalars and counters.**  An overlay value shadows the base's.  A counter is
  **copy-on-write**: the first `kv-increment` / `kv-decrement` seeds the overlay from
  the base value, so afterwards the overlay holds base+net and reads are exact.  An
  untouched counter reads straight through.
* **Whole-key delete.**  A sticky tombstone in `::deleted-keys` shadows the base for
  that key.  A later `kv-add-to-set` repopulates it from the overlay *only* — the base
  stays shadowed, which is "deleted, then re-added fresh".  `kv-put` shadows the same
  way, because a put replaces a key rather than merging into it.
* **Wholesale clear.**  `kv-clear!` empties the overlay and sets `::cleared`, after
  which every base key reads absent.  That is O(1) rather than a tombstone per base
  key, and it is what makes `reindex` work on a fork: clear the merged index, then
  rebuild it from the merged records.

Bookkeeping lives in the overlay under reserved keys — `::cleared`, `::deleted-keys`,
and `[::removed K]` — namespaced here, so they cannot collide with an index key (every
one of those is a vector tagged with an unnamespaced keyword, or `[:term-roster]`).
Because the bookkeeping *is* overlay data, a durable overlay carries it durably and a
remount serves the same merged view with no separate recovery step.

## What has to be merged, and why

`kv-count` answers the **merged** cardinality, never the overlay's.  The count-aware
trie is a selectivity structure — `plan/order` costs every conjunct off `count-at`, and
`provers/est-bindings` off the functor root — so a base-blind count would not be a
wrong answer, it would be a silently wrong *plan* for every query touching inherited
content.  `kv-intersect` merges for the same reason: `sentexes-with-args` is one set
intersection over the functor and argument roots, and it must see the base's postings
or a fork would stop finding its own inherited facts.

Merging is not the same as *building* the merged set, and the difference is the cost of
every query plan a fork makes.  A key the fork has not touched — no overlay members, no
recorded removal, no tombstone — merges to the base's own value, so `inherited?` names
that case and `kv-count` / `kv-members` hand the base's own answer straight back.  Over
a flat-map base the two roads read the same, because its `kv-members` is a reference
return; over a `:dense` base, where the posting has to be materialized into a set first,
counting through the merge cost 12.6 ms per call on a 100,000-handle root — a selectivity
read, per conjunct, on a key the fork had never written to.  `kv-member?` is the same
observation at member granularity: `exception-rule?` probes both sides rather than
merging, which is what keeps the firing-path gate O(1) across the seam.

`kv-get` is the scalar/counter read and does **not** merge set values: an overlay value
shadows the base's.  No key in the index is read both ways — the trie's counters are
read by `kv-get` and its handle sets by `kv-members` — and a backend is free to hold a
posting in a private representation (`vaelii.impl.dense-kv` returns an `IntPostings`
here), so merging at this op would mean type-testing another backend's internals.
`kv-entries`, whose contract *is* Clojure sets, merges properly.

**Single writer.**  Pure runs one (docs/storage.md).  A batch is applied op by op
through this decorator rather than as one atomic step the way `MemoryKvBackend` applies
it, so the instance lock is held around the whole of `kv-batch` — an incidental reader
beside the writer then sees a batch whole or not at all, as it does on every other
backend.

Mounting a fork: freeze a base, compose a private writable overlay over it, and hand
back the two stores a KB is built from.

A **base** is any pair of stores mounted read-only (`vaelii.impl.overlay.frozen`); a
**fork** is a fresh writable pair composed over it.  Nothing is copied and nothing in
the base is written, so N JVMs mount one frozen base and each evolves its own fork —
the sharing needs no protocol between them, and equally offers no coherence between
them: a base that changes under a mounted fork is outside the contract.

## Which index a fork can be taken over

The overlay is a `KvBackend` decorator, so it forks exactly the index path that is
written over that protocol: `KvIndexStore` (`vaelii.impl.kv`) and therefore the
`:memory`, `:dense` and `:disk` index axes.  The `:columnar` index is a **native**
`IndexStore` — its trie is int-id nodes in parallel arrays, with no keys and no backend
underneath — so a `KvBackend` decorator would fork its roots and leave its trie behind.
That is refused here rather than half-done.  Forking a columnar index is a different
construction: its compacted CSR mode is already an immutable base, so the natural shape
is a mutable columnar head over a frozen CSR base, not a KV decorator.

## Bookkeeping

The record half keeps tombstones and released premise marks in a small `KvBackend`
beside the overlay (`vaelii.impl.overlay.store`).  An in-RAM overlay gets an in-RAM one
— the whole fork is ephemeral — and a disk overlay gets a durable one under
`<dir>/overlay-meta`, so remounting that directory over the same base serves the merged
view it was left in.  The index half needs none: its bookkeeping lives in the overlay
index itself, under reserved keys, and so is exactly as durable as the fork is.

`OverlayRecordStore` — a composite `RecordStore` layering a private **writable**
overlay over a shared **read-only** base.  Reads resolve overlay-first, skipping
tombstoned base handles; writes land only in the overlay; the base is never mutated.
The record half of the `:overlay` backend (the index half is
`vaelii.impl.overlay.kv`).

* **The id seam.**  The overlay's handle counter is seeded above every handle the base
  holds, so a newly minted handle can never collide with a base one.  A record written
  at a handle the base *already* uses is therefore an **override** — the same handle,
  a different record — and the overlay's copy wins every read.  That is how a base
  record is edited without editing the base: `mark-premise` materializes an override
  before it writes, since the assumption strength lives on the record.
* **Tombstones.**  Deleting a base handle cannot touch the base, so it is recorded and
  the read path filters it.  They are sticky: a base record cannot come back through
  fall-through, only by being written again into the overlay (a revival, at the same
  handle).
* **Wholesale clear.**  `clear-records!` empties the overlay and marks the base
  hidden — one flag rather than a tombstone per base handle — so a fork can be reset
  to empty without walking what it inherited.
* **Durable bookkeeping.**  The tombstone sets, the released premise marks and the
  hidden flag live in a small `KvBackend` under reserved keys, mirrored in atoms for
  the read path.  Every mutation writes through, and a mount rebuilds the atoms from
  it, so remounting a durable overlay over the same base serves the same merged view:
  a deleted base record stays deleted, a released premise stays released.  An
  ephemeral fork passes an in-RAM bookkeeping backend and pays nothing for the
  machinery.

**Counts need no delta bookkeeping here.**  A `RecordStore` in pure exposes handle
*sets* rather than counts, and everything counted — `sentex-count`, `context-size`,
`count-with-functor` — is read off the index, where the merge is the trie's own
copy-on-write counters and the merged root sets (`vaelii.impl.overlay.kv`).  So the
counts a fork reports are exact by construction rather than by a second, parallel
accounting that could drift from the records.

**The fork's belief is rebuilt, not overlaid.**  The JTMS is not storage — it is a
separate protocol (`vaelii.impl.jtms`) over derived state — and pure already has the
operation that computes it from records: `recover`.  So a fork gets its own network by
recovering over the merged view, and nothing here layers one truth-maintenance graph
over another.

Conjunctive query planning: the order a conjunction's literals are solved in.

A conjunction is commutative — `[(parentOf Tom ?y) (dog ?y)]` and its reverse have
exactly the same solutions — but it is not equicost.  Solved left to right, the
first literal's matches are enumerated in full and each one re-drives the second;
so the first literal's *fan-out* multiplies everything after it.  Leading with the
selective literal is the whole game, and on a measured three-literal join it ran
7x faster than leading with the general one.

Three mechanisms, the first two of which the KB already had lying around unused:

**Selectivity** — the count-aware trie answers "how many facts are under this
path prefix" in O(1) (`count-at`), and the secondary argument roots answer "how
many facts have this term at position n" (`count-with-arg`) for the ground
arguments the trie cannot reach.  `est-matches` reads both.

**Sideways information passing** — a literal's cost is not fixed, it depends on
what is already bound when it runs.  `(parentOf ?x ?y)` is the whole extent of
`parentOf`; the same literal after `?x` is bound is one person's children.  So no
literal is costed once and for all: an estimate is always taken under the variables
bound at the point the literal would run.

**The cartesian factors last, on structure rather than on cost** — a literal
sharing no variable with anything else in the conjunction narrows nothing and is
narrowed by nothing, so wherever it runs it multiplies the row count of everything
after it.  Its own extent is then the wrong thing to rank it by, and rank it the
wrong way: a *selective* isolated literal is the worst kind, because taking the
cheapest available literal puts exactly that one first, where its factor is applied
to the whole rest of the plan.  `deferring-isolated-order` holds them to the back.

Sharing no variable is what makes such a literal *unconstrained*; it is not on its
own what makes it a multiplier.  A literal matching at most once multiplies by at
most one, so it can only prune and belongs first — and the ground literal, which
both chaining paths produce by substituting a rule's bindings before planning, has
no variables to share and so satisfies the structural test vacuously.  Both
conditions are therefore checked, and `cartesian-factors` is where.

That placement is deliberately made on **structure and not on an estimate**.
Whether a literal shares a variable is read off the conjunction; how big a join
comes out is a guess the index can only bound from above, and those bounds do not
compose — a plan chosen by minimizing estimated cost end to end multiplies the
bound's error once per literal, and lands wide of one that never trusted it that
far.  So the estimate decides the order *within* each group, where it is compared
once and locally, and structure decides which group a literal is in.  The one thing
an upper bound *can* settle is that a literal will not fan out at all — a bound of 1
is a proof of it — which is the only load the estimate carries in that decision.

## What is never reordered

Ordering here is an execution decision and must not change the answer set.  Two
classes of literal are held back, exactly as `sentex/canonicalize-rule` holds them
back when it canonicalizes a rule for storage:

- **Deferred (evaluable) literals** — `evaluate`, `lessThan`, `greaterThan`.
  These consume bindings rather than produce them; `(evaluate ?z (+ ?x ?y))` run
  before `?x` is bound does not throw, it quietly yields *no* solutions.  They are
  never hoisted above a literal that binds them.  They are, however, pulled
  *forward* to the first point where all their variables are bound — a test that
  can run early prunes the search early, which the storage canonicalization (which
  parks them uniformly last) does not attempt.
- **The recursive literal of a rule** — an antecedent whose functor is the rule's
  own consequent functor.  It stays last among the generators, because a backward
  chainer executes the conjunction left to right and one that re-enters the rule
  before generating anything has nothing to recurse *on*.

  Note what this is **not** protecting against.  A rule's antecedents are put into
  canonical order at *storage* (`sentex/canonicalize-rule`), which is where an
  author's spelling stops being observable — assert the same rule with the
  recursive literal written first and the stored antecedents are identical.  So
  left-recursion is not a state a rule can reach here, and this pin is the cost
  model being kept from re-introducing one, not a rescue.

## Determinism

Ties break on the literal's original position, so a plan is a function of the
conjunction and the KB's counts, never of iteration order.  Same knowledge, same
plan — the order-independence the rest of the engine holds to (see
`vaelii.impl.jtms`) applied to execution rather than belief.

The point algebra over time **instants** — a relation algebra over the generic
constraint network in `vaelii.impl.qcn`, and the smallest one there is.  Three base
relations, jointly exhaustive and pairwise disjoint, so exactly one holds of any two
instants:

  :before   t(a) < t(b)
  :equal    t(a) = t(b)
  :after    t(a) > t(b)

`vaelii.impl.interval` is about stretches of time, which have extent and can therefore
meet, overlap and nest; this is about the moments themselves, where the only question is
which came first.  The two meet at `vaelii.impl.stp`, which relates an interval to its
two endpoint instants and puts numbers on the gaps between them.

**The same algebra appears twice in this tree.**  `vaelii.impl.orientation` composes two
independent one-dimensional projections to get the nine cardinal directions, and each
projection is exactly these three relations under the spellings `:lt` / `:eq` / `:gt`.
The table is duplicated rather than shared: there the three relations are a position on
an axis and are a private implementation detail of a nine-relation algebra, here they
are an order in time with their own vocabulary, and neither namespace should have to
read the other's keywords to say what it means.  Nine identical entries are cheaper than
that coupling, and either copy is checkable against the definitions on its own.

Instants are **stored as ordinary sentexes** — the three named binary predicates
(`instantBefore`, `instantAfter`, `instantEqual`) plus three derived ones
(`instantNotBefore`, `instantNotAfter`, `instantNotEqual`) that each name a *disjunction*
of them.  Instants are ordinary individuals; nothing about them is special, and nothing
here is about clocks or calendars — only about order.

The calculus reads every asserted instant relation visible from a context into a
qualitative constraint network — `{[i j] → #{possible base relations}}`, an unrecorded
pair meaning "unknown", i.e. all three — and `qcn/path-consistent` tightens it to a
fixpoint.  The prover then answers a goal `(P i j)` by **entailment**: it holds iff every
relation still possible between i and j satisfies P, `possible ⊆ denotation(P)`.  So
`(instantBefore A B)` and `(instantBefore B C)` entail `(instantBefore A C)`, and the
weaker `(instantNotAfter A C)` with it.

For three relations path consistency is not merely sound but **complete**: the point
algebra's full disjunctive form is tractable, and a network of it that survives the pass
has a model.  So an emptied constraint here means genuine unsatisfiability, which is what
makes a cycle of strict `instantBefore` facts a reportable contradiction rather than a
suspicion.

The vocabulary ships in `kb/upper/TimeContext.txt` beside the interval relations.  The
prover is **opt-in** on top of it: register it with `vaelii.core/add-prover`, and until
then a KB stores and retrieves instant relations as ordinary facts without paying for the
network.

Storage protocols so the record store and index store each have swappable
implementations (in-memory by default, on-disk for durability, or an alternate KV
store later).  The rest of the system programs against these protocols and never
against a concrete backend.

Pluggable provers for the query engine.  A prover answers a goal and declares
how it expects to perform, so the engine can choose among applicable provers:

  applicable?   can it answer this goal at all?
  est-bindings  ~how many solution bindings it will produce
  cost          a qualitative first-answer cost tier (see `cost-tiers`)
  completeness  0..100 — see the contract below
  solve         the solutions, as raw binding maps

`ask` runs the cheapest *complete* prover alone (fewest `est-bindings`);
otherwise it unions the applicable provers cheapest first by `cost` tier.
Built-in provers: transitivity (genl/genlContext,
complete via the cached closures), disjointness (complete), `different` (the
unique-name assumption read off the equality closure — ground only, see
docs/equality.md), facts (the index), and rules (backward chaining through the same
engine).

## What completeness 100 claims

**For this goal shape, my answers are a superset of what every other prover reading
the same sources would answer.**  That is the reading that licenses running alone,
and it is a claim a prover is competent to make about itself.

The tempting alternative — *nothing else can answer this goal* — is a claim about a
predicate, and it stops being true the moment a KB adds a second way to reach that
predicate.  Whether such a way exists is not a question any one prover can answer,
because it is about the sources it does **not** read.  So the engine asks it, once
per goal, in `sole-prover`: a claimant runs alone only when `shadowing-channels` is
empty.  A prover therefore declares a constant and reasons only about its own
sources, and a prover registered through `add-prover` is guarded without its author
knowing the mechanism exists.

A computed prover normally earns the claim it makes: the closure provers are built
out of the very facts `FactProver` would return and out of the derivations a rule
contributes, and a calculus reads both into its network — converse and composition
included — before entailing anything.

Generic qualitative-constraint-network path consistency — the shared substrate
every relation algebra reasons through (`vaelii.impl.space` is RCC-8 topology,
`vaelii.impl.orientation` cardinal direction, `vaelii.impl.interval` Allen's interval
time).

Pure data in, pure data out: nothing here knows about a KB, a context, or belief.
Reading stored facts into a network and reading an answer back out is the algebra's
job; this namespace only tightens.

A relation **algebra** is a map:

  {:universe  the full set of base relations — an unknown constraint
   :identity  the singleton constraint on the diagonal (i,i)
   :compose   (fn [s1 s2] → s) — composition of two relation sets
   :converse  (fn [s] → s) — the converse of a relation set}

A **network** is `{[i j] → #{base relations}}`, both directions stored; an
unrecorded pair is the universe.  So a network is a *value*, which is what lets a
caller memoize an expensive pass on its content.

Sets are the interface and **bitmasks are the arithmetic**: a network is encoded into
a flat array of masks for the duration of a pass and decoded back on the way out, so
every caller keeps reasoning in relation sets while the cubic loop reasons in
`bit-and`.  See "bitmask relation sets" below.

Path consistency is sound but not in general complete: it tightens every pair to
what composition permits, and an emptied constraint proves unsatisfiability, but a
path-consistent network can still be globally unsatisfiable outside an algebra's
tractable subclass.  So a constraint that survives is *possible*, not *satisfiable*,
and a non-entailment is "not provable", never "provably false".

The KB glue every relation algebra over `vaelii.impl.qcn` shares — reading believed
facts into a network, and reading entailments back out as prover solutions.

`qcn` itself knows nothing about a KB: an algebra is a parameter and a network is a
value.  This namespace is the other half of that seam, and it is the *same* half for
every calculus, so it is written once here rather than three times over.  A **calculus**
bundles what actually differs:

  {:name        a keyword, naming the cache and the parity oracle
   :algebra     the `qcn` relation algebra
   :denotation  {predicate -> #{base relations}} — base ones are the singletons,
                derived ones the wider disjunctions}

Everything else — the reader, the two caches, the four goal shapes, the cost and
completeness declarations — follows from those three.  `vaelii.impl.space`,
`vaelii.impl.orientation` and `vaelii.impl.interval` each define an algebra and a
vocabulary and call `calculus`; a fourth would be the same.

Both polarities are read and both are answered.  A believed `(not (P a b))` narrows the
pair by the **complement** of P's denotation, and a goal `(not (P a b))` is answered by
**refutation** — `possible ∩ denotation(P) = ∅`, where the positive goal needs the
stronger `possible ⊆ denotation(P)`.  Both are licensed by the base relations being
jointly exhaustive and pairwise disjoint, which is what makes "not P" a constraint
here rather than an absence of information.

Three caches, and they answer different questions:

* the **network is resident**, on the KB's own `:qcn` atom, keyed `[calculus context]`
  and stamped with `observe/change-clock` — so it is read out of the KB once and then
  reused until the engine actually mutates something.  Building it is one
  belief-filtered read per predicate of the calculus per polarity (twenty-eight of them
  for RCC-8), and it is asked for constantly: a rule joining a qualitative antecedent
  asks per binding, and every settle re-checks `entailment-withdrawn?` once per firing
  of every rule that mentions the calculus.  Those are stretches in which nothing
  mutates at all, which is exactly what the clock recognises.
* the **path-consistency pass** is memoized on the network *value*, in an atom the
  calculus owns.  That is sound across queries because the network is derived from the
  believed facts: any change to them yields a different map and so a different key.
* the **support-carrying pass** — which stored sentexes an entailed relation rests on —
  is memoized separately, on the same network value, so an ordinary query never pays to
  propagate support nobody asked for.

Beside those, and not a cache at all, the resident atom carries the **join baseline**:
the network a calculus's forward rules were last re-joined over, which is what lets the
next re-join run over the pairs that moved instead of over every pair the network
entails (`join-delta`).  It deliberately outlives a clock tick — its job is to describe a
moment the clock has moved past — and it is safe to lose, since losing it costs a full
re-join and nothing else.

Rebuild the index store wholesale from the record store.

Everything the index holds — the trie, the secondary roots, the rule index, the
exception re-check index, the inverted term index — is *derived* from the
stored sentexes, so the repair for a damaged or stale index is mechanical:
clear it and re-derive every entry.  Three situations need it:

* a crash between the record write and the index pipeline (`assert` spans both
  stores; each side is a single pipeline, but the seam between them remains)
  — the orphaned record is unfindable, and re-asserting its sentence
  would mint a *second* handle for the same canonical form;
* an index layout change (the leaf/child key split makes an index written in the
  old shape read as empty — fail-safe, but a persistent KB needs this rebuild);
* any suspicion that counts and extents have drifted: a rebuild is cheaper
  than an audit.

Run `core/recover` afterwards: it rebuilds the TMS and taxonomy from the
stores, and parts of that rebuild (`rebuild-taxonomy` reads the functor root)
read the very index this restores.

Named bare, like `recover`: the `!` convention marks destruction of stored
*knowledge*, and this destroys only derived state and recreates it from the
records, which stay untouched.

Relative direction — where one thing lies from another **as seen from a point of
view**: the mouse on the lion's left, the crow in front of the fox.  A relation algebra
over the generic constraint network in `vaelii.impl.qcn`, beside the RCC-8 topology of
`vaelii.impl.space`, the cardinal directions of `vaelii.impl.orientation` and Allen's
intervals in `vaelii.impl.interval`.  The compass says where a place is on the map;
this says where a thing is from where you stand, which is the only thing a story ever
says.

**The frame of reference is the context.**  Relative direction is ternary in the
literature — A is left of B *from viewpoint C* — and a constraint network is strictly
binary, a constraint being a set of relations on a *pair*.  The resolution is that a
context already **is** a frame of reference: a network is built per context out of the
facts visible there, so `(leftOf Mouse Lion)` asserted in `LionMouseContext` is a claim
in that microtheory's frame and in no other.  Two microtheories looking at the same
individuals from opposite sides state opposite facts and neither contaminates the
other; a frame that has to be argued about rather than assumed is a context, and the
argument is `genlContext`.  So this calculus is binary, composes exactly as the
cardinal directions do, and needs nothing of the shared glue that the other three do
not already need.

The nine base relations are the projection-based calculus that shape allows.  A
relative direction decomposes into two **independent** one-dimensional point relations,
one per axis of the frame — left-right, and front-back — each `:lt` / `:eq` / `:gt`,
reading the axes as coordinates that grow rightwards and frontwards:

  :left  [:lt :eq]   :front-left  [:lt :gt]   :behind-left  [:lt :lt]
  :right [:gt :eq]   :front-right [:gt :gt]   :behind-right [:gt :lt]
  :front [:eq :gt]   :behind      [:eq :lt]   :eq           [:eq :eq]

That decomposition is the whole trick, and it is why there is no 9×9 table here:
**composition is computed, not transcribed.**  Composing two relations is composing
their left-right projections and their front-back projections separately through the
three-relation point algebra, then reading the result pairs back as relations.  Since
the nine relations are exactly the nine `[left-right front-back]` combinations, that
read-back is total and the composition of any two base relations is a non-empty set —
so the table nobody wrote down cannot disagree with itself, and left-then-in-front *is*
front-left because `:lt;:eq` is `:lt` on one axis and `:eq;:gt` is `:gt` on the other.
(The one-dimensional point algebra below is the same mathematics the cardinal
directions project onto; the two calculi share it as a fact about ordered axes, not as
code, and neither reads the other's vocabulary.)

Relative directions are **stored as ordinary sentexes** — the nine named binary
predicates (`leftOf`, `frontRightOf`, `sameRelativePositionAs`, …), plus four derived
predicates (`leftwardOf`, `frontwardOf`, …) that each name a *disjunction* of them: a
leftward component, whatever the front-back one.  The things related are ordinary
individuals; nothing about them is special, and nothing declares a viewpoint, because
the context is the viewpoint.

The calculus reads every asserted relation visible from a context into a
qualitative constraint network — `{[a b] → #{possible base relations}}`, an unrecorded
pair meaning "unknown", i.e. all nine — and `qcn/path-consistent` tightens it to a
fixpoint.  The prover then answers a goal `(P a b)` by **entailment**: it holds iff
every relation still possible between a and b satisfies P, `possible ⊆ denotation(P)`.
So `(leftOf A B)` and `(leftOf B D)` entail `(leftOf A D)`, and with it the weaker
`(leftwardOf A D)`.

An emptied constraint anywhere means the asserted relations are unsatisfiable, and then
*no* goal of this calculus is answered in that context — an inconsistent theory should
not be mined for conclusions.  Since the frame is the context, an inconsistency is
confined to the frame it was stated in.

**Soundness.** Path consistency is sound but not in general complete, so an entailment
reported here is real while a *non*-entailment means "not provable", never "provably
false" — the same open-world reading `argIsa` and `exceptWhen` take.

The vocabulary ships in `kb/upper/SpaceContext.txt` beside the topology, the compass and
the distance scale — all of them are *about* space, so CoreContext keeps only the
grammar they are declared in.  The prover is **opt-in** on top of it: register it with
`vaelii.core/add-prover`, and until then a KB stores and retrieves relative directions
as ordinary facts without paying for the network.

Unification, pattern matching against the indexed store, and backward chaining.

Matching is *type-aware*: a unary type predicate is matched over the subtype
closure, so an antecedent `(animal ?x)` is satisfied by a stored `(dog Fido)`.
This is how increasing an individual's specificity never loses the reasoning
that applied to its more general types — we consult the genl closure at match
time rather than materializing supertype facts.

Incremental forward-chaining match — a TREAT-style alpha network.

The reference forward chainer (`vaelii.impl.chain`) is semi-naive: a new fact seeds
the agenda, candidate rules are found by the rule index, and each candidate's
non-trigger antecedents are re-joined against the store on every assert.  That
re-join goes through `res/match-pattern`, which walks the **count-aware trie** —
and the trie narrows strictly left to right, so a non-trigger antecedent with a
*leading variable* (`(parentOf ?x Pi)`, the second half of a grandparent join)
can only be answered by scanning the whole `parentOf` extent.  That scan is O(N)
in the fact count, once per assert — the grandparent chain measured
6.4ms/assert at n=200 and 10.3ms/assert at n=400, a textbook quadratic load.

This namespace keeps **alpha memories** in RAM — the stored facts grouped by
functor and indexed by argument value — and answers a non-trigger antecedent with
a hash lookup on its most selective ground argument instead of a scan.  A leading
variable no longer forces a full extent walk: `(parentOf ?x Pi)` reads the bucket
of facts with `Pi` in position 2 directly.

## Correctness by reuse, not by reimplementation

The one and only novelty here is *which stored facts a non-trigger antecedent
finds*.  Everything else — the semi-naive agenda, the trigger match (`match1`),
context placement, `exceptWhen` blocking, the definitional checks on the derivation
path, justification dedup, functional-equality twins, the depth guard — is the
reference's, reached by binding one seam (`chain/*matcher*`) and calling
`chain/chain-all` unchanged.  So the network cannot diverge in *any* of those; it
can only diverge in the match, and `rete-match-pattern` is written to return the
**identical set** `res/match-pattern` returns — same belief filter, same
polarity check, same symmetric mirror, same subtype fan-out, same `?ctx` binding —
differing only in the candidate source (a RAM bucket, a superset of the trie hits,
filtered by the identical `unify`).  `rete_oracle_test` pins that equality directly
(per pattern) and end to end (the derived sentex + justification sets over randomized
assert/retract sequences must match the reference `chain`).

## The alpha memories

A per-KB atom, `{:by-functor {f {:all {id sentex}
                                  :by-arg {[pos val] {id sentex}}}}}`.  Only ground
**facts** live here (rules are matched by the rule index, not as facts, and never
appear among a fact pattern's trie hits).  Belief is *not* baked in: a datum stays
in its memory when it is defeated or superseded, and `in?` is consulted at read
time exactly as `match-one` does — so a belief flip needs no memory update, and the
only structural mutations are a stored fact arriving (`kb/create-sentex`) or leaving
(`integrate/sentex-removed!`), routed here through `vaelii.impl.observe`.  Subtype
and symmetric resolution also happen at read time (over the live taxonomy), so a
`genl` or `symmetric` edge change needs no memory update either.

See docs/inference.md, "Incremental rule matching".

Symbolic (schematic) equational rewriting — the oriented term-rewriting half of
equality, the gap docs/equality.md leaves open.

A schematic equation `(equals L R)` with variables — `(equals (fatherOf (fatherOf
?x)) (grandfatherOf ?x))` — is not a merge of two symbols (that is the partition,
docs/equality.md) nor a ground reifiable-NAT compound (that reifies to symbols,
docs/nat.md).  It is a **rewrite rule over a schema**: oriented into a terminating
reduction `L → R`, it lets a term be normalized so that a stored `(parentChain
(fatherOf (fatherOf Tom)))` and a query `(parentChain (grandfatherOf Tom))` meet at
one normal form.

## Orientation and termination

An equation is oriented by a **reduction order** — the Knuth-Bendix order `kbo>`
with unit weights — so rewriting strictly decreases every term at each step and
therefore terminates, whatever the rule set and without any confluence/completion
argument (`orient`).  The heavier side (by `term-size`) rewrites to the lighter; an
**equal-weight** pair is oriented by a fixed symbol precedence (root, then
lexicographically on the arguments), so a shape like `(f (g ?x)) = (g (f ?x))`
orients where a size-only rule would refuse it.  Both are gated by the variable
condition (`var-dominates?`), which keeps the order stable under *every*
substitution.  Only a **permutative** equation — `(rel ?x ?y) = (rel ?y ?x)`, which
no term order can orient — or one whose variable condition fails both ways is
refused (`orient` returns nil).

## What normalizes, and what does not

Rewriting applies to **terms in argument position** — the denoting terms a
schematic equation is about — never to a top-level predication (`normalize-sentence`
keeps the sentence's functor and rewrites each argument).  `fatherOf` the function
symbol and `fatherOf` a predicate are the same symbol; protecting the predication is
what stops a rule about the *term* `fatherOf(fatherOf(x))` from rewriting a *fact*
that merely happens to share the shape.

This namespace is **pure**: it takes the oriented rules as data and knows nothing of
the store, the taxonomy, or belief.  The taxonomy caches the active oriented rules
(belief-following, like the equality partition), `vaelii.impl.kb` threads
`normalize-sentence` into `rewrite-term` so migration and query both see one normal
form, and `vaelii.impl.special` justifies each rewritten twin — the same
belief-following machinery ground congruence already uses.  Bottom layer: it
requires only `vaelii.impl.sentex`.

A rule *is* a sentex — same structure (sentence + context), different indexing.
Its sentence is an implication:

  (implies (and <antecedent> ...) <consequent>)     ; single antecedent needs no `and`

Antecedents and consequent are sentence patterns that may contain variables.
Rules are indexed by their antecedent/consequent predicates (see the index
store) so forward chaining finds candidate rules without scanning, and — being
ordinary sentexes — they get handles, TMS support, and retraction for free.

Rules must be range-restricted: every consequent variable appears in some
antecedent, so a fired consequent is ground.  The one exemption is a **head
existential** — a consequent variable explicitly marked `(exists ?y C)`, which
forward firing skolemizes to a deterministic constant (docs/skolem.md); range
restriction permits only the marked variable and still rejects any *accidentally*
unbound one.  The same closure is required of an `exceptWhen` exception, which is a
query rather than a conclusion but must be ground for the same reason (checked at the
assert layer via `sentex/check-exception-closed`).

Somewhere safe to be wrong.

A **sandbox** is a scratch microtheory of one browser session's own, hung below
`WellContext` so it sees the whole shipped ontology and nothing shipped sees it.  A
reader can therefore use every type, every relation and every rule the KB ships, and
cannot damage any of them: their content is visible only from inside, and one control
takes all of it away again.

Why that shape and not a permission system: visibility here is *logical*, not
administrative.  `genlContext` already decides what a context can see, and hanging the
sandbox at the bottom of the spindle gives exactly the asymmetry wanted — everything
flows in, nothing flows out — with no new concept and nothing to enforce.  A shipped
rule firing over sandbox facts places its conclusion **in the sandbox**, because
placement is the maximal common descendant of the rule's context and the antecedents'
(docs/contexts.md), and the sandbox is the only context below both.  So the derived
content is inside the thing that gets discarded, without anything arranging for that.

Three facts about the lifecycle:

- **The context is created on the first write, not on the first page.**  A reader who
  only looks costs the KB nothing, and a KB full of empty sandboxes would be a KB with
  a `genlContext` edge per idle visitor.
- **The session id is in the context name**, so two readers of one process never share
  one.  It is minted into a cookie by `wrap-session` and validated on the way back in —
  a name is being built from it, and a name built from unvalidated client input is an
  injection.
- **Reset is a real teardown**, not a flag: every sentex in the extent goes through
  `edit`'s `:remove`, and the `genlContext` edge with them.  The edge is not in the
  extent — `genlContext` is a forced-decontextualized predicate, so it is stored in
  `UniverseContext` — which is why it is fetched by hand rather than swept up with the
  rest.

Promotion — moving something out of a sandbox into a context that outlives it — is
deliberately not here.  A sandbox is a dead end, and a dead end that cannot be
half-escaped is easier to reason about than one with a door in it.

Scenario extraction over a qualitative constraint network — turning "here is what is
still possible" into "here is one way it could be".

Path consistency leaves a *set* of relations on every pair.  That is the right answer to
what is entailed, and the wrong shape for a caller that wants a concrete arrangement: a
drawing of the regions, a timeline of the intervals, an example to show someone.  A
**scenario** is one consistent choice of a single base relation for *every* pair — a
singleton-valued network that survives path consistency, and so an arrangement nothing
believed rules out.

The search is ordinary backtracking, with the two refinements that make it bearable:
**fewest possibilities first**, so the most constrained pair is decided while it is still
cheap to be wrong about it, and **re-tighten after every choice**, so a decision that
empties some *other* pair is caught at once rather than at the leaf.

**Calculus-generic.**  It takes a `vaelii.impl.qcn-kb` calculus, so it works for RCC-8
topology, cardinal direction, Allen's intervals, the point algebra and anything added
later, with no line of it aware of which.  Everything it needs is on `qcn` and `qcn-kb`'s
public surface: the network, its nodes, a constraint, and the pass.

**Deterministic.**  The same believed facts yield the same scenario every time, and two
KBs built by asserting the same facts in a different order yield the same scenario as each
other.  Both orderings the search makes — which pair to decide next, and which relation to
try first — break their ties on **content**: nodes and relations are ordered by how they
are written, never by a handle id or by map iteration order.  Handles are allocated in
assertion order, so keying on one would smuggle that order into the answer, which is what
the whole engine forbids.

**The count is exponential**, so nothing here enumerates eagerly.  `scenarios` is a lazy
sequence — one scenario costs one path down the search tree, not the tree — and takes a
`:limit` for a caller that would rather say how many it wants than remember to bound the
sequence itself.  See docs/scenario.md.

kb/CoreContext.txt        the vocabulary head (see vaelii.impl.core-context)
kb/upper/<C>.txt          definitional layers, between Core and Universe
kb/middle/<C>.txt         theory layers, between Universe and Well

Ontology KB files: declarative content held as **plain text on the classpath**
rather than as code.

A KB file is a list of ordinary vaelii sentences — one s-expression each, with
`;;` line comments and blank lines allowed — named for the context its sentences
assert into, and grouped **term-centrically**: every sentence about a vocabulary
term sits together, and the terms run in natural sort order.  Nothing is
interpreted here that `assert` would not interpret anyway: a rule is just a
sentence carrying an `implies` / `set/*Rule` / `exceptWhen` wrapper.

The files live under `resources/kb/`, in a shallow tree that mirrors the context
spindle:

    kb/CoreContext.txt        the vocabulary head (see vaelii.impl.core-context)
    kb/upper/<C>.txt          definitional layers, between Core and Universe
    kb/middle/<C>.txt         theory layers, between Universe and Well

The file *name* is the context; the sub-directory is the layer.  What stays in
**code** (vaelii.impl.starter) is the *order* the files load in and the handful of
genuinely computed assertions.  Sentences read with `clojure.edn`, so a KB file is
data and can never run code.

The sentex — Vaelii's unit of knowledge: a sentence paired with the context it
holds in (sentence + context = sentex).

A *sentence* is a logical form written as a Clojure s-expression, e.g.
(parentOf Tom Bob).  Ground (all constants) or a *pattern* with variables like ?x.
A *context* names the situation / assumption frame it is asserted within.

The structural connectives `not`, `implies`, and `and` are **canonicalized into
the record** rather than left as data: a sentex carries a `truth` (`:true` /
`:false`, with double negation eliminated), and — for a rule — a decomposed
`antecedent` (vector of patterns) and `consequent`.  So the connectives never
reach the inverted **term index** (their heads are stripped, even nested inside a
rule — see `content-forms`), and the positional **trie key** drops the
`implies` / `and` rule frame; a negative literal keeps its `not` there as its
*polarity*, so a rule concluding `(flies ?x)` and one concluding `(not (flies ?x))`
get distinct keys.

Beyond the connectives, a sentence is put into a **canonical form** so that
logically identical knowledge is stored once:

  * **canonical variables** — a rule's variables are renamed `?var0`, `?var1`, …
    by first occurrence in canonical order, and `:varmap` maps them back to what
    the author wrote (`{?var0 ?x}`), so display can restore the original names.
  * **canonical literal order** — a rule's antecedents are sorted by a
    *structural* order (polarity, arity, ground arity, variable degree, shape),
    falling back to a lexical comparison of constants only as the last resort.
    Variables compare by their canonical *index*, never by name.
  * **symmetric arguments sorted** — `(siblingOf Bob Ann)` and `(siblingOf Ann Bob)`
    canonicalize to one sentex when `siblingOf` is declared symmetric.
  * **comparison siblings folded** — `greaterThan` is stored as `lessThan` with
    its arguments reversed, so only the `<` direction is ever stored.
  * **comparison chains collapsed** — `lessThan` is variable-arity, and chained
    comparisons in a rule merge: `(lessThan ?a ?b)` + `(lessThan ?b ?c)` becomes
    the single literal `(lessThan ?a ?b ?c)`.  `different` gets **neither** fold:
    it is not transitive, so a merged chain would claim more than was asserted.

An `exceptWhen` exception does not touch the rule record: it is stored separately as
a meta-sentex naming the rule by handle (see the `RuleSentex` field notes below).

`:sentence` holds the canonical, readable form for display and matching.

A sentex is one of two records — `AtomicSentex` (an atomic sentence: a fact, a metadata
declaration, a query pattern) or `RuleSentex` (an implication) — so an atomic sentex does
not carry the rule-only slots (there are 100M+ of them), and each still round-trips
through nippy with its type intact.

Headless EDN-over-HTTP daemon: one JVM owns one KB and serves it to remote clients
(`vaelii.impl.client`).  A thin reitit-ring + jetty layer over `vaelii.core`, the
network dual of the in-process API.

**Wire format is EDN.**  A sentence is a symbol s-expression — `(dog Fido)`, `?x`,
`(genl dog animal)` — which EDN round-trips losslessly; JSON would mangle the symbols.
The body of every call is `{:op <keyword> :args [...]}`, and the reply is
`{:ok true :result …}` or `{:ok false :error "…"}`.  EDN is read with
`clojure.edn/read-string` (never `clojure.core/read-string`), so an untrusted body
cannot evaluate code — EDN has no reader-eval.

**The daemon is the single writer** (docs/storage.md, the single-writer contract): it
owns the one process allowed to mutate the store, so it serializes every op through
one monitor.  Concurrent client writes therefore apply one at a time and cannot
interleave; reads pay the same lock, which is conservative but keeps the contract
simple.

**Only the allowlisted ops are reachable** (`ops`).  Each is a `vaelii.core` fn with
the KB supplied by the daemon — the client sends only the op and the remaining args —
so no client can reach an arbitrary var.  Sentex records in a result are projected to
plain maps before they hit the wire (the `sentex`-map contract), so the client reads
them back without the `impl` record class.

Belief settling: relabel the TMS, resolve soft contradictions on the one axis
(defeat-class), report the represented dilemmas, and run the `exceptWhen`
re-check queue to a joint fixpoint with belief.

Top engine layer (kb <- checks <- special <- integrate <- chain <- settle <-
vaelii.core): settling reads believed content (kb), garbage-collects what a newly
blocked justification was supporting (integrate's removal choke point tears it
down), and re-derives what a released exception was suppressing (chain fires it
again).

Head existentials: the deterministic constant a rule head `(exists ?y C)` fires to.

A rule head `(exists ?y C)` (docs/skolem.md) leaves `?y` unbound after the antecedent
substitution.  Forward firing replaces it with a *deterministic* skolem constant so the
semi-naive fixpoint terminates: the same `(rule, antecedent-binding)` must produce the
same constant, or a re-derivation would mint a new one each round and never converge.
The constant is a NAT `(SkolemFn <rule-handle> <exist-index> <frontier-values…>)` routed
through the ordinary reify path — `nat/reify-or-mint-nat` dedups it against
`termOfUnit`, so re-firing on the same binding resolves to the one constant.  A single
skolem function reified per-argument (rather than a per-rule function name) means one
lazy `reifiableFunction` declaration turns the whole mechanism on, and the frontier
values in the arguments key determinism.

A namespace of its own because it has **two callers on two layers** and belongs to
neither.  The write path asks `has-existential-head?` when a rule is asserted, and
declares the reifiable function then, so a rule that fires during its own assert already
finds it; the forward chainer (`vaelii.impl.chain`) calls `skolemize-conclusion` at each
firing.  Its own vocabulary is rules and firings — rule handles, frontier variables, a
substituted conclusion — so it is not part of `vaelii.impl.nat`, which knows about
reified terms and nothing about rules; minting is only *how* it makes the constant.

The mint itself is a full assert, one layer above this one, reached through
`vaelii.impl.wiring` — which is where the reason it cannot be a require is written down.

The seam to an external solver (ultimately an ASP/clingo backend) for assigning
truth at the *edges* — the defeasible nodes that a set of soft, prioritized
contradictions leaves genuinely undecided.

Design constraints (see docs/nmtms.md):

* Most of the KB is monotonic / default-true with no conflict; only the edges are
  contested, so a Program covers just the contested defeasible nodes.
* Known-true content (:monotonic) is never sent — it is the fixed
  background the solver assumes, not something it decides.
* Contradictions are *soft and prioritized*: a solve never fails.  Instead the
  solver reports which contradictions it could not satisfy (their sentences are
  the result), highest priority first.

* **A solve is order-independent.**  Which side of a tie loses may not depend on
  when anything was asserted — see `content-key`.  This is the engine-wide
  invariant (docs/nmtms.md): the same knowledge, given in any order, must yield
  the same beliefs.

A `Program` is a self-contained description a real backend renders to ASP.  This
namespace ships only a deterministic local *stub* solver; a real backend is a
future plug-in registered with `core/set-solver`.

RCC-8 qualitative spatial reasoning — a relation algebra over the generic constraint
network in `vaelii.impl.qcn`, alongside the cardinal directions of
`vaelii.impl.orientation` and the interval time of `vaelii.impl.interval`.  This one is
topology: whether two regions touch, overlap or nest, saying nothing about which way
they lie.

The eight RCC-8 base relations between two regions are jointly exhaustive and
pairwise disjoint, so exactly one of them holds of any pair:

  :dc    DC    disconnected
  :ec    EC    externally connected (touching, no shared interior)
  :po    PO    partially overlapping
  :eq    EQ    equal
  :tpp   TPP   tangential proper part      (x inside y, touching the boundary)
  :ntpp  NTPP  non-tangential proper part  (x strictly inside y)
  :tppi  TPPi  the converse of TPP
  :ntppi NTPPi the converse of NTPP

Spatial knowledge is **stored as ordinary sentexes** — the eight named binary
predicates (`nonTangentialProperPart`, `externallyConnected`, …), plus six derived
predicates (`partOfRegion`, `regionOverlaps`, …) that each name a *disjunction* of
base relations.  Regions are ordinary individuals; nothing about them is special.

`region-network` reads every asserted spatial relation visible from a context into a
qualitative constraint network — `{[r1 r2] → #{possible base relations}}`, an
unrecorded pair meaning "unknown", i.e. all eight — and `qcn/path-consistent`
tightens it to a fixpoint.  the prover then answers a goal `(P r1 r2)` by
**entailment**: it holds iff every relation still possible between r1 and r2
satisfies P, `possible ⊆ denotation(P)`.  So `(nonTangentialProperPart A B)` and
`(nonTangentialProperPart B C)` entail both `(nonTangentialProperPart A C)` (the
composition table pins the pair to `#{:ntpp}`) and the weaker `(partOfRegion A C)`
and `(regionOverlaps A C)`, whose denotations are supersets of it.

An emptied constraint anywhere means the asserted network is spatially inconsistent,
and then *no* spatial goal is answered — an inconsistent theory should not be mined
for conclusions.

**Soundness.** Path consistency is sound, and decides RCC-8 over its maximal
tractable subclass; on the full language it can leave a network path-consistent yet
globally unsatisfiable.  So an entailment this prover reports is real, but a
*non*-entailment means "not provable", never "provably false".  That is the same
open-world reading `argIsa` and `exceptWhen` take, and it is what story-scale
networks need.

The vocabulary ships as `kb/upper/SpaceContext.txt`, an *upper* context rather than
the vocabulary head: these fourteen predicates are *about* space, so CoreContext keeps
only the grammar they are declared in (`binaryPredicate`, `comment`) and a KB carries
the subject only if it loads the layer.  The prover is **opt-in** on top of that —
register it with `vaelii.core/add-prover` — so a KB can store spatial facts and
retrieve them as ordinary facts without paying for the network.

Opt-in `clojure.spec` contracts for the public `vaelii.core` API.

The engine already validates the *content* of what it stores — naming invariants,
well-formedness, disjointness (`vaelii.impl.naming` / `vaelii.impl.wff`).  These
specs guard the other side: the *shape* of the arguments a caller passes, the
option and budget maps especially, so a typo like `{:strength :monotone}` or a
string where a millisecond count belongs is rejected at the door with a spec
explanation rather than surfacing as a downstream error.

Nothing here runs unless a caller opts in with
`(clojure.spec.test.alpha/instrument public-syms)` — instrumentation is a
dev/test tool, so shipping the specs costs a populated registry and no more.  They
double as machine-checked documentation and as generators for property tests.

The `s/fdef`s name their targets by fully-qualified symbol, so loading this
namespace does not load `vaelii.core` — the specs register against the public var
names, which are the stable contract, independent of how the implementation is
split across `vaelii.impl.*`.

Coverage is the whole shape-carrying surface: every entry point that takes a
handle, a context, a level, a strength/direction, or one of the option / budget
maps.  The pure taxonomy reads (`genls`, `context-up`, …) are specced too, since a
wrong-arity call to one of them is exactly the kind of mistake instrumentation
should surface early.

The special-predicate dispatch table: what each functor the engine interprets
*means* to the derived state around the store, stated once, with both halves of
every meaning side by side.

A special predicate needs behaviour in four places — reflecting a stored sentex
into the caches, the removal mirror, `recover`'s cache-only replay, and `wff`'s
per-functor well-formedness check — and the compiler cross-checks none of them, so
the enumeration lives once here: `entries` maps each functor to its arms,

  :integrate    (fn [kb sentex handle])  reflect a newly stored sentex into the caches
  :disintegrate (fn [kb sentex])         the mirror, reference-counted on (:id sentex)
  :rebuild      (fn [tax sentex])        recover's cache-only replay — no re-check
                                         posting, no migration, no universal lifting,
                                         because the store already holds what those
                                         side effects produced
  :wff          (fn [tax sentence])      structural well-formedness (vaelii.impl.wff
                                         keeps the check fns; the table points at them)
  :derived?     bool                     the :integrate arm also runs on the
                                         derivation path (see `integrate-transitive`)

and `check-entries` refuses an asymmetric entry **at namespace load**, so an
add-side arm without its removal and rebuild halves is a build failure rather
than a cache that drifts on the first retraction or restart.

Because the arms are where a special predicate's whole behaviour lives, the
machinery those behaviours need lives here too: the exception re-check queue the
taxonomy arms post to, the universal-predicate lifting, and the equality
migration.  Third layer of the engine stack (kb <- checks <- special <-
integrate <- chain <- settle): everything here reads kb and checks, and the
store-mutation choke points in `vaelii.impl.integrate` sit directly above.

A starter common-sense KB: a documented, **schema-only** upper + middle ontology.
It loads the CoreContext vocabulary (vaelii.impl.core-context), then the starter's own
contexts, each a KB file on the classpath under resources/kb/:

  * upper (definitional — between Core and Universe): what things *are*, always
    true, like `genl`.  Split by domain, one context each:
      - AbstractContext.txt — the abstract type skeleton (physical/intangible and
                              their kinds) + the structural relations partOf/locatedIn.
      - OrganismContext.txt — the biological taxonomy + its disjointness.
      - LifeContext.txt     — the organism relations (parentOf, siblingOf, flies,
                              mortal, birthYearOf, olderThan, …) with argIsa + metadata.
      - SocietyContext.txt  — the social relations (marriedTo, likes, owns).
      - MeasureContext.txt  — the theory of measurement: the two measure terms, the
                              dimensionOf/conversionFactor table with the units that
                              fill it, the comparisons, and weightOf / heightOf.
      - SpaceContext.txt    — qualitative space: RCC-8 region relations (eight base
                              + six derived) and cardinal directions (nine + four).
      - TimeContext.txt     — qualitative time: Allen's interval relations (thirteen
                              base + seven derived), plus the length / totalDuration /
                              overlapDuration vocabulary the arithmetic computes over.
  * middle (theory — between Universe and Well): how the definitional things
    *interrelate*, where several overlapping theories can coexist.
      - AnatomyContext.txt   — what kinds of thing have what kinds of part.
      - BiologyContext.txt   — birds fly by default except penguins; living things
                               are mortal; flight enables travel; sleep is what the
                               theory is willing to assume.
      - KinshipContext.txt   — grandparentOf, ancestorOf, olderThan, and parenthood
                               from maternity and paternity.
      - MereologyContext.txt — a part is located where its whole is; owning a whole
                               entails owning its parts.
      - SizeContext.txt      — comparative size: stated between kinds, computed
                               between objects from their measures.
      - SocialContext.txt    — what acquaintance follows from; employment as one way
                               of belonging.

The context spindle is a five-layer axis, most general (top) to most specific
(bottom): CoreContext, the upper layer, UniverseContext, the middle layer,
WellContext.  Each upper/middle file wires itself into the axis, so the topology is
data.  **No cast and no contingent facts ship**: the starter is a schema, and
contingent data (a cast, worked examples, the Aesop fables) belongs below WellContext
and lives in the tests that need it.

The unit table is the one place individuals ship, and it applies that rule rather
than excepting itself from it: a minute is sixty seconds by stipulation, so the
factor is vocabulary and not a measurement anybody took.  MeasureContext.txt states
the test it holds a unit to.

What stays in code here is the *order the layers* load in — loading order is logic,
the definitional layer must precede the theories that reason over it — and the one
computed batch (every type is also a unaryPredicate).  Within a layer, every
context file present is loaded (discovered from the classpath), so adding a KB is
dropping a file in kb/upper/ or kb/middle/, no code change.

A **simple temporal problem** — the metric half of time, where the qualitative calculi
say only which of two things came first.  A constraint is a bound on the *gap* between
two instants,

  lo ≤ t(Q) − t(P) ≤ hi

and a set of them is closed by all-pairs shortest paths over the distance graph they
describe.  The closure answers the tightest gap the constraints entail between *any* two
instants, including pairs nobody wrote a constraint for, and a **negative cycle** in that
graph is the proof that no assignment of times satisfies them all.

This is not a relation algebra and it is deliberately not forced through
`vaelii.impl.qcn`: there is no finite set of jointly-exhaustive base relations here, and
no composition table — the constraint on a pair is an interval of the reals, composition
is addition and tightening is `min`.  So it is its own small algorithm, written the way
`qcn` is written: **pure data in, pure data out**, knowing nothing about a KB, with the
KB reading and the prover in their own marked section below.

**Constraints are measures**, not bare numbers.  A stated one is the ordinary fact
`(temporalDistance P Q M)` where `M` is a `(QuantityFn N Unit)` for an exact separation or
a `(QuantityIntervalFn Lo Hi Unit)` for a bounded one, and a negative magnitude says Q
falls before P.  Every magnitude normalizes through `provers/normalize-quantity` against
the KB's `dimensionOf` / `conversionFactor` table, so the arithmetic happens in the
dimension's base unit and an answer is rendered back in that same unit — exactly the
contract `vaelii.impl.duration` follows, so a separation and a duration are written the
same way and compare directly.  Constraints spanning more than one dimension are refused
rather than mixed.

**Bind or check**, like `EvaluateProver` and the duration arithmetic: an open measure is
bound to the tightest separation entailed, and a ground one is *entailed* exactly when the
derived bound is contained in it — a stated bound is a weaker claim than the derived one,
so the derived one implies it.

**The bridge to the interval algebra** is `(startOf I P)` / `(endOf I P)`, which name an
interval's two bounding instants.  With them a metric fact and an Allen relation are about
the same thing, and `allen-narrowing` reads the closure back as constraints on the
*interval* relations: if the closure puts A's end strictly before B's start then A is
`before` B, and so on for all thirteen.  It narrows and never widens — it returns relation
sets for a caller to intersect into an interval network, and mutates nothing.

`vaelii.impl.duration` is the other consumer: `overlap-window` bounds how long two
intervals overlap from their endpoints alone, which is what turns an indefinite overlap
into a real figure.

The prover is **opt-in**: register it with `vaelii.core/add-prover`, and until then a KB
stores and retrieves `temporalDistance` facts as ordinary facts without paying for the
closure.  The vocabulary ships in `kb/upper/TimeContext.txt` either way.  See
docs/stp.md.

Assumption strengths on beliefs, and the derived *defeat-class* that resolves
soft contradictions.

There are exactly two classes, and a user asserts content at either:

  :monotonic  known-true; indefeasible; never sent to a solver.
  :default    defeasible; the common case — most of a common-sense KB.

They form a total order  monotonic > default.  In a contradiction the member of
*least* class is defeated; :monotonic ('known true') content is never sent to a
solver.

Derivation adds no class of its own.  A justification confers `min(its own
strength, the weakest of its antecedents' classes)`, and a rule's own strength is
read off its defeasibility: a **bare rule** confers :monotonic — it adds no
defeasibility, so its conclusion is capped by whatever it rests on — and a
**`set/defaultRule`** confers :default, because it introduces defeasibility.  So a
bare rule over :monotonic facts concludes :monotonic (it *is* monotonically
entailed), and the same rule over a :default premise concludes :default.

There are exactly two classes; do not add a third.  Undercutting a defeasible
generality is done with `exceptWhen` (docs/exceptions.md) — the excepted rule states
its own exception and simply does not fire — so no intermediate class is needed to
out-rank one belief with another.

The inline-SVG primitives the term page's concept graph is drawn with: a node, an
edge, an arrowhead, and the arithmetic that lays out a row, a column or a ring.

**No graph library.**  The browser ships two JavaScript files and this adds none — a
layout that is a fold over a row of boxes is a dozen lines, and a dependency that drew
it would be the largest thing the client loads.  Nor a shell-out: a page that renders
by starting a process is a page that cannot be served.

Everything here is **pure** — no KB, no access facade, no belief — so it is tested on
hand-built maps.  What a node *means* is the caller's: it supplies the term, the
colour class, the link and the tooltip, and this decides only where the box goes and
what shape it is.

Coordinates live in one flat user space and may be negative; `scene` crops the
`viewBox` to the union of what was actually drawn, so a sparse graph is centred rather
than adrift in a fixed canvas and a long snake_case label is never clipped.  Every
number reaching an attribute is a **long**: Clojure's `/` yields a ratio, and `1/2` in
an SVG attribute is not a coordinate.

estimate(node) = Σ literal-cost(Lᵢ)                     what the conjunction costs
               + size-penalty × |literals|              shorter conjunctions first
               + depth-sign × depth-weight × Σ dᵢ       rewriting allowance left
               + tree-sign  × tree-weight  × tree-depth search-tree level

The node engine's search **policy** — one additive estimate whose terms carry signs the
caller picks, so `vaelii.impl.inference` searches breadth-first, depth-first or best-first
without a second driver.  The frontier is a priority queue precisely so that changing a
number is enough; this namespace is that number.

    estimate(node) = Σ literal-cost(Lᵢ)                     what the conjunction costs
                   + size-penalty × |literals|              shorter conjunctions first
                   + depth-sign × depth-weight × Σ dᵢ       rewriting allowance left
                   + tree-sign  × tree-weight  × tree-depth search-tree level

**The base term is the KB's own cost model, not a second one.**  It is
`plan/explain`'s per-literal estimate summed — the count-aware trie model with sideways
information passing that already orders every join in the engine, so a conjunction is
costed here exactly as `core/query-plan` reports it.  One model, two readers; a node
ordering that disagreed with the plan it is about to run would be a cost model arguing
with itself.

**The signs are the whole personality of the search.**  Σ dᵢ is what a node is still
*permitted* to rewrite, so a negative depth sign prefers the node with the most room
left and a positive one the node closest to spending it — a node nearly out of
allowance is a node nearly ground, hence nearly answerable by facts alone.  The tree
term is the analogous choice over the search tree rather than the rewriting budget:
positive is level order, negative is a dive.

**Ordering is a cost decision and never a semantic one.**  Every tactician here
returns the same answer set; what differs is when.  `inference_tactics_test`'s
completeness sweep is the gate that keeps it that way, and the one mode that
deliberately returns fewer answers (`:first-result?`) says so in its own docstring and
is excluded from that sweep by name.  The join *inside* a node is ordered by
`plan/order` alone and never by the strategy, for the same reason: a complete search
has to visit the same literals whatever order the nodes pop in.

See docs/inference.md.

Cached transitive closures for the two transitivity relations at the heart of
common-sense reasoning:

  genl    relates unary *types*    (genl dog animal)   — the type hierarchy
  genlContext  relates *contexts*       (genlContext AContext BContext)     — context inheritance

Transitivity is not done with rules (too central, too hot); instead we store the
**direct adjacency** of each relation and answer the reflexive-transitive up/down
closure *on demand*.  `genls` is ancestors-incl-self, `specs` is descendants-
incl-self.

We deliberately do **not** materialize the full closure.  A materialized closure
is Θ(V²) for a deep hierarchy — a 10k-node `genl` chain stores ~50M pairs — so
building it incrementally makes a bulk load quadratic no matter how clever each
insert is: the representation itself is the cost.  Storing only the O(V+E)
adjacency makes an insert O(1) amortized and a closure read O(reachable-subgraph),
which is what a deep or bulk load needs.  Reads are memoized per closure
*generation* (bumped on every edge change), so a shallow hierarchy — where the
reachable subgraph is tiny — still answers each repeat read in O(1).

- **Insertion** records the edge in `:fwd` / `:rev` and, so cycle checks stay
  cheap, maintains a topological `:depth` potential (`edge x→y ⇒ depth[x] >
  depth[y]`).  No closure is touched.
- **Deletion** drops the edge from the adjacency and prunes any node left with no
  edge.  Depths are left as loose upper bounds — a deletion only relaxes the
  ordering, so the invariant survives untouched.
- **Cycle safety.** `genl?` / `sees?` answer reachability with an early-exit walk
  pruned by `:depth`: a real path `x → … → y` has strictly decreasing depth, so
  `depth[x] ≤ depth[y]` rejects the pair in O(1).  `wff` rejects `genl` /
  `genlContext` cycles up front, so the closures stay acyclic; `reach` guards with a `seen` set
  regardless, so a stray cycle terminates rather than being subtly wrong.

`closures` (the from-scratch materialized build) survives as the **reference
implementation** the on-demand reads are tested against — the oracle test in
`taxonomy_test` compares `genls` / `specs` for every node against it after every
random edit.

Context semantics: (genlContext Sub Super) means Sub *sees* Super's assertions, so a
context K sees a sentex in context Y iff Y is in genls-of-contexts(K).

## Edges are supported, and support is belief-sensitive

A relation is `{:support {[a b] {handle ctx}} :edges #{[a b]} :fwd {} :rev {}
:nodes #{} :depth {} :gen n}`.  `:support` records **every sentex that asserts an
edge**, keyed by handle with the asserting sentex's context as the value — handle
and context enter and leave together, so they cannot desync; a nil context means
the writer had none to record (a probe) and the edge constrains everywhere.
`:edges` is the *active* set the closures are computed from — an edge with
no believed supporter is not in it.  That distinction is what keeps three things
right:

- **Belief.** A defeated `(genl dog animal)` leaves the closure, so `isa?` cannot
  outrun belief.  Matching is belief-sensitive everywhere in the engine, the
  taxonomy included; `refresh-beliefs` reconciles after a relabel.
- **Reference counting.** The same edge asserted in two contexts is two sentexes.
  Retracting one must not remove the edge while the other still asserts it.
- **Idempotence.** Re-asserting an edge that is already active is a no-op —
  `activate` returns early rather than touching the adjacency at all.

## Equality is the third supported relation, and it is not a partial order

`rewriteOf` / `sameAs` / `equals` all feed one **equivalence** closure, so it is
stored as a partition — member → class, class → members and representative —
rather than as up/down closures.  It shares the `:support` discipline above and
nothing else: insertion is a union, and deletion can *split* a class, which no
union-find can undo, so it rebuilds the affected class from its surviving edges.
See the section below and docs/equality.md.

The same belief discipline reaches the four flat caches too — `disjoint`, the
disjoint metatypes and their members, the predicate properties, and `inverse`.
They carry no per-claim `:support` record of their own; their supporters are
reference-counted in the shared `:cache-support` map, and `refresh-beliefs`
reconciles each cache entry against belief exactly as `refresh-relation` does for
genl — an entry is active iff some supporter is stored *and* believed.  So a
defeated `(disjoint dog cat)` stops constraining, a defeated `(functional P)` stops
merging, and a defeated `(inverse P Q)` stops answering the swapped goal, the way a
defeated genl edge leaves the closure.  See docs/taxonomy.md.

A bidirectional **token dictionary** — `path-token ↔ int` — the first new durable
ground truth the dense (`:memory-columnar`) index rests on.

The columnar trie (`vaelii.impl.columnar`) labels its edges with `int` tokens rather
than boxed structured values, so it needs a stable `token → int` map and an `int →
token` inverse to decode a node's child labels back for `children`.  A *token* is
whatever a trie path level can be (`sentex/path`): a symbol (predicate / individual /
type / context), a number, a keyword (`:false` / `:rule`), `nil` (a rule's assumption
/ constraint slot), a `[::subterm k]` arity marker, or a whole literal list (a
`:false` body, a rule's antecedent vector).  They arrive already canonical from
`sentex/path` (the sentence went through `sentex/canon`), so the dictionary interns
them **as-is** — re-canonicalizing would turn a marker vector into a list and break
`sentex/subterm-mark?`, exactly as the current `KvIndexStore` relies on raw path
tokens as keys.

**Content-keyed, first-writer-wins.**  An id is allocated the first time a token is
seen and never changes; ids count up from 0 (array-friendly).  The id *value* depends
on first-encounter order, but the index's correctness does not — an id is an opaque
edge label the inverse map decodes — so a rebuild from the records (`reindex` / `recover`)
that re-interns in a different order yields an equal index (identical lookups), which
is the order-independence that matters.  A durable columnar index that persisted its
`int` edges would instead load this dictionary before reading them; that is the seam
Phase 2's durable variant uses.

**Keyed by Clojure equality, not Java's** — see `Key` below.  That is not a refinement;
it is what makes this dictionary answer the same questions the flat map it replaces
answers.

**Single-writer**, like the index it serves: the maps are mutated in place under the
one-writer contract, no atom.

The dropped-conclusion ledger: what the derivation path refused to store, kept as a
value a caller can read afterwards instead of thrown at whoever happened to be
writing.

A namespace of its own because of **who writes it**.  Two paths file entries and they
sit on opposite sides of the engine: the forward chainer
(`vaelii.impl.chain`) files a conclusion it dropped, and the prover registry
(`vaelii.impl.provers`) files an aggregate's numeric error — and the chainer is built
*on* the registry, so the registry cannot name it.  The ledger reads nothing from
either, only `(:violations kb)` and `(:chain-stats kb)`, so it sits below both and the
edge runs the one direction the layering allows.

Why a ledger rather than a throw: an entry is recorded from inside the semi-naive
fixpoint and from inside a relabel, and neither may abort — a definitional check that
aborted mid-fixpoint would leave belief half-computed, which is the failure the value-
first checks (`vaelii.impl.checks`) exist to avoid.  So a violation is *reported*, and
the run continues without the conclusion.

What the engine does with each term of its own grammar — the answer to "is this
declaration enforced?", which is otherwise only readable by grepping `special.clj` and
`checks.clj`.

The question exists because nothing about a declaration's *shape* says whether anything
reads it.  A naming invariant passes on anything correctly spelled, so
`(maxCardinality parentOf 2)` is a well-formed ternary fact, storable, believed, and
read by nobody — and a KB author gets identical silence from a constraint that is
enforced and one that was never implemented.  A roster is what turns that silence into
an answer.

**Population: CoreContext's own terms.**  Not every predicate in the KB — a domain
relation is *supposed* to be inert, and `(likes Fred Mary)` asks nothing of the engine.
CoreContext is the vocabulary microtheory, whose charter (see the header of
`resources/kb/CoreContext.txt`) is exactly "the engine-interpreted special predicates
and the predicate meta-ontology", and its file is term-centric: one `(comment <term>
…)` block per term.  So the terms it comments are precisely the grammar, and precisely
the set where "declared but unimplemented" is a defect rather than the normal case.

**Two classes, and the distinction is the point.**  `:enforced` means some code path
reads it and the KB will refuse, derive, or answer differently because of it — the
`:by` string says which path, and whether that path is keyed on this functor by name or
is a generic mechanism the declaration merely enrols in.  `:inert` means nothing does,
with `:why` recording that this is a decision rather than an omission: most of the
inert entries are *derived* predicate types, which exist so a KB can be queried for
what a mark implies, and are read by no check because the mark itself is what the
checks read.

**What keeps it honest** is `audit`, and two tests over it: a term CoreContext comments
with no roster entry fails, and a roster entry naming a term CoreContext no longer
comments fails.  So the next plausible-looking functor cannot land unimplemented in
silence, and a retired one cannot leave a stale claim behind.  The `:enforced` side is
cross-checked against `special/entries` as well, which is machine-readable: a functor
the table gives an arm to and the roster calls inert is a contradiction, not a matter of
opinion.

**Why the answer does not live in the ontology.**  A `(notEnforced P)` marker was the
obvious alternative and is self-defeating — it would be a declaration the engine does
not read, which is the exact defect this namespace exists to find.  Putting it in each
term's `comment` prose is worse: nothing can check prose without matching strings, so it
would drift the first time a check was added and the sentence was not.  A roster in code
drifts too, but a test can see it drift.

A small reitit-ring web browser over a KB:

  /                 the upper ontology (contexts, types, core predicates, disjointness)
  /stats            KB-wide counts, contexts by size, and the reasoning-health ledgers
  /find?q=<pattern> the terms whose name matches, from the index's term roster
  /term?q=<term>    every sentex containing the term, grouped by the index root that
                    reaches it (functor / argument-position / context / term-index)
  /sentex/:id       a sentex (atomic or rule): its belief state (IN, or the why-not
                    reason — superseded / defeated / unsupported), supports, dependents
  /justification/:id    a justification: its supports (arguments) and dependent sentex
  /levels?q=<goal>  the lookup-to-query stack: what each of the 8 levels answers
  /edit             the multi-sentex editor (GET seeds it, POST saves) — a fragment
  /{term,find,levels}/rows   one more page of a capped list, as bare rows

Run it with `lein run -m vaelii.impl.web` (serves a starter-loaded KB on :3000).
Handlers are pure `request -> response`, so they are testable without a server.

Every page is answered twice over: as a whole document, and — when htmx asks, which
is every navigation and search — as the `#main` fragment that actually lands.  What a
page costs in KB reads is part of what this demonstrates, since the browser reads the
public surface alone and each read is a round-trip under `--attach`; see the `view`
section below and docs/web.md.

Well-formedness checks for the special predicates: genl / genlContext (the type and
context hierarchies), disjoint / disjointMetatype, and argIsa (argument types).
Each returns a seq of problem strings; `assert` throws if any are present.
Ordinary sentences are checked for argument *types* by checks/constraint-checks.

The per-functor check fns are defined here; **which functor gets which check is
not** — that dispatch is one arm of the special-predicate table in
`vaelii.impl.special`, so the functor enumeration lives in exactly one place and
a predicate added to the table without a `:wff` arm is visibly missing rather
than silently unchecked.  `special/wff-problems` is the walk.

Plus one check that is about a *rule set* rather than a sentence:
`negation-cycle` finds the cycle through negation that an `exceptWhen` exception
closes.  Two things can close one — a rule arriving, and a `genl` edge arriving
underneath rules already stored — and `checks` runs the search on both paths (see
the section at the bottom, and docs/exceptions.md).

The write path and the prover registry as the layers *beneath* them see it — the whole
inventory of calls the require graph cannot express, in one file.

Everything else in the engine is layered, and every edge is a static require the
compiler checks: kb <- checks <- special <- integrate <- chain <- settle <- vaelii.core.
Exactly two calls run the other way:

  `assert-sentence` — the full assertion path, called from `vaelii.impl.nat` (a reified
  NAT stores its `(termOfUnit K E)` map and its materialized types) and from
  `vaelii.impl.skolem` (a firing mints its witness).  Storing is a *whole* assert —
  naming, the definitional checks, the index, chaining, settle — so the write path runs
  chaining, and chaining calls back here to mint a constant (docs/skolem.md).

  `solve-goal` — the prover registry, called from `vaelii.impl.resolution` to discharge
  a deferred antecedent (`different` / `evaluate` / `unknown`).  Backward chaining is a
  leaf the registry dispatches to, and `unknown` runs the registry back over its own
  argument, so negation-as-failure is mutually recursive with the chainer that asked
  for it (docs/naf.md).

Both are genuine mutual recursion: the cycle is in the **behaviour**, neither is a
misplaced function, and no arrangement of the code removes either.  Why they are
gathered here rather than left at their call sites, what `lein lint`'s **E8** enforces,
and why each is a `delay` rather than a dynamic var — docs/namespaces.md, "The
layering".