From 7619f04280b1412c76f4619b221e860e96e64e79 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 13 Oct 2026 12:54:23 +0000 Subject: [PATCH] D-CMR plan: Experiment A's i32 arm is a counterexample, not today's fold Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013z2e1YXkm6o6HNrDn5BPWA --- .claude/plans/d-cmr-concept-chain-normalization-v1.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/.claude/plans/d-cmr-concept-chain-normalization-v1.md b/.claude/plans/d-cmr-concept-chain-normalization-v1.md index 7668eb0f3..e70798866 100644 --- a/.claude/plans/d-cmr-concept-chain-normalization-v1.md +++ b/.claude/plans/d-cmr-concept-chain-normalization-v1.md @@ -229,8 +229,10 @@ update and maintenance laws), never a precondition for `SUM`. ## 7. Experiments, each with an independent oracle and a negative control - **A. Cancellation.** At the aggregate level: `Sum(A) − Sum(A∧B)` against - `Sum(A∧¬B)` and an exact `i128` oracle; an eager variant accumulating into - `i32` shows the loss. Under checked arithmetic the rewrite must refuse. + `Sum(A∧¬B)` and an exact `i128` oracle. An eager variant that deliberately + accumulates into `i32` is the counterexample that shows the loss; it is not + a model of today's fold, which accumulates exactly into `i64` within the row + bound. Under checked arithmetic the rewrite must refuse. - **B. Range intersection.** k compatible ranges intersect before any row is read. Baseline: `fold_ranges` and `Lowering::Range` (tests at quack `lib.rs:5204–5248`).