fix(incremental): Avg rounds the exact mean once, core pins exact sums, Meter counts sum updates; notes and evidence (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

@@ -312,7 +312,9 @@ of that step, are gone; formula-owned keys still go to the model, whose cache st
    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`.
+   `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`
@@ -328,8 +330,12 @@ of that step, are gone; formula-owned keys still go to the model, whose cache st
    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.
+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

context/test-evidence/improvise-incremental.md

@@ -665,12 +665,12 @@ alone in 1,500 cases: this test is the pin.
 difference between them can show it) and is closed by a test that reads the formula sum itself. Each
 fault and the tests that name it:
 - eager's `Sum` adds in order: `sums_are_exact_whatever_the_order_the_cells_were_added_in`,
-  `a_million_overwrites_in_a_thousand_cell_group_do_not_drift`;
-- eager's `Avg` adds in order: `an_average_is_the_exact_sum_over_the_count`;
+  `twenty_thousand_overwrites_in_a_thousand_cell_group_do_not_drift`;
+- eager's `Avg` adds in order: `an_average_is_the_exact_total_over_the_count_rounded_once`;
 - the formula-level `SUM` adds in order: `a_formula_sum_over_an_expression_is_exact_in_both_backends`;
 - a read of several groups keeps only the first group's sum: nine differentials, among them
   `incremental_matches_eager_on_a_collapsed_group_with_a_hidden_member_under_every_aggregation`;
-- `Avg` divides by the number of groups: `an_average_is_the_exact_sum_over_the_count` and seven more;
+- `Avg` divides by the number of groups: `an_average_is_the_exact_total_over_the_count_rounded_once` and seven more;
 - sums never move after the build: thirteen tests, the first
   `a_sum_read_after_a_write_comes_from_the_delta_and_equals_a_fresh_sum`;
 - a retraction adds: eleven tests, among them `overwriting_zero_with_negative_zero_moves_the_sign_of_a_sum`;
@@ -685,9 +685,6 @@ fault and the tests that name it:
 Both backends must give the bits of 1.0 for each. Fails on eager adding in order, which is the
 discrepancy clause 8 exists for: the test failed on the pre-change code with 0.
 
-### an_average_is_the_exact_sum_over_the_count
-
-Five values whose sum `f64` addition misses; both backends give the exact sum rounded once, then divided.
 
 ### a_zero_total_has_the_sign_ieee_gives_the_same_addends
 
@@ -698,7 +695,7 @@ Five values whose sum `f64` addition misses; both backends give the exact sum ro
 Two cells of `0.0` overwritten by `-0.0`, then one overwritten back. The cell delta calls the two zeros
 equal, so the move comes only from the raw change log. Fails on a sum fed from the delta.
 
-### a_million_overwrites_in_a_thousand_cell_group_do_not_drift
+### twenty_thousand_overwrites_in_a_thousand_cell_group_do_not_drift
 
 20,000 overwrites of a 1,000-cell group, with values that make an `f64` sum drift; the maintained
 sum equals eager and a sum built afresh, bit for bit. The count is not a million (the ADR's
@@ -712,3 +709,60 @@ measurement) because a test binary cannot afford it; the property does not depen
 ### a_sum_read_after_a_write_comes_from_the_delta_and_equals_a_fresh_sum
 
 After a write, a `Sum` read builds nothing and equals the same read of a backend built afresh.
+
+### Review of PR #353: averages, core's own tests, the meter (improvise-hrjz)
+
+Ten faults (`improvise-core` and `improvise-incremental` run together): eager's `Sum` and `Avg` and the
+formula `SUM` adding in order, an average that divides a rounded sum, a formula `SUM` over nothing
+that is `-0.0`, the group's average dividing a rounded sum, a total that keeps one group's sum,
+sums not metered, a new cell's sum lost, sums never moving. Each was watched failing; the tests are named below.
+`same_value` compares numbers by bits since step 4, so the random suites see the sign of a zero in `Sum`
+and `Avg` too.
+
+The drift test was renamed `twenty_thousand_overwrites_in_a_thousand_cell_group_do_not_drift`: its old
+name claimed fifty times what it runs.
+
+### an_average_is_the_exact_total_over_the_count_rounded_once
+
+Five values whose sum `f64` addition misses; both backends equal `ExactSum::mean`, which `numtower/tests/mean.rs`
+checks against exact rationals. Fails on an average that divides a rounded sum.
+
+### an_average_does_not_overflow_with_its_sum_in_either_backend
+
+`Avg([MAX, MAX])` is `MAX`. Fails on a rounded sum divided.
+
+### model::types::exact_sum_tests::a_sum_does_not_depend_on_the_order_of_its_addends
+
+Core's own `apply_agg`: the three-addend sum is 1 in every order. Fails on eager adding in order, which the
+tests in `improvise-incremental` had been the only ones to see.
+
+### model::types::exact_sum_tests::an_average_rounds_the_exact_mean_once_and_does_not_overflow
+
+`Avg([MAX, MAX])` is `MAX` and `Avg([0.1, 0.2, 0.3])` is the exact mean. Fails on a twice-rounded average.
+
+### model::types::exact_sum_tests::a_formula_sum_is_exact_whatever_the_order_of_the_records
+
+`SUM(Revenue * 1)` over `[1e16, 1, -1e16]` in two orders is 1. Fails on the formula-level `SUM` adding in order.
+
+### model::types::exact_sum_tests::a_formula_sum_over_nothing_is_positive_zero
+
+`SUM(Revenue WHERE Region = Nowhere)` is `+0.0`; it was `-0.0` while it summed with `Sum for f64`. Fails
+on the old behaviour.
+
+### model::types::exact_sum_tests::a_stored_group_sums_exactly_and_averages_once
+
+A measure aggregated by `Sum` over `[1e16, 1, -1e16]` is 1, and by `Avg` is the exact third.
+
+### the_mean_is_the_nearest_f64_to_the_exact_total_over_the_count
+
+Up to eight finite addends, the mean against exact rationals (`numtower/tests/mean.rs`). Fails on an
+average of a rounded sum.
+
+### a_mean_whose_sum_would_overflow_is_still_finite
+
+`[MAX, MAX]` has the mean `MAX`.
+
+### non_finite_sums_have_non_finite_means_and_zero_keeps_its_sign
+
+Infinities and NaN read as `ExactSum::value` does, and a zero keeps its sign.
+

crates/improvise-incremental/src/shapes.rs

@@ -70,9 +70,8 @@ fn same_bits(change: &CellChange) -> bool {
 }
 
 impl Shape {
-    /// The canonical delta moves counts and multisets; the raw changes move sums and the sign of
-    /// a zero, which tell the two zeros apart. Returns the group updates the delta caused
-    /// and the sum updates the changes caused.
+    /// The delta moves counts and multisets; the raw changes move sums and the sign of a zero.
+    /// Returns the group updates and the sum updates.
     fn apply(&mut self, cats: &[String], delta: &CellDelta, changes: &[CellChange]) -> (u64, u64) {
         let (mut updates, mut sums) = (0, 0);
         let mut touched = Vec::new();

crates/improvise-incremental/tests/exact.rs

@@ -33,12 +33,6 @@ fn model_of(values: &[f64], func: AggFunc) -> Model {
     model
 }
 
-fn exact(values: &[f64]) -> f64 {
-    let mut sum = ExactSum::new();
-    values.iter().for_each(|v| sum.add(*v, 1));
-    sum.value()
-}
-
 /// Both backends' sum of `values` under `func`, as bits.
 fn both(values: &[f64], func: AggFunc) -> (Option<u64>, Option<u64>) {
     let model = model_of(values, func);

crates/numtower/src/sum.rs

@@ -155,9 +155,8 @@ impl ExactSum {
         }
     }
 
-    /// The exact sum divided by `count`, rounded once: a mean that neither overflows with the
-    /// sum nor rounds twice. Non-finite sums and the sign of a zero read as `value` does.
-    /// Panics on a zero `count`.
+    /// The exact sum over `count`, rounded once, so the mean neither overflows nor rounds twice.
+    /// Non-finite sums and a zero's sign read as `value` does. Panics on a zero `count`.
     pub fn mean(&self, count: u64) -> f64 {
         assert!(count > 0, "the mean of nothing");
         match (self.nan != 0, self.pos_inf != 0, self.neg_inf != 0) {

crates/zset/tests/circuit.proptest-regressions

@@ -1,7 +0,0 @@
-# Seeds for failure cases proptest has generated in the past. It is
-# automatically read and these particular cases re-run before any
-# novel cases are generated.
-#
-# It is recommended to check this file in to source control so that
-# everyone who runs the test benefits from these saved cases.
-cc da6d39e3f2d54dc796842f642b0fc17d09a1491a9937c3d3f95d453d2d9487ed # shrinks to prior = [(3, -1)], snapshot = [(3, 2), (5, -2), (0, 1), (1, 1)], chunk = 0, budget = 1

crates/zset/tests/rebuild.proptest-regressions

@@ -1,7 +0,0 @@
-# Seeds for failure cases proptest has generated in the past. It is
-# automatically read and these particular cases re-run before any
-# novel cases are generated.
-#
-# It is recommended to check this file in to source control so that
-# everyone who runs the test benefits from these saved cases.
-cc b276367684808122e5f3fedb8e87a6ab970895f3efce9e6b98a40ade2cdb7227 # shrinks to prior = ZSet { weights: {} }, snap = ZSet { weights: {0: -1, 1: -1} }, post = ZSet { weights: {} }, chunk = 0, budget = 1