docs(context): correct the Eager-math evidence, restore the product-targeted test, record the cycle changes (improvise-bw4p.20)

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

context/code/core.md

@@ -94,7 +94,8 @@ target category and every `none_cat` stripped), and iterates
 `stem × formula target` until nothing changes, bounded by `MAX_EVAL_DEPTH = 16`.
 Chained formulas (`Margin = Profit / Revenue` over `Profit = Revenue - Cost`)
 converge naturally; circular references converge to `CellValue::Error("circular")`
-rather than overflowing the stack.
+rather than overflowing the stack. "Nothing changed" is `model::types::settled`: numbers by bits (a
+zero that changes sign is a change) with every NaN one value, so a NaN can settle.
 
 **A cell still moving when the bound runs out has not converged, and the cached
 path had to be told so** (improvise-7iww). The direct evaluator gets this free:

context/code/improvise-incremental.md

@@ -218,8 +218,8 @@ taken where clause 4 and clause 7 leave a choice; evidence is in
     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`, which is what ARM's `fmin`/`fmax` return; on other
-    platforms eager may differ there, and `tests/random.rs` keeps `+0.0` out of its pool for that reason.
+    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
 
@@ -268,14 +268,8 @@ is followed in outline, and the places it is not are the reason for this section
 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
-   differs from the passes in two places. A cell holding NaN is never equal to itself, so eager's
-   passes never see it settle and call it `circular`, and the cells that read it keep what they
-   computed from the NaN; `mark_nan_circular` does the same afterwards. And eager stops on `==`,
-   which calls `-0.0` equal to the `0.0` an early pass read from a stored cell, so a stem with a
-   zero cell can settle on a sign dependency order never sees (a stored `0.0` at `F1`, `F3 = F1`,
-   `F4 = F3 ^ -1`, then `F1 = -0`: eager's `F4` is `inf`). A stem whose ordered evaluation holds any
-   zero is therefore evaluated again by the passes (`holds_a_zero`). `Evaluation::Plain` always
+   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
@@ -370,9 +364,17 @@ that say otherwise (step 4 items 4 and 10, step 5 item 5). Each is a user-visibl
    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 (each cell is a function of the final values it reads), so the
+   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
 

context/test-evidence/improvise-incremental.md

@@ -439,7 +439,8 @@ After the last retraction the group reads as absent and its map holds no zero-we
 
 ### group::tests::min_and_max_skip_nan_and_are_nan_over_nothing_else
 
-NaN is skipped by `Min` and `Max`, a group of only NaN gives `+inf` and `-inf` and still counts.
+NaN is skipped by `Min` and `Max`; a group of only NaN gives NaN (it gave `+inf` and `-inf` before the
+Eager-math follow-up) and still counts.
 
 ### group::tests::a_fold_over_several_groups_is_the_fold_of_their_union
 
@@ -472,7 +473,6 @@ What each fault was and the test that names it:
   `a_formula_that_keeps_moving_for_sixteen_passes_is_circular`,
   `dependency_order_and_the_plain_passes_leave_the_same_cache`;
 - dependencies after dependents: `dependency_order_and_the_plain_passes_leave_the_same_cache` and five more;
-- NaN is not marked circular: `a_formula_cell_holding_nan_is_nan_and_not_circular`;
 - fifteen passes / seventeen passes: `a_chain_added_last_link_first_is_circular_exactly_where_eager_says`;
 - the passes end without marking the cells still moving, or begin from the old cache:
   `a_chain_added_last_link_first_is_circular_exactly_where_eager_says`,
@@ -559,7 +559,10 @@ which is evaluated after it. Fails when such a formula set is not wide.
 
 ### a_formula_cell_holding_nan_is_nan_and_not_circular
 
-NaN is not equal to itself, so eager's passes never see it settle. Fails when the ordered path leaves it.
+A NaN formula result is a value: `Profit` and `Margin` over a NaN cell read NaN under both evaluations and
+eager. It used to be `circular` in eager, because NaN is not equal to itself and never settled; the
+fixed point now compares with `settled` (follow-up, "Eager's math, fixed"). Fails when NaN is
+marked `circular`.
 
 ### a_new_aggregation_for_the_measure_a_filtered_formula_falls_back_to_changes_it
 
@@ -643,16 +646,23 @@ runs because its two heaviest tests shared it. The tests are unchanged.
 East plus the maximum of West), the first version kept 14. Fails when a new aggregation dirties only
 the stems of formulas that name the measure, and when `Stems::carrying` ignores the measure.
 
+### a_new_aggregation_reaches_a_product_targeted_filtered_sum
+
+A Product-targeted `SUM(F0 WHERE Region = East)` with no None category, and `SetMeasureAgg Cost Min`.
+It agreed with eager before the fix too, so it pins the shape and not the fault.
+
 ### a_new_aggregation_reaches_a_filtered_sum_on_the_fallback_path
 
-The reviewer's second repro, a Product-targeted `SUM(F0 WHERE Region = East)`. It already agreed on this
-fixture and stays as the second shape of the same hazard.
+The reviewer's shape: `P0 = SUM(Revenue) WHERE Region = East` on `_Measure` with Time as the None
+category, then `SetMeasureAgg Revenue Max`, so the fallback to the raw group at the formula's own target
+reads the new aggregation. Fails when a new aggregation does not reach the stems carrying the measure.
 
 ### ordered_evaluation_keeps_the_zero_eager_settles_on
 
-A stored `0.0` at `F1`, then `F3 = F1`, `F4 = F3 ^ -1`, then `F1 = -0`: eager settles on `F3 = 0.0` and `F4 = inf`
-because it calls `-0.0` equal to the `0.0` it first read; the first ordered evaluation gave `-inf`. Fails
-(only `Ordered`) when a stem with a zero is not re-evaluated by the passes. The ordering property's pool
+A stored `0.0` at `F1`, then `F3 = F1`, `F4 = F3 ^ -1`, then `F1 = -0`. Eager used to settle on `F4 = inf`
+because it called `-0.0` equal to the `0.0` it first read, while the ordered evaluation gave `-inf`; with
+zero signs settled by bits both give `F3 = -0.0` and `F4 = -inf`. Fails (only `Ordered`) when a stem
+with a zero is not re-evaluated by the passes, and in core when zeros settle equal. The ordering property's pool
 now holds `-0`, `Units * -1` and `-Cost`, and compares after every edit, but did not find this fault
 alone in 1,500 cases: this test is the pin.
 
@@ -768,8 +778,9 @@ Infinities and NaN read as `ExactSum::value` does, and a zero keeps its sign.
 
 ## Eager's math, fixed (follow-up to steps 4 to 6)
 
-Ruling (user, 2026-10-10): do not reproduce math bugs found in Eager; fix Eager. Eight faults were
-injected (six in the table below, two more in the groups' NaN handling); `nan-never-settles` survived the
+Ruling (user, 2026-10-10): do not reproduce math bugs found in Eager; fix Eager. Six faults were
+injected into core and the groups (mixed zeros, Min over NaN, NaN never settling, zeros settling equal, and
+the groups' Min and Max over NaN); `nan-never-settles` survived the
 first pass because NaN produced by one evaluation always has the same bits, and is closed by a unit test of
 `settled`. Each fix has a regression test named after the bug:
 - `model::types::eager_math_tests::min_and_max_of_both_zeros_do_not_depend_on_their_order` and
@@ -785,3 +796,8 @@ first pass because NaN produced by one evaluation always has the same bits, and
   oscillation is still `circular`.
 The random and differential suites compare numbers by bits and their pools hold both zeros again.
 
+User-visible changes this evidence also covers: 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) was `-0` and is now `circular`, as the
+same cycle over nonzero data always was; a cycle fed a NaN (`A = A + 1`, `A = A` with `A` NaN) settles on
+NaN instead of `circular`.
+

crates/improvise-incremental/tests/formulas.rs

@@ -379,3 +379,31 @@ fn ordered_evaluation_keeps_the_zero_eager_settles_on() {
         same_model(&model, &[], &edits, by).unwrap_or_else(|e| panic!("{by:?}: {e}"));
     }
 }
+#[test]
+fn a_new_aggregation_reaches_a_product_targeted_filtered_sum() {
+    let mut model = Model::new("products");
+    for (cat, items) in [("Region", vec!["East", "West"]), ("Product", vec!["F0"])] {
+        model.add_category(cat).unwrap();
+        for item in items {
+            model.category_mut(cat).unwrap().add_item(item);
+        }
+    }
+    model.category_mut("_Measure").unwrap().add_item("Cost");
+    for (region, v) in [("East", 4.0), ("West", 9.0)] {
+        let key = CellKey::new(vec![
+            ("Region".into(), region.into()),
+            ("Product".into(), "F0".into()),
+            ("_Measure".into(), "Cost".into()),
+        ]);
+        model.set_cell(key, CellValue::Number(v));
+    }
+    model.add_formula(parse_formula("P0 = SUM(F0 WHERE Region = East)", "Product").unwrap());
+    let none = vec![];
+    let edits = [Edit::SetMeasureAgg {
+        measure: "Cost".into(),
+        func: improvise_core::formula::ast::AggFunc::Min,
+    }];
+    for by in [Evaluation::Ordered, Evaluation::Plain] {
+        same_model(&model, &none, &edits, by).unwrap();
+    }
+}