[frankmcsherry]

Three explain soundness fixes, found by the differential testing (findings 5 and 6, plus one found while sweeping for them). With them, the explain oracle passes with the negation and non-monotone skips removed. Each commit has a regression test in tests/explain.rs that fails without it. +93/−25, all in explain/ and its tests.

1. Demand is a set (e6b9824).

• The bug: demand reaching a collection along two paths was summed. With negative counts on one path, the two cancelled and the explanation came out empty. The minimal case is a negated collection joined with its own swap.
• Why it's more than negation: negative counts occur inside every loop too, because each round's records hold that round's changes.
• The fix: a collection maps data to diffs, and an explanation names the data whose diffs must be accurate, so demand's counts mean nothing and must never cancel. Demand, and every table demand is looked up in (reference run, restricted run, sources), is now read as a set, through Sb::presence, renamed from distinct_full.
• Test: negated_fanout_explanations_sufficient.

2. A min demands the inputs at or below its demanded value (50fafd8).

• The bug: a min's keyed lookup kept only the inputs whose value equals the demanded value. When the restricted run raised a key's minimum (the inputs achieving the lower value left out), demand asked for the inputs achieving the wrong, raised value, and never the reference's lower ones. The minimal case is label propagation, then a count per label.
• The fix: narrowing keeps the inputs at or below the demanded value. That covers both ways the restricted run can be wrong: a raised minimum takes in the reference's lower achieving inputs, and a lowered one takes in the inputs that lowered it. It's a single predicate.
• Test: min_then_count_explanations_sufficient, plus the updated value-contract unit test.

3. The restricted run reads demanded rows whole (5179498).

• The bug: the restricted run's inputs, and each demand set's closure, matched demanded rows to source rows by key alone. Demanding one row brought in every source row at that key, at inflated counts.
• The fix: they now match whole rows (Sb::restrict).
• Test: restricted_rows_keep_their_counts.

Validation

• Sweep: with the DDIR: a differential-testing sweep over random lambda programs #980 harness copied in locally, keeping only the timed and quadratic skips, 15,000 seeds with 0 failures. The earlier failing cases 3003503, 3004641, 3004659, 3005430 and 9006406 all pass.
• Checks: the release explain suite with ignored tests (29/29), workspace tests, doc tests, clippy, the LDBC smoke and SNB suite at 1 and 4 workers plus maintained mode.

Cost: release explain suite, instructions retired: 423.1G on master-next, 567.4G here (+34%). This was accepted for correctness.

Follow-up once #980 lands: remove the harness's shape skip for these findings, so case.explainable = !g.timed && !exploded;, and update the Case::explainable doc.

🤖 Generated with Claude Code

https://claude.ai/code/session_019XsakwFGwtESwZ1gSYwG4o