Streamline the proxy reduce tactic

[frankmcsherry]

The proxy reduce tactic re-derived each key's working state from scratch: every presented record was cloned into an EditList, exploded into a per-edit history, and re-sorted — per key, per window; pending times lived in BTreeMap<u64, Vec<T>>s rebuilt per retire; and each key slot carried ~19 heap vectors. This PR reworks the tactic to work directly from the presented windows, with each piece of state pooled at its natural lifetime.

• Windows are worked in place. After next_window the harness owns the presentation: per key bracket it lifts the history and output times by the seed meet and re-sorts the bracket to (time, id) order, with suffix meets in shared columns (prepare). The lift is preserved exactly — losing it turns linear sweeps quadratic; see the comment at the call site. EditList/ValueHistory leave the proxy path entirely, and a key slot shrinks to the six vectors that are genuinely wave-persistent (accumulations, reached, synth, produced). The backend's requirements are unchanged; ReduceWindow now documents that presented records belong to the harness afterward.
• Pending flattens. The tactic's cross-retire state becomes two sorted (key, time) columns: the due/carried split is one scan, changed a dedup of the due keys, due lookup a single ascending cursor per retire, and the next pending set accumulates flat with one sort at retire end. The three BTreeMaps are gone.
• One witness set. Novel times enter reached as they step in, so absorb tests and close joins against the single novel set of formal/Differential/RoundCoverage.lean's round_coverage, rather than a split across reached and the novel buffer.
• Scratch pools across retires. All retire-scoped working state moves into a Scratch held by the tactic, cleared at its boundary (retire/window/wave/tick) rather than reallocated — profiling showed per-retire setup was ~30% of the tactic's cost on iterative workloads, whose retires are many and small. Naming the backend's diff types re-parameterizes the tactic over (B1, B2, Bk); every construction site is ProxyReduceTactic::new(backend) with inference, so no caller changes.
• ProxyReduceBackend::emit now documents the guarantee its calls already carried — per tile, disjoint ascending key ranges, each consolidated — which licenses backends to build output incrementally instead of staging rows.
• The vestigial history.rs folds into join.rs, and the bench's propagate round count becomes env-configurable (PROP_ROUNDS), which profiling wanted.

Measured on tests/int_proxy_bench (defaults): churn 21.7 → 19.8ms/round (0.47x cursor-same), multimoment 16.2 → 14.6ms (0.90x — the proxy tactic now beats the cursor tactic on identical storage), propagate 2.53 → 2.37ms (1.04x). A scale sweep to the GB range (4M-key churn, 1M-key multimoment, 1M-key string-valued wide) shows the ratios and per-key costs stable across two orders of magnitude, and — measured with interleaved fresh-process repeats — memory parity with the cursor tactic (churn 4M: 3756 vs 3703MB peak RSS).

🤖 Generated with Claude Code