# `improvise-incremental`: the reasoning

`crates/improvise-incremental` began as ADR 009 step 2 (improvise-t8ow, epic improvise-bw4p): the
plug. It holds the `Derived` trait, `Eager` (today's evaluator behind it) and the
differential harness every backend is checked with, and, from step 4 (improvise-u2le), the
first backend that keeps state, `Incremental` (section "Step 4" below). The step 2 sections
describe the trait and the oracle; they predate the backend. The decisions are the ADR's
(`context/adr/009-incremental-evaluation.md`). The evidence for each test is in
`context/test-evidence/improvise-incremental.md`.

## The shape

| item | what it is |
|---|---|
| `Derived` | the two things the evaluator reads: `value(key, agg)` and `raw_fold(partial)` |
| `Eager` | an owned `Model` plus its None categories; every answer is a call into `Model` |
| `Maintained` | a `Derived` that is told each `Edit`; `Eager` is one |
| `Edit` | one model mutation as data (set, clear, add or remove a formula, set a measure's aggregation) |
| `probes`, `Probe` | every question worth asking of a model, and a way to put it to any backend |
| `differential` | runs one edit sequence on a candidate and on `Eager`, comparing every probe at every step |
| `Divergence`, `Report` | what a failure names (step, probe, both answers) and what a pass compared |
| `Incremental` | the backend of step 4: maintained groups and occupancy; formulas and `Sum`/`Avg` still go to the model (later steps change that) |

## Interpretations

Clause 2 names the trait and says what it carries ("the formula result at a key, and the raw
fold of the cells that match a partial key") and nothing else. These are the readings taken.

1. **`Derived` lives in this crate, not in improvise-core.** The ADR says improvise-core
   "gains a trait". Putting it there changes an existing crate's source, which the brief for
   this step ruled out, and the brief was ambiguous about it. This departs from the accepted
   ADR's text, so it is flagged to the user and not decided here: improvise-bw4p.2 moves it
   (one file and a `pub use`, since the trait names only core types). While it sits
   downstream, core cannot read through it, which is the clause's point.
2. **Two methods, the minimum.** `value(key, agg)` is the formula result at a key, or the cell
   as stored or folded; `raw_fold(partial)` is the fold of matching stored cells. `agg` is
   `Aggregation`, the evaluator's own type. Hidden-item `covers`, totals and occupancy joined the trait
   in improvise-bw4p.3 (section "Step 4 groundwork"). A group is exercised: a stored key with one coordinate
   replaced by its item's group is a probe.
3. **`raw_fold` is never a formula, and `Eager` enforces it.** For a partial naming a formula
   target `Eager::raw_fold` is `None`; otherwise it is `evaluate_aggregated(partial, OverHidden)`,
   because the evaluator's own raw fold (`aggregate_raw`, `aggregate_cell_values`) is private to
   core. Calling it through the public path is exact for any partial that names no formula
   target. improvise-bw4p.2 exposes the raw fold from core so `Eager` stops going round.
4. **`Eager` recomputes formulas after every edit.** Production does it in `rebuild_layout`
   (`Model::recompute_formulas(none_cats)`), and an over-hidden read of a formula cell reads
   the cache it fills. So `Eager` carries the None categories of the view it stands for and
   recomputes under them after each edit, as a layout rebuild does.
5. **`Edit` is the vocabulary of the harness, not of the wire.** Five variants, each one
   public `Model` call. A later step adds variants for what it maintains (an item added, a
   category removed); the harness does not care which. An `Edit` fault reaches both sides of a
   differential alike, so it is pinned only where a direct `Eager` test reads the result:
   `ClearCell`, `AddFormula` and `RemoveFormula`, and `SetMeasureAgg` through the fold tests.
   `SetCell` is read by nearly every test.
6. **Values agree by float rules with every NaN one value** (`same_value`), the rule clause 3
   states for cell deltas, except the two zeros: they differ, since a drawn `-0.00` is not `0.00`
   and eager's `Min` and `Max` return the sign they were given. Clause 8 has its own tests
   for the sign of a zero sum.
7. **The `zset` dependency arrived with step 3**, as the cell delta (below).

## Step 3: the cell delta (improvise-5r8c)

`delta.rs` holds `DeltaValue`, `CellDelta = ZSet<(CellKey, DeltaValue)>`, `cell_delta` and
`moved_records`. `improvise-command`'s `apply_effects` reads them for the record tier and the
dirty flag (`context/code/command.md`). Evidence: `context/test-evidence/improvise-incremental.md`.
These are the readings taken, where ADR 009 clause 3 leaves a choice.

1. **`DataStore` logs, `improvise-incremental` builds the Z-set.** The ADR says the store
   "emits a `ZSet`", but core never depends on `zset` (clause 2). `DataStore::record_changes`
   turns on a `Vec<CellChange>` log (`None` while off, so an unwatched store keeps nothing),
   `drain_changes` empties it and `cell_delta` folds it. The log lives in the store, not in
   `Model::set_cell`, so every route that writes a cell is seen, including `RemoveCategory`'s
   sweep.
2. **`DeltaValue` canonicalises on construction**: every NaN becomes `f64::NAN`, `-0.0` becomes
   `+0.0`, and the order is `total_cmp` on the result, with numbers before text before errors.
   The inner value is private, so a non-canonical one cannot be built. Equality is the order's
   `Equal`, so `==` and `Ord` agree.
3. **`CellKey` is `Ord` by derivation**: the sorted coordinate pairs, compared as strings.
   Clause 3 calls this "the natural order of ids", which ADR 007's id form will change; the
   derive then moves with the key type.
4. **The record tier is the set of records a consolidated batch delta names.** A cell written
   and written back inside one batch cancels, as the old XOR did.
5. **The dirty flag needs two inputs the ADR does not name.** Besides a non-empty delta and
   the formula set, `document_config` stays (an `AddItem` writes no cell and the existing test
   requires it dirty) and the saved order joins, which no delta carries: `DataStore::reorders`
   counts `SortData`, and any logged insertion or removal dirties too, because a clear-then-set
   of one value nets to zero yet moves the cell to the end of the store (a same-item rename).
6. **`document_generation` and the wire are untouched**, and `Eager` and the `Derived` trait
   are not used: no backend consumes the delta yet. The differential for this step is the
   delta against the store it describes (`the_cell_delta_of_an_edit_is_...`), since there is
   nothing to compare with `Eager`.

## What the harness checks

`differential(model, none_cats, candidate, edits)` builds `Eager` over a clone of the model,
applies each edit to both, and after step 0 and after every edit asks both every probe. The
probe set **accumulates**: probes from the model at every earlier step stay asked, so a backend
that goes on answering for a removed formula diverges. A pass returns a `Report` of how many
states and answers were compared.

`probes(model)` takes the base keys (each stored key, and each with one coordinate replaced by
its item's group), every sub-partial of a base key dropping at most `MAX_DROPPED = 3`
coordinates plus the empty key, and each formula's target over each of those. Each key is asked
as an exact value, an over-hidden value and a raw fold. A fold dropping more than three
coordinates from a stored key is not asked about. `edit_probes`
adds the key an edit names, so a cleared cell is asked about after it is gone. A divergence
reads `divergence at step N: <probe>: eager <a> != candidate <b>`.

## Step 4 groundwork: what a view draws (improvise-bw4p.3, improvise-bw4p.4)

The subset probes above cannot see a drawn cell on a view with four or more None categories
(it drops more than `MAX_DROPPED` coordinates of a stored key), and the trait could not be asked
about hidden items, totals or occupancy. Both are closed. These are the readings taken.

1. **`Reading` is how a view reads.** The aggregation (`Aggregation::of` its None categories)
   and the hidden `(category, item)` pairs of `View::hidden_items`. `covers(cat, item)` is the
   predicate `GridLayout::evaluator` passes as its `covers`. It is a value, not a closure, so a
   probe can name it and a divergence can print it. A fold over a group or a spanned category
   leaves hidden members out; a read of a key naming neither does not (a hidden East still counts
   in `{Product=A}` when Region is None), while an occupancy count always leaves them out. The
   count follows the drawn items, not the value; `Eager` mirrors production in both.
2. **Three methods join the trait**: `covered(key, reading)` is `Model::evaluate_covering`;
   `total(key, over, reading)` is `evaluate_spanning`, a column total as ONE fold over the
   visible items of the omitted categories; `occupancy(partial, reading)` is ADR 009 clause 7's
   count by axis item: the stored cells matching `partial`, none of whose coordinates is hidden,
   where a coordinate naming a group matches every stored member of that group (a collapsed group
   is a remap, so the Coastal line of two visible members counts 2). A key naming a formula
   target has no stored cells and is not asked. "Has a value" (what `prune_empty` asks) is
   `covered(..).is_some()`, already probed.
3. **`drawn_probes(model, views, none_cats)` asks what each view draws**, built from the view's
   own `GridLayout` (pruned as production builds it): for every drawn cell the three subset
   questions plus `Covered` and `Occupancy`; for every column its `column_key` occupancy and, where
   `GridLayout::draws_totals` (the condition `grid_body` also reads), a `Total` over the row
   categories; for every row the occupancy of its cell key less the column coordinates. Lines
   carry the page coordinates, as a cell's key does, so a page is its own slice. A records view is
   skipped: its keys are synthetic `_Index`/`_Dim` coordinates naming no stored cell and it has
   no totals, while its stored keys are the subset probes' business. A view whose None categories
   differ from the oracle's is skipped, since `Eager` recomputes its formulas under one set (a
   backend keeping a cache per aggregation class is therefore not exercised on the others).
   `differential_in(model, views, ..)` adds them at every step; `differential` is that with no
   views. A view is a `View`, not a document, because the model holds none.
4. **`sub_partials` is polynomial**: it enumerates the sets of at most `MAX_DROPPED` dropped
   indices, not the 2^n masks. The probe set is unchanged for every key length (a test compares
   it with the old walk up to 12 coordinates, and counts it at 64). `MAX_DROPPED` stays: it
   bounds the subset probes, and the drawn probes carry the cells that drop more.
5. **The hidden fixture is a workbook the corpus now includes** (`hidden`): no shipped demo
   hides an item, so a backend wrong about hidden items would have passed the direct
   `Eager`-against-evaluator comparison as well.
6. **`Probe` is `Hash + Eq`**, so `Asked` deduplicates on the probe itself (`Aggregation` gained
   `Hash` in core for it).

## Step 4: the incremental backend (improvise-u2le)

`Incremental` (`incremental.rs`) is the first `Derived` that keeps state. It owns a `Model`
(the store) and `Shapes` (`shapes.rs`, the groups). `Maintained::apply` applies the edit to the
model, drains the store's change log into a `CellDelta` and feeds the delta to every shape. A
read asks a group, never the store, for what step 4 owns. The rest of this section is the readings
taken where clause 4 and clause 7 leave a choice; evidence is in
`context/test-evidence/improvise-incremental.md`.

1. **A shape is a set of category names, not a None list.** Clause 4 says "a group is the cell key
   minus the None categories". The trait is asked about keys of any category set (the harness
   drops up to three coordinates of a stored key), so the unit is the set a key names: a `Shape`
   maps the projection of a stored cell onto those categories to a `Group`, and a cell lands in
   it only if it has all of them. A view's None list is one of these sets. Clause 7's "one
   circuit serves every shape key with the same None list" holds trivially, since the sets are
   shared by every reader.
2. **A shape is built on its first read, by one pass over the store, and fed every delta after.**
   Clause 7 makes a new key's first build a sliced job under ADR 008's job runner. That runner
   does not exist, so the pass is synchronous and counted (`Meter::builds`, `built_cells`).
   Nothing evicts a shape. `Shapes` holds its map in a `RefCell` because `Derived` reads take
   `&self`; the cell is private to `shapes.rs` and no reference to it leaves a method.
3. **A group is a count, a count of numbers and a multiset** (`group.rs`). One update touches one
   map entry (O(log d)); the count and the multiset serve every function, so
   `SetMeasureAgg` rebuilds nothing. A read of several groups (a collapsed group, a total) folds
   their union without merging them: `fold_groups` sums the counts and takes the smallest of the
   groups' minima, the largest of their maxima, or the one value they share.
4. **Eager's rules are reproduced, not improved** (superseded for NaN and zeros by "Eager's math, fixed" below). An all-numbers group reduces; any other group
   is unanimous or `Error("mixed")`, so `Count` of a group holding text is that text. `Min` and
   `Max` skip NaN and are `+inf`/`-inf` over only NaN, as `fold(INFINITY, f64::min)` is. The
   multiset orders by the delta's total order, with NaN last, so the skip is a step past one
   key. A group holding a NaN and a non-number is mixed, because NaN is not equal to itself in
   `CellValue`'s `==` and is a distinct key here.
5. **`Sum` and `Avg` stay with the store until step 6.** Their eager result depends on the
   order the cells are added in (insertion order in the store, not `CellKey` order, whatever
   clause 3 says), so a group cannot reproduce it without keeping that order. The backend routes
   a read whose measure aggregation is `Sum` or `Avg` to `Model::evaluate_covering` and
   `evaluate_spanning`, which is eager's own path. Step 6 replaces both sides with `ExactSum`.
   Because `Sum` is the default, the corpus reaches the groups only once a `SetMeasureAgg`
   edit has changed a measure; the differential tests apply those on purpose.
6. **Formulas stay with the model until step 5.** A key a formula owns is read through the model,
   and `apply` calls `Model::recompute_formulas`, as `Eager` does. Step 5 replaces the call.
7. **A fold is the union of its members' groups.** `fold.rs` is `Model::group_expansion` read off
   the public model: the cross product of the covered members of every group the key names and
   every covered item of every category in `over` that it omits. Under `OverHidden` the members
   are groups of one shape (the base's categories plus the spans'). Under `Exact` the cells
   admitted are exactly the member keys, so the read is a lookup per member and a throwaway
   `Group`. A total therefore reads one group per covered row, not one per stored cell, but still
   one per row: clause 7's maintained totals with a subtracted hidden overlay are not built (see
   "Not built").
8. **Occupancy counts by inclusion and exclusion.** `occupancy(partial)` is the cells under
   `partial`, where a coordinate naming a group matches each of its members' items, with no
   hidden coordinate. For each way of choosing a member per group coordinate the count is the
   group's cell count, less the cells holding a hidden item of a category the key leaves free,
   by inclusion and exclusion over those categories: `N(P) - sum N(P + h) + ...`. The cost is
   the product of the hidden items per free category, a group read each. A key naming a hidden
   item itself is zero.
9. **The meter counts operations.** `Meter` is `updates` (group updates a delta caused), `reads`
   (groups a read looked at), `builds` and `built_cells`. `tests/measure.rs` fixes one table at
   two sizes and asserts the counts: an overwrite costs two updates per shape whatever the table
   holds, and a read of a group of 36 or 72 cells costs one group. Eager's cost for the same read
   is `matching_values().len()`, which the test prints beside it. This is the local fixture the
   brief asked for; ADR 009 step 4 says "measured at ADR 008's fixture", which needs ADR 008
   (unapproved) and is deferred.

10. **`Min` and `Max` keep the sign of a zero.** The multiset calls `-0.0` and `+0.0` one
    value (clause 3), so a group also counts its negative zeros from the raw change log, as step 6's
    sums are fed. Eager's `f64::min` and `f64::max` leave the sign of a tie between the two zeros to
    the platform and the order (`fmin` on ARM returns `-0.0`; x86 may not). The backend reproduces the
    part that does not depend on either: all zeros negative gives `-0.0`, all positive gives `+0.0`.
    With both, `Min` is `-0.0` and `Max` is `+0.0`; eager now returns the same (see "Eager's math,
    fixed").

### Not built in step 4

- Maintained totals (clause 7): a total reads one group per covered row.
- Eviction of shapes, and the build as a sliced job.
- `Sum`, `Avg` (step 6) and formulas (step 5) are eager's, behind the same trait.
- The ADR 008 fixture measurement.

## Step 5: formulas (improvise-shbc)

`Incremental` calls `recompute_formulas` only for the documents item 2 calls wide. Otherwise it keeps
the formula cache itself (`Model::formula_cell`, `set_formula_cell`, `clear_formula_cells` and the
now-public `evaluate_formula_cell`, the small additions to `improvise-core`) and decides which cells of
it to evaluate again; the evaluator that computes each value is core's own. The ADR (clauses 5 and 6)
is followed in outline, and the places it is not are the reason for this section.

1. **A stem is the unit, because eager's cache is per stem.** `Stems` (`formulas.rs`) holds, per
   target category, how many stored cells give each stem (a cell minus that category and the
   None categories, as `recompute_formulas` derives them), and which stems at least one category
   gives (`live`). Counts come from the raw store changes, one net count per stem per category per
   batch, so an overwrite never makes a stem vanish and reappear. A stem that appears is
   evaluated; one that goes has its cells removed.
2. **A stem's cells are evaluated from nothing.** `recompute_formulas` clears the cache and runs
   fixed-point passes over every stem together. When no formula reads another stem's cache the stems
   are independent, so running the same passes on one stem from an empty cache gives exactly what
   the whole run gives for it, including `circular` for a cell still moving after sixteen
   passes. That is why a dirty stem is cleared first (`passes-start-warm` shows what a warm start
   changes). Where they are not independent (`Stems::is_wide`: two target categories, or a name in
   another category that is not None) the backend falls back to `recompute_formulas` for the whole
   cache, so those documents are exact and not incremental.
3. **Which stems a change reaches is a superset, read off the formulas.** For formula `f`,
   `Reads` is the set of names in its expression and in the formulas those names target, and the
   categories that puts in play (its target's, every name's, every `WHERE`'s and `IS`'s). A stored
   cell can change what `f` evaluates to at stem `s` only if it agrees with `s` everywhere outside
   those categories. `Readers` indexes each live stem by what is left of it outside them, per
   category set, so a changed cell finds its stems by looking up its own projection on each set:
   no scan of the stems. This is clause 5's input rule made coarser, once for every shape of
   formula: it re-evaluates a stem for a cell of an item the formula never names (a change to a
   `Note` cell evaluates the stems `Profit` has). It cannot miss one, which is what the aggregate
   over an expression needs, since the cells it reads are chosen at run time by the records.
4. **The aggregate-over-expression pipeline (clause 5, items 1 to 3) is not built.** A dirty stem
   evaluates its formulas whole, so `SUM(Revenue * Price)` is re-folded over its records when any
   cell under the stem changes, not adjusted for the one record. That needs the evaluator to
   accept a maintained aggregate in place of folding, which is a change to core's evaluator and
   to the order its records are visited in (insertion order, not `CellKey` order). It is a bead.
5. **Dependency order is an optimisation and is checked against the plain passes** (the NaN and zero differences below are gone: "Eager's math, fixed"). `Order` is the
   formulas' dependency graph by name. When it has no cycle and there are fewer formulas than
   passes, one evaluation per cell in dependency order reaches the fixed point eager's passes
   reach (a chain of fifteen links needs fifteen passes and a sixteenth to see no change). It is the same fixed point, because Eager's convergence test compares by bits ("Eager's math, fixed").
   `Evaluation::Plain` always
   runs the passes; `tests/ordering.rs` compares the two after every edit, zero signs included, and
   `tests/formulas.rs` compares both with eager.
6. **A formula edit rebuilds the stems.** Adding, removing or replacing a formula (the fingerprint
   of the formula list moves) rebuilds the stems from the store by one pass, clears the cache and
   evaluates every stem, because a formula has a cell at each. Clause 5 wants a formula delta;
   the index is not maintained across a formula edit. `Meter::rebuilds` counts it.
7. **A new aggregation dirties the stems it can reach.** `measure_agg` is not a cell, so no change
   reaches the readers. A fold under a None category takes its aggregation from the `_Measure`
   coordinate of the key, which for a formula targeting another category comes from the stem and
   from no name the formula reads, so every live stem carrying that measure is dirtied
   (`Stems::carrying`). Where a formula names the measure (it targets `_Measure`) `reads_name` dirties every stem.
8. **A write of the same bits changes nothing; a write of `-0.0` over `0.0` does.** The cell delta
   treats the two as one value (clause 3), but a formula may not (`Units ^ -1` is `inf` and
   `-inf`), so the formula side reads the raw change log, not the canonical delta.

### Not built in step 5

- The aggregate-over-expression pipeline and the per-record order key (item 4).
- Stems that survive a formula edit (item 6), and name-level selectivity within a stem (item 3).
- Incremental cache for documents with formulas in more than one target category, or a name in
  a non-None category other than the formula's own (item 2): they use the whole recompute.
- Strongly connected components as a maintained structure: `Order` is rebuilt with the stems, which
  is O(formulas) on a formula edit, and cycles are found by depth-first search, not Tarjan's.

## Step 6: Sum, Avg and totals through an exact sum (improvise-hrjz)

ADR 009 clause 8, in both backends. `Sum` and `Avg` stop being the one reading that went to the
store: a group now holds a `numtower::ExactSum` beside its counts and multiset, and `Reduce`
(was `OrderFree`) has all five functions. Step 4's delegation, and its sentence in section 5
of that step, are gone; formula-owned keys still go to the model, whose cache step 5 maintains.

1. **`ExactSum` already signs a zero total** (`numtower/src/sum.rs`, PR #348, written for step 8's
   last test): `-0.0` only if every finite addend is `-0.0`, `+0.0` for any other zero, an exact
   cancellation included. An earlier version of this step wrote that rule as a wrapper, `FloatSum`;
   it was dropped when `gh/main` brought the same rule into `ExactSum`, and the tests of the rule are
   that PR's `tests/zero_sign.rs`. One difference from the wrapper: an empty sum reads `+0.0`, where
   `Sum for f64` starts at `-0.0`. Core's `SUM` over no rows therefore changes from `-0.0` to `+0.0`
   (a formula `SUM` whose `WHERE` matches nothing); `a_formula_sum_over_nothing_is_positive_zero`, in core,
   pins it.
2. **Core sums through it.** `apply_agg` (`Sum`, `Avg`) and the formula-level `SUM` in `eval_agg` call
   `exact_sum`, so `Eager` is exact, and so is every reading of the model, with no flag: the user
   visible change clause 8 names (displayed sums change in their last bits) is this commit. `improvise-core`
   gains the `numtower` dependency; both of the new edges are in `Cargo.nix` and the harness lock.
3. **A group's sum is fed from the raw changes, not the cell delta.** The delta calls `-0.0` and
   `+0.0` one value (clause 3), so an overwrite of `0.0` by `-0.0` is no delta at all, yet it moves
   the sign of a zero sum. `Shape::apply` takes the delta for counts and the multiset and the change
   log for sums, skipping only a change that left the same bits. The ADR's two clauses 3 and 8 are
   consistent only because the sum reads the store's values and not the delta's. The cost is a second
   walk of the batch per shape.
4. **Totals and collapsed groups absorb.** A read of several groups (`total`, a collapsed group,
   a hidden member left out) adds their accumulators with `absorb` and reads once, so a total is the
   same bits whatever the grouping and whatever the order of the rows. The clause 7 hidden overlay
   (subtracting the hidden cells from a kept total) is still not built; a total is a union of member
   groups, not a kept total less an overlay.
5. **`Avg` is the exact total over the cell count, rounded once** (`ExactSum::mean`). The first
   version divided a rounded sum, which rounds twice and overflows with the sum: `Avg([MAX, MAX])`
   was `inf` and a correctly rounded mean differs from the twice-rounded one for about 2% of random
   multisets. Both backends now use `mean`, so this is a second user-visible numeric change
   beside the sums: a displayed average can differ in its last bit, and a mean whose sum would
   overflow is finite. `numtower/tests/mean.rs` checks it against exact rationals.
6. **What a group costs.** An `ExactSum` is 70 limbs of `i64` and a few counters, about 650 bytes
   (`size_of`), in every group of every shape, whether or not the measure is summed. Clause 8
   accepts 568 bytes "per summed group"; here the shape does not know which measure its groups
   serve, so a shape at cell granularity (a read of a full key) pays it for each cell. Sparing
   groups that are never summed, or holding the sum only above one cell, is the improvement; it
   is a bead.
7. **The drift test is 20,000 overwrites, not a million.** ADR 009 measured 1.7e-9 at 18,000 cells
   after a million cycles. `tests/exact.rs` runs 20,000 overwrites of a 1,000-cell group with
   values chosen so an `f64` sum drifts, and asserts the two backends equal each other and a sum
   built afresh to the bit. The count is what a test binary can afford; the property it pins is
   independent of it.

### Not built in step 6

- The hidden overlay and kept totals (clause 7).
- A group that does not pay for a sum it never reads (item 6).

## Eager's math, fixed (user ruling 2026-10-10)

"Don't reproduce math bugs you might find in the Eager mode." Every place the earlier steps matched
Eager's arithmetic "as eager does" was reviewed. The items below supersede the sentences in steps 4 and 5
that say otherwise (step 4 items 4 and 10, step 5 item 5). Each is a user-visible numeric change.

1. **Min and Max of both zeros** is `-0.0` and `+0.0`, whatever the order or the platform. Core's fold used
   `f64::min` and `f64::max`, whose tie between the zeros is left to the platform; it now orders by
   `total_cmp` over the non-NaN values. Incremental already returned this. (improvise-bw4p.20)
2. **Min and Max over only NaN** are NaN, where they were `+inf` and `-inf` (the seed of the old fold leaking
   out). NaN among numbers is still skipped.
3. **A NaN formula result is a value, not a cycle.** The fixed point compared cached cells with `!=`, so a
   cell that settled on NaN never settled and became `circular`, dragging the cells that read it. It now
   compares with `model::types::settled`: numbers by bits, every NaN one value. A cell that really oscillates
   is still `circular` after sixteen passes. `mark_nan_circular` is gone.
4. **A zero's sign is a change.** `settled` compares by bits, so `0.0` becoming `-0.0` between passes moves
   the cell, and eager's fixed point and dependency order's agree. Dependency order is the unique fixed point
   of an acyclic set under bit equality, up to NaN payload and sign (`settled` merges NaNs): each cell is a
   function of the final values it reads. So the
   `holds_a_zero` fallback is dropped and `Ordered` needs no extra precondition.
5. **Empty `SUM`** is `+0.0` (step 6), listed here for completeness.
6. **Cycles over zeros and NaN.** A cycle that only flips a zero's sign (`X = -X`, `X = X * -1`,
   `IF(X < 1, -X, X)`, `A = -B` with `B = A` over zeros) used to settle, because `-0.0 == 0.0`; it is now
   `circular`, as the same cycle over nonzero data always was. A cycle fed a NaN (`A = A + 1`, or `A = A`
   with `A` NaN) used to be `circular` and now settles on NaN.
7. **`Min` and `Max` skip NaN while `Sum` and `Avg` propagate it.** Kept: it is IEEE's `minimumNumber` and
   `maximumNumber` for the extremes and ordinary addition for the sums, and consistent with ADR 005.
   Whether a spreadsheet user expects one rule for both is a product question (bead text in the hand-back).

### Left alone, with the reasoning

- **`Count` of a group that holds text** returns the text (the unanimity branch of
  `aggregate_cell_values`), not the number of cells. That is probably not what a user wants, but it is a
  decision about what a `Count` measure means for non-numbers, not an arithmetic error, so it is filed
  rather than changed.
- **The division and equality epsilon** (`FLOAT_EQ_EPSILON`, 1e-10) is shared and deliberate (gotcha 17).
- **A group holding NaN beside text** is `mixed`: NaN is a number and text is not, so no unanimity exists.
- **`Avg` and `Sum`** are already exact and correctly rounded (step 6).
- **Overflow of the exact sum to infinity** follows `ExactSum::value` (round to nearest, so an overflowing
  total is infinite): correct IEEE behaviour.


## Step 7: live sources (improvise-rnak)

ADR 009 clause 2 names two kinds of live source: one that reports its changes, which feeds cell deltas
like `DataStore`, and one that answers aggregate queries but reports none, which implements the derived
value by pushdown. The core half of both is in `context/code/source.md` (`CellSource`, `Model::over`).
The brief ordered this half after the evaluator hook; the hook came first because a source that reports
changes still has its formulas evaluated over it. User ruling 2026-10-10: formulas are computed in RAM
from the source's folds, never pushed down; `Derived` stays in this crate.

### Change-reporting (`Incremental::over`)

1. **`ChangeSource` is `CellSource` plus `drain_changes(&self)`, and a source's cells are those as of the
   last drain.** A shape is built lazily, by a pass over the source, at its first read. If a source
   showed a write before reporting it, a shape built in between would hold the write and the next
   drain would add it again. So the contract is that nothing is visible until it is drained, which is
   what a database does inside a read transaction and what `DataStore` does already (its log is
   drained in the step that made the edit). `&self` because a live source is shared with the model that
   reads it and changes behind it by interior mutability of its own.
2. **`Incremental::over(model, feed, none_cats)`** takes a `SharedFeed`, the alias core exports (a generic
   `Arc<S>` could not take it: `S` is `Sized`). The model is put over the feed (`Model::over`), which
   drops the cells it came with, so none is left for `get_cell`, persistence or the harness to read. Its categories, formulas and aggregations are the definition; the
   source holds the data. Shapes and stems are built from the feed as it stands.
3. **`sync()` drains and maintains; `apply_changes(&[CellChange])` maintains changes the source already
   reflects**, for a source whose changes reach the backend by another route (a trigger table, a
   channel). `Maintained::apply` on a fed backend takes definition edits (a formula, an aggregation)
   and drains: a cell edit is the source's to make, and `apply` refuses it with an `assert!` in every
   build (a release build lost it silently when only `Model::set_cell`'s `debug_assert` stood in the way).
   **A feed has one drainer**: a drain is destructive, so two backends over one feed split its changes
   (`context/code/source.md`, `ChangeSource`).
4. **Freshness is the source's.** ADR 003 left "polled, triggered, or stale until refreshed" open: `sync`
   is the poll, and when it is called is the host's decision. Nothing here schedules it.
5. **What a change costs** is what it costs for the owned store: two group updates and two exact-sum
   updates per maintained shape, no pass over the source (`the_cost_of_a_reported_change_...` counts the
   rows the source serves for snapshots: zero after the build). Formulas are evaluated at the stems the
   change reaches, as in step 5.
6. **Three routes into the store were routed through the source**: `Shape::of` (the build) reads
   `cells(&[])`, `Stems::build` reads `keys(&[])`, and `Incremental::read` reads `value_at`. `Eager::occupancy`
   reads `keys(&[])` too, so an `Eager` over a source would answer it.

`tests/support/live.rs` holds `LiveTable`, the scripted source (an indexed store behind a lock, with
a pending list and a counter of snapshot rows) and `Fed`, an `Incremental` over one that a differential
can drive: a cell edit becomes a write to the table followed by `sync`.

### Query pushdown (`Pushdown`)

For a source that answers aggregate queries and reports nothing. `Pushdown::new(definition, source,
none_cats)` puts the model over the source (`Model::over`) and keeps nothing else: no shapes, no
change log, no stems. These are the readings taken.

1. **`AggregateQuery` is `CellSource`; there are two traits, not three.** The brief's `AggregateQuery`
   (`fold`, `count`) is the trait core already has: `summarize` is the fold, `count` the count. `Derived`
   stays here (user ruling) and stays a different thing: the values a view draws, which a backend
   builds from a source's aggregates and its own state. A source implements `CellSource` and a backend
   implements `Derived`.
2. **Folds are queries, formula cells are computed in RAM.** `value`, `raw_fold`, `covered` and `total` are
   the model's evaluator over `Model::source()`, so a fold is one `summarize` and the rest is arithmetic
   on the answers. The formula cache is the one thing `Pushdown` holds. That is the user's ruling
   (2026-10-10), and it makes the evaluator hook the only change to core's evaluation.
3. **Staleness is `refresh()`.** A stored cell or a fold is current at the moment of the read. A formula
   cell is the cache's value until `refresh` recomputes it from the source as it now stands, which
   costs one `distinct_without` per formula and the folds each formula reads. When to refresh is the
   host's (ADR 003's "polled, triggered, or explicitly stale"); nothing here schedules it. A
   delivery layer that wants notices from a pushdown-backed shape has no moved keys to name, so it
   marks them "correct" (ADR 009 clause 9), which is a bead (below).
4. **Occupancy is one `count`.** A group in the partial becomes a span over its own name and its
   members; the view's hidden pairs go as `excluding`. `Eager::occupancy` lists every key to say the
   same thing.
5. **`define(edit)` takes a formula or an aggregation edit and refreshes.** A cell edit is the source's:
   `define` refuses it with an `assert!` of its own in every build (`a_cell_edit_on_a_pushdown_is_refused`).
6. **What the differential proves, and what it does not.** `value`, `raw_fold`, `covered` and `total` are
   the same four functions for `Eager` and `Pushdown` (`reads.rs`; they were copies, and are shared now),
   so a Pushdown-against-Eager differential cannot see a mistake in them. `Pushdown::members` repeats
   `Eager::group_holds` in a different form (a span list against a predicate), and that repetition
   is compared. What the differential proves is the **source's** semantics: that `summarize`, `count`
   and `distinct_without` give, for every select the evaluator and the views make, the answers a
   `DataStore` gives. The evaluator over a source is proven equal to the evaluator over the owned
   store in `improvise-core` (`over_tests`). Nothing else is claimed.
7. **A refresh wants one snapshot.** `refresh` asks `distinct_without` and then folds, so a source that
   changes between the queries can serve them from different revisions. The passes heal what they
   can: a write between two folds is read again by the next pass, and the cache ends equal to the new
   state's values (`writes_between_two_queries_of_a_refresh_are_healed_by_the_fixed_point`). A stem
   that appears after the stem list was taken has no cell until the next refresh
   (`a_stem_that_appears_between_the_stem_list_and_the_folds_waits_for_the_next_refresh`). A real source
   should serve a refresh from one read transaction; nothing here can ask it to.
8. **Known evaluator defect: the result can depend on the order of the stems** (improvise-bw4p.30). The
   passes of the fixed point update the cache in place, visiting stems in the order `distinct_without`
   lists them, and stop at sixteen. A document whose stems read each other settles in one pass listed
   along its dependency chain and takes one pass per link listed against it, so an eighteen-link chain
   is `circular` the second way. That is the evaluator's fault, not an obligation on a source: a SQL
   source has no order to keep, and bw4p.30 is to make the fixed point independent of it. Until then
   the first-seen order (`DataStore`'s insertion order) is what the oracle uses, and
   `the_order_stems_are_listed_in_decides_a_result_today` pins today's behaviour: along the chain 18,
   sorted `circular`, and a source listing its stems sorted is a divergence. No fixture before it had a
   result that depended on the order. When bw4p.30 lands the test's sorted half must change to expect
   agreement, and this item goes.
9. **What is and is not proven.** The tests run against `Remote` (`tests/support/remote.rs`), a scanning
   in-memory table with counters, that shares no evaluator with `Eager` and answers queries over rows.
   Without a real SQL engine only the **contract** is proven: that a source answering these six
   queries as specified gives `Eager`'s answers, and what each read costs in queries. Nothing here
   shows that SQLite can answer `summarize` exactly (an exact sum is not what its `SUM` returns:
   `context/code/source.md`), or what a query costs. The first real source is improvise-rucf, still
   deferred.

### What step 7 did not predict

- **The hook came before the change feed**, not after (a fed backend's formulas are evaluated over the
  source; see `context/code/source.md`).
- **`TableSource` and `LiveTable` found nothing in `Incremental`**; the corpus and the random edits pass
  over a source on the first run. What the tests found was in the fixtures: a rival that read the owned
  store for the stored fallback of a filtered formula passed until a cell was stored where the `WHERE`
  fails, and a rival that forgot a group's own name as an item passed until a cell was stored under
  one.
- **The two-second limit decided the shape of the tests** more than the design did: the corpus
  differential over a scanning source is 2.5s untrimmed, so it follows `corpus_eager`'s trimming, and
  each random test is its own binary.

## Scheduling: sub-circuits on a worker pool (user ruling 2026-10-11)

Multi-threading here is **scheduling**. Each sub-circuit stays synchronous and single-threaded
(`zset.md`, "Threads"), the only thing that crosses threads is an edge (`zset.md`, "Edges"), and
a small executor decides which thread runs which sub-circuit next. This is a ruling recorded here,
not an ADR amendment. Native threads are assumed. `sched.rs` and `staged.rs` compile for wasm32
(a `Mutex` and a `Condvar`), but `improvise-command` depends on this crate, so the module is in
the browser bundle: `Pool`, the only thing that spawns a thread, and the blocking calls
(`claim_blocking`, `wait_idle`, which `Condvar::wait` would make panic there) are
`cfg(not(target_arch = "wasm32"))`. Nothing here runs on wasm.

1. **A unit is a sub-circuit with the edge ends around it** (`Unit`: `turn(budget)` and
   `neighbours()`). Placement is manual: which nodes sit in which unit is how the graph was built,
   and `staged::PLACEMENT` names it for the example. Two node-building functions (`aggregate_nodes`,
   `grid_nodes`) build the same nodes into one circuit (`single_circuit`, the reference) or into
   two.
2. **Runnable means queued.** `Executor::kick(id)` queues a unit once. A unit is kicked by the
   host (`Staged::submit`), and by a neighbour whose turn moved a frame (`Turn::progress`, which a
   unit derives from its edges' `traffic()`). A kick reaches both directions, because a request
   flows back along an edge. Progress is a count of frames, so it ends: two neighbours cannot kick
   each other for ever.
3. **The ownership token is the unit itself.** A claimed unit is taken out of its slot, so a second
   worker cannot reach it. A kick that arrives while it runs sets `again`, and the owner queues it
   when it hands the unit back (`finish`). No lock is held during a turn; one mutex guards the
   queue and the slots, and a turn takes microseconds beside it.
4. **Fairness is the budget and the back of the queue.** A turn handles at most `budget` frames
   (`EdgeSource::poll(max)`), then says `more`, and `finish` queues it behind the units already
   waiting. A full edge is **not** `more`: the sender would spin through the queue while its
   consumer is not running (`a_full_edge_does_not_make_its_sender_spin`). The consumer that frees
   room reports progress and kicks its producer back, so a backlogged sender runs when it can
   send. For the same reason a middle unit (the aggregate) needs no `more` at its budget: its
   consumer's progress kicks it. The tail (the projection) has no consumer to kick it back, so it
   says `more` when it read a full budget (`a_unit_whose_kicks_coalesced_still_drains_its_edge`,
   because kicks coalesce into one queue entry). Both clauses were first written untested; a
   review injected their removal and everything passed, which is how the first was found to be a
   spin and the second redundant. The resumable `step(deadline)` predicate of `Rebuild` is for a sliced snapshot load,
   and this example has none.
5. **The executor spawns nothing.** `claim` and `finish` are what a worker calls. `Pool` is N
   threads looping on them; the tests' scheduler calls them in an order a seed chooses, with up to N
   units held at once and the turn of a held unit already run, so a kick can land on a running
   unit. Both drive the same code.
6. **Results do not depend on N or the order.** The deltas sum, and every operator in the graph is
   a function of its input's integral. So any schedule settles where the single circuit does
   (`placed_circuits_equal_one_circuit_for_any_workers_and_order`, 1 to 4 workers, random
   commands, random order, commands arriving while it runs; and a real pool of 1 to 4 threads).
   Per-tick outputs (`delay`, `differentiate`) would differ with coalescing, and the example has
   none.
7. **What the example is.** `Staged`: the host's end of the first edge, an aggregate stage (sum of
   a cell's value per row and column, `aggregate`) and a grid projection (the cell each group draws,
   a total per row). The incremental backend (`Incremental`) keeps its groups in its own shapes
   and does not run on a `Circuit`, so the stage is the same computation built as zset nodes rather than a
   split of `Incremental` itself. Running `Incremental` on circuits is a later step.
8. **A panic in a turn kills that unit and nothing else.** A turn runs outside the lock, so
   nothing is poisoned and, in the first version, the pool waited for ever on a unit that never
   came back. Now the worker catches the unwind and calls `Executor::abandon`: ownership is
   released, the unit is dead (never run or kicked again), the panic is recorded
   (`Executor::panics`, `UnitPanic { unit, message }`), and neighbours go on. `wait_idle` and
   `Pool::finish` return `Err(UnitPanic)` for the first one once the rest is quiet. A unit that
   cannot name its neighbours is buried the same way. A kick of a unit that does not exist panics
   before it takes the lock (`no such unit`), so a bad index cannot poison the executor; the
   `lock()` message now names the only thing that can poison it, a panic in the executor itself.
9. **Workers are counted and a dropped `Pool` stops them.** `Executor::workers()` counts live
   worker threads, so a worker that leaves on a spurious wake is visible
   (`every_worker_stays_through_wakes_with_nothing_queued`); `Drop for Pool` shuts down and joins
   (`a_pool_that_is_dropped_waits_for_its_workers`), discarding what is queued. A dead unit is
   dropped inside `catch_unwind` (`bury`), because a drop that panics would otherwise kill the
   worker after the bookkeeping and hang or shrink the pool; `Pool::join` does not panic over a
   dead worker while the host is already unwinding. `claim_blocking`
   returns `None` as soon as `shutdown` is set. The real-thread tests run behind a watchdog
   (`tests/support/watchdog.rs`), so a lost `notify_all` fails by name and not by hanging.
10. **Not done.** A work-stealing or priority scheme (one FIFO queue); a unit with a `Rebuild`
    job sliced by the deadline predicate; a timeout that calls `connection_lost` on the edges (the
    edges here never lose a frame); restarting a dead unit.