test(incremental): exact sums in both backends, evidence and the step 6 reasoning (improvise-hrjz)

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze

context/code/improvise-incremental.md

@@ -280,3 +280,51 @@ which cells of it to evaluate again; the evaluator that computes each value is c
   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::FloatSum` 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. **`FloatSum` is `ExactSum` and the sign of a zero** (`numtower/src/sum.rs`). `ExactSum` is the
+   fixed-point accumulator the ADR measured, and adding `-0.0` to it adds nothing, so it cannot
+   say whether a zero total is `+0.0` or `-0.0`. `FloatSum` counts the addends and the `-0.0`
+   among them: a zero total is `-0.0` only if every addend is, which is what adding the same values
+   in `f64` gives, and an exact cancellation is `+0.0`. An empty sum is `-0.0`, as `Sum for f64` is,
+   because `SUM` over no rows reads that way today. Clause 8 says the sign rule "lives in
+   numtower"; this is where.
+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 sum over the cell count.** Both backends round once in the sum and once in
+   the division.
+6. **What a group costs.** A `FloatSum` 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).