docs(adr): ADR 009 states correction as the Z-set difference target minus held (improvise-felo.4)

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

context/adr/009-incremental-evaluation.md

@@ -227,13 +227,21 @@ an **edge adapter**. So every edge has the same semantics:
   treats the hop as dropped. The downstream side then asks for a correction from its
   last stamp.
 
-- **Correction is an engine operation.** The engine offers, per shape key, a
-  **correction** computed from a client's last stamp. Where the shared log still covers
-  that stamp, it is the net delta since then. Otherwise it is a replacing delta: the
-  current state for the client's window, with whatever the client held retracted. A
-  full refetch is the case with an empty basis. A correction is idempotent, resumable
-  by stamp, and written in the same lossless delta form as a notice, so a client, a
-  gateway or a worker applies it with the same code.
+- **Correction is Z-set arithmetic.** A correction is `target − held`, where `target`
+  is the current state for the client's window and `held` is what the client holds.
+  Applying it with ordinary Z-set addition gives `held + (target − held) = target`, so
+  the group structure of `ZSet` provides it, with no separate machinery. The client
+  sends its last stamp:
+  - where the shared log covers that stamp, the host sends the sum of the logged deltas
+    since then;
+  - otherwise the host sends `target`, and the client, which knows `held`, applies
+    `target − held`;
+  - a full refetch is `target − ∅`.
+
+  A correction is labelled with the publication range it covers, so it is applied only
+  at the stamp it starts from, which makes it idempotent and resumable. It uses the same
+  lossless delta form as a notice, so a client, a gateway or a worker applies it with the
+  same code.
 
 Aggregation stays on the model side (ADR 008), so the operators that aggregate run on
 the model side, which may itself span a hop. Which other edges cross a wire is a
@@ -348,8 +356,9 @@ Step 8's required tests:
 - `[AddItem, SetCell]` publishes one notice, and no client asks for a correction;
 - a dropped notice is detected;
 - a reconnect after a host restart asks for a correction;
-- a corrected state equals the state of a client that was never stale (a property
-  test over random edit sequences and losses);
+- a corrected state equals the target, `held + (target − held) = target`, and
+  correcting a state that is already correct is the zero Z-set (property tests over
+  random edit sequences and losses);
 - a refused frame consumes no publication number;
 - a dropped hop triggers a correction.