docs(adr): ADR 009 answers stale state with an engine correction operation (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

@@ -220,17 +220,26 @@ an **edge adapter**. So every edge has the same semantics:
   Every request can be retried, and a resync from a publication stamp is idempotent. A
   client asks for "notices since n", and the host answers from **one shared, bounded log
   of published notices**: a single log, not one per edge or client. A request older than
-  the log's start is answered "refetch".
+  the log's start is answered with a correction (below).
 - **Failure is local to a hop.** A hop may be a socket or a series of requests, and it is
   alive while its next message or request succeeds. Each hop keeps alive in both
   directions. A side that hears nothing within the timeout, or whose request fails,
-  treats the hop as dropped. The downstream side then resyncs: it refetches through the
-  path, and the host answers from current state.
+  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.
 
 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 deployment choice. The engine's
-invalidation signal, which ADR 006's replay trigger relies on, is the change notice and
-the refetch rule below, followed from a displayed cell's key back to the model.
+the model side, which may itself span a hop. Which other edges cross a wire is a
+deployment choice. The engine's invalidation signal, which ADR 006's replay trigger
+relies on, is a correction trigger below, followed from a displayed cell's key back to
+the model.
 
 **A request** is a shape key plus a window, given as an absolute cross-product top-left
 and dimensions. The window is never state, and a request costs O(visible).
@@ -261,13 +270,13 @@ client, addressed to none. It carries:
   the circuit computes them. Moved records alone would miss formulas with cross-stem
   inputs.
 
-A notice whose key lists exceed a fixed size carries "refetch" instead.
+A notice whose key lists exceed a fixed size carries "correct" instead.
 
 **What a client does.** It intersects the moved keys with its window. A fold row has no
-maintained key, so it maps member keys through its own remap first. It then refetches
-what moved. It refetches everything when it sees a publication gap, a new
-`document_generation` or host instance, its shape in the eviction list, or a notice it
-cannot read. A slow client may merge pending notices: the union of keys, the covered
+maintained key, so it maps member keys through its own remap first. It then fetches what
+moved. It asks for a correction when it sees a publication gap, a new
+`document_generation` or host instance, its shape in the eviction list, a notice it
+cannot read, or a dropped hop. A slow client may merge pending notices: the union of keys, the covered
 range of publications, and axis changes kept in order. Because the wire is lossless, outputs keep the
 circuit's bit identity end to end.
 
@@ -336,11 +345,13 @@ test):
 8. delivery.
 
 Step 8's required tests:
-- `[AddItem, SetCell]` publishes one notice, and no client refetches;
+- `[AddItem, SetCell]` publishes one notice, and no client asks for a correction;
 - a dropped notice is detected;
-- a reconnect after a host restart refetches;
+- 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 refused frame consumes no publication number;
-- a dropped hop forces a refetch.
+- a dropped hop triggers a correction.
 
 ## Open questions