diff --git a/sw-block/design/v3-recovery-algorithm-consensus.md b/sw-block/design/v3-recovery-algorithm-consensus.md
index bfcb41104..1ec6b357b 100644
--- a/sw-block/design/v3-recovery-algorithm-consensus.md
+++ b/sw-block/design/v3-recovery-algorithm-consensus.md
@@ -24,7 +24,7 @@ These are **not** preferences — they are the **minimal joint axioms**. Everyth
 ### 1. Boundary & truth (**P1**)
 
 - **Recover is a bounded session**, not ambient state (`StartSession … EndSession` / fail).
-- **Authoritative convergence** toward **healthy replicated state** is proven only via **explicit barrier handshake** **`AchievedLSN ≥ engineered target`** together with **`baseDone` / layer-1 conjunct as defined by product**. **Inferring “done” from traffic silence, Kind ratios, or sender idle windows is forbidden.**
+- **Authoritative convergence** toward **healthy replicated state** is proven only via **explicit barrier handshake** whose **`AchievedLSN`** and receiver conjuncts match the **engine-authored cut semantics** for **that session** (**§6.9**, **§IV `T2`**) together with **`baseDone` / layer-1 conjunct as defined by product**. **Inferring “done” from traffic silence, Kind ratios, or sender idle windows is forbidden.**
 
 ### 2. Exactly one causal WAL frontier per peer-session (**P2**)
 
@@ -54,7 +54,8 @@ These are **not** preferences — they are the **minimal joint axioms**. Everyth
 
 ### 7. Engine owns trigger numbers (**P7**)
 
-- **`fromLSN` / `pinLSN` / `targetLSN`** are **frozen or engine-authored** facts at session admission; transport **silently overwriting** (`fromLSN := 0` when engine chose `R+1`) violates **parity** with decision logic.
+- **`fromLSN` / pin lower bound** (**`pinLSN` when product distinguishes them**): **frozen or engine-authored** at session admission; transport **silently overwriting** (`fromLSN := 0` when engine chose `R+1`) violates **parity** with decision logic.
+- **`targetLSN` (when carried on wire / coordinator)**: names **only** the **historical WAL job upper bound `Y`** per **§6.9** — **not** the Primary tape’s physical end (**`head` keeps moving**). Implementations MUST NOT treat “`shipCursor` reached `targetLSN`” as equivalent to **`cursor == head`** or **steady healthy** unless **§6.9 Phase C** is already satisfied under the closed **§IV `T2`** semantics.
 
 ---
 
@@ -122,6 +123,55 @@ Implementations **must** obey the **scheduler choices** below. Prose **`send(...
 
 **Dual-mode carve-out (**`WalShipper`**)**: **`ModeBacklog`** vs **`ModeRealtime`** (**steady / no substrate replay**) is **architect‑approved** under **`§13 — E‑WALSHIPPER‑DUAL‑MODE`**. **`§6.3**(A)(B)** and **§6.8**(3)(4)(9) remain **literally normative in Backlog**; Realtime semantics **do not** replace **P2 / §6.8(1)/(5) / §6.4**.
 
+##### Reference pseudocode — **`Drive(input)`** (**single serializer**, **`HOPE‑SHIPPER‑MONOTONIC`**)
+
+**Purpose**: every reviewer instantiates the **same** (**a**) state, (**b**) atomic boundaries, (**c**) **`INV`** links — not a second informal compilation.
+
+**Dense‑LSN product**: sparse / non‑contiguous LSNs **`MUST`** replace literal **`+1`** step and dense **`ReadAtLSN`** with **`NextPresentLSN` / product scan — **architect leaf**. **Substrate** **`ReadAtLSN(k)`** is **semantic** only — **batch prefetch** **MAY** hide behind it (**mini-plan §12.4 #1**).
+
+**§6.1 / §V (`CHK‑RECOVER‑REWIND‑ONCE`) alignment**: **`cursor`** here is **`next LSN to emit`** (**same convention as **`v3-recovery-wal-shipper-spec.md` §7.1** `while cursor < head`**). **`§6.1 **`cursor[P] := fromLSN`** **and** engine **`fromLSN`** **MUST** be paired so **first lawful ship `lsn`**, **`ReadAtLSN(cursor)`** (debt path), and receiver **`expect_next_LSN`** after rewind (**spec §7.4**) **agree** — **exclusive‑floor **`fromLSN`** ⇒ commonly **`cursor := fromLSN+1`** for first frame **`lsn = fromLSN+1`**; **inclusive / product variants** **`MUST`** document the mapping **without** drifting **`Drive`** cases.
+
+```text
+# —— (a) STATE (per peer P, under one serializer lock) ——
+state:
+    cursor : LSN                    # next LSN to emit (unsent prefix starts at cursor; §6.2 debt = cursor < head)
+    fifo   : queue<Append>          # single mailbox — NO separate backlog/live queues
+    head() : LSN                    # consistent read: exclusive next-assign slot (dense: new append takes lsn==head, then head++)
+
+# —— (b) ATOMIC BOUNDARY — entire body runs under shipMu / single-writer serializer (P2, §6.4) ——
+# Event sources:
+#   NotifyAppend(...) → fifo.push(Append); Drive(peek)
+#   timer / ShipOpportunity      → Drive(∅)
+
+def Drive(input):   # input ∈ { ∅, Append{lba,lsn,data} }
+
+    # CASE A — debt: next emit exists before tail (cursor < head).
+    # FIFO: pending Append WAITS (§6.3(A) “incoming does not overtake debt”).
+    if cursor < head():
+        e := substrate.ReadAtLSN(cursor)          # MUST be the record at exactly this LSN (dense)
+        emit(e.lba, e.lsn, e.data)
+        cursor := cursor + 1                      # exactly one LSN advanced
+        return                                    # input (if any) stays in fifo
+
+    # CASE B — no debt: cursor == head. Tail path (steady / post-catch-up).
+    if input is Append{lba, lsn, data}:
+        if lsn == cursor:                          # dense: next assigned tail
+            emit(lba, lsn, data)
+            cursor := cursor + 1
+            fifo.pop()
+            return
+        if lsn < cursor:
+            fifo.pop()                              # idempotent retry / duplicate notify
+            return
+        # lsn > cursor — gap / contract violation. NO silent substrate scan to fill (§13 T4a spirit).
+        raise CursorGap{cursor, lsn}              # engine MUST rebuild-on-gap / re-anchor (NEGATIVE‑EQUITY ban on “heal by scan”)
+
+    # CASE C — ∅, cursor == head: nothing to ship
+    return
+```
+
+**Derived invariant (sender → wire)** — **`INV‑WIRE‑WAL‑LSN‑MONOTONIC`**: **successful** **`emit(...)`** sequence in a session yields **strictly increasing `lsn`** with **no gaps** (dense) — **precondition** for **`INV‑RECV‑WAL‑NAIVE`** (**§6.10**).
+
 #### 6.4 Flip / “mode transition” atomicity = **Primary Wal + ship serialization** (**R1**)
 
 The historical **gap-at-flip** bug is **not** a magical “mode bit” — it is **check-then-act** between **“`cursor` caught `head`”** and **a concurrent append** extending **`head`**.
@@ -176,7 +226,111 @@ If **sustained append rate > sustainable ship rate** for the session, **`head−
 
 **Dual-mode scope (`§13`)**: Checklist items **(3)(4)(9)** (debt-before-tail priority, periodic idle drain tied to **`send(∅, debt)`**) are **`MUST`** in **`ModeBacklog`**; **`ModeRealtime`** obeys **`§13 — E‑WALSHIPPER‑DUAL‑MODE`**.
 
-**Still open**: flip hysteresis (**§IV `T1`**), **`targetLSN`** vs **`head` at barrier** (**`T2`**), bearer policy while backlog exists (**`T3`**). Closing those rows **updates** checklist edge semantics but **does not** relax **(1)**–**(4)** **in **`ModeBacklog`**, **`§13`**, or **(9)** as read **`ModeBacklog`**.
+**Still open**: flip hysteresis (**§IV `T1`**), **`targetLSN`** vs **`head` at barrier** (**`T2`** — **process refinement in §6.9** must close into an explicit phased rule before code claims “healthy”), bearer policy while backlog exists (**`T3`**). Closing those rows **updates** checklist edge semantics but **does not** relax **(1)**–**(4)** **in **`ModeBacklog`**, **`§13`**, or **(9)** as read **`ModeBacklog`**.
+
+### 6.9 `targetLSN` — **when to use what words** (**job-bound slice** vs **single-tape ship**)
+
+Normative **`WalShipper`** truth is always **§6.2–6.4**: **one ordered tape**, **`cursor` vs `head`**, **`send(incoming, debt)` / `send(∅, debt)`**, **single serializer** (**P2**). **Recover does not contradict steady Wal**: it temporarily adds **lanes** (**base**, dual‑lane framing), not a **second causal ship owner**.
+
+#### **Receiver-hard invariant — `Y` does not cut the WAL into two tapes**
+
+**Normative**: A numeric **`targetLSN = Y` MUST NOT mean** “Primary WAL becomes **two independent ordered logs** (**≤Y** vs **>Y**).” The replica consumes **one** recover-WAL apply story: **§7 `checkMonotonic` / session state** advances on **every** **`(LSN, LBA, data)`** in **strict LSN order** relevant to **`StartSession..EndSession`**, regardless of wire **frame kind** (`WALKindBacklog` vs `WALKindSessionLive` …) or **whether** Primary used **`ScanLBAs`** vs **`NotifyAppend`** to **choose** emission order.
+
+Permitted meaning of **`Y`** (**only**): a **sender-side scheduling / enumerator bound** (**how** Primary drains its **single** tape into frames) plus a **frozen lineage field for barrier/certification**. **Forbidden**: any design where the receiver treats **≤Y** and **>Y** as **separate ingest frontiers**, **restart rewind semantics**, or **reorder-permitted halves** — that **engineering shape is incompatible** (**applies-before / applies-after fights**, **duplicate or stale LSN**, **barrier nonsense**).
+
+**Informative**: Framing prefixes “historical blob then tail blob” **on the wire** is allowed **only if** arrival + apply preserves **single global LSN monotonicity** as seen by **`RebuildSession`** — i.e. it is **one tape carried in two envelopes**, **not two truths**.
+
+#### **Product veto — interpreting `target` as WAL “segmentation” is negative equity**
+
+If **`targetLSN=Y`** appears in **architecture narrative** as **segmenting WAL** — i.e. “first segment done, mission accomplished” — without **WalShipper `cursor→head`** closure, architects classify that pattern as **`NEGATIVE‑EQUITY`**: recurring sessions, stalled adoption, confusion at **receiver** (**§6.9 invariant**) and **`MinPin`/retention** pressure. **`Y` MAY exist as lineage text** (**§IV `T2`**) but MUST NOT substitute for **tape monotonicity**.
+
+#### **Positive model (`HOPE‑SHIPPER‑MONOTONIC`) — the only durable fix**
+
+Implementations converge by keeping **WalShipper** as the **sole** causal advance of **unsent LSN prefix** (**P2**): **`cursor` moves forward monotonically** on **Primary’s one order** (**§6**), never “two halves decide independently.” Recover **inherits** steady Wal **strategy abstraction** (**§6.3**) — **explicitly**:
+
+| Ship opportunity kind | **`send` form** | Role when **`cursor < head` (backlog / debt)** |
+|-----------------------|----------------|-----------------------------------------------|
+| **No freshly paired append on this tick** | **`send(∅, debt)`** | **Periodic / timer‑driven** **`emit-from-cursor`** — backlog **cannot** rely only on arrivals (**Primary‑idle starvation forbidden** — **§6.8 item 4** **`ModeBacklog`**). |
+| **Append visible / tail visible** | **`send(incoming, debt)`** | **Oldest‑unsent first** whenever debt non‑empty (**§6.3**(A)); **`incoming` extends** tape; **never** mailbox split. |
+
+**Normative shorthand**: backlog’s “extra oxygen” is **empty‑input advancement** (**`send(∅, debt)`**); **choose‑among‑eligible** advancement when **`incoming` exists** is **`send(incoming, debt)`** — **same serializer**, **monotone `cursor`**. **Realtime carve‑outs** (**§13**) do **not** fork this story into **Wal segmentation**.
+
+Some implementations (**today `seaweed_block`**) also carry **`targetLSN = Y`** on **lineage / coordinator**. **Mandatory reading**: **`Y` is not “the WAL tape ends here.”** **`head` may exceed `Y` at any instant** during the same session — new appends **extend** backlog as **`cursor < head`** on the **same** tape (**§6.2 operational debt**). Therefore:
+
+| Phrase | Meaning |
+|--------|---------|
+| **Stream Wal ship** (**primary**) | **`WalShipper` decisions** advancing **`cursor` toward live `head`** under **§6.3 / §13** — **continuous**, append‑fed and timer‑fed in **ModeBacklog** as applicable. |
+| **Historical WAL job bound at `Y` (sender-only helper)** | **Primary-only**: a **bounded substrate read** that emits **backlog-class** frames for **`(fromLSN, Y]`** (e.g. **`ScanLBAs`** stops at **`LSN > Y`**). This is **one emission tactic** on the **same** tape — **not** “first tape then second tape” at the receiver (**see invariant above**). |
+| **`targetLSN = Y`** | **Lineage + coordinator**: freezes **`Y`** for **barrier text** and **sender bookkeeping**; **does not** fork replica apply order. |
+
+#### Recover **process** (how a `Y`-bearing session reaches caught up and stays healthy)
+
+Architects + implementers **MUST** document which phases their code performs; mismatches (**stopping after step 3 alone**) are **§IV `T2` bugs**. **Informative canonical skeleton**:
+
+1. **Admit**: Engine publishes **`fromLSN`** (often **≈ rebuild semantic lower bound**) and **`Y`** (**`targetLSN`**) unchanged to **receiver lineage** (**§I P7**). **Coordinator** **`StartSession`** records both; **`pin`/recycle** obey **§I P6** / pin wire doc.
+2. **Base / extent lane** (**if used**): **GLOBAL block sweep** (**§5**) — dense or sparse **per product** — subject to **`bitmap`** arbitration (**P5**). **Independent of LSN**, except synthetic frontiers pinned by session contract.
+3. **Sender: bounded read for backlog-class frames ending at `Y`**: Emit **`(LSN,LBA,*)`** with **`fromLSN < LSN ≤ Y`** through recover bearer (**does not authorize a second replica WAL frontier** — **§6.9 invariant**).
+4. **Same serializer: tape tail (**`LSN > Y`**) into frames** (**Phase C**) via **WalShipper** only — **`NotifyAppend`**, **SessionLive**/seal, **`DrainBacklog`**, **ModeRealtime** per **§13**; obeys **`cursor→head`**. **`ScanLBAs` stopping at `Y` does not** permit **`cursor < head`** on Primary to stall without **WalShipper** drain (**§6.2**).
+5. **Barrier**: Receiver answers **`AchievedLSN`** consistent with **`Y` + Phase C semantics** (**§IV `T2`** must pin the exact predicate: e.g. **conjunct **`walApplied ≥ Y`** ∧ tail policy ∧ `baseDone`**). **§I P1** completion uses this handshake, **not** “silence after step 3 alone”.
+6. **End session → steady**: **`EndSession`**, steady **`Ship`/`NotifyAppend`** resumes; **`cursor == head`** in steady means **implementation‑lag‑only**, not **semantic policy debt reopened** (**§6.2** last paragraph). **Healthy** ⇒ engine **probe/decision** predicates satisfied (**control plane**, not **`Sender.Run` idle** alone).
+
+#### Anti‑patterns (**normative DON’Ts**)
+
+- **Treat “historical WAL job finished ( enumerator past `Y` / coordinator saw through `Y` )” as “WAL recover done”** while **`head > cursor`** on Primary — **violates §6.2**.
+- **`targetLSN=Y` marketed as WAL segmentation semantics** (**“Tape A then Tape B”**) — **`NEGATIVE‑EQUITY`** (**§6.9 Product veto**) — violates **receiver invariant**.
+- **`targetLSN` as UX throttle** forcing **cheap barrier** followed by **new session churn** whenever **`head` moves**, without **explicit product policy** — **risk per execution institution § Risk envelope**.
+- **`targetLSN` as silent substitute** for **`fromLSN` / rewind** (**P7 parity** violation).
+
+Implementations aiming to **omit `Y`** on wire (**pure stream recover**) MUST still obey **§I P1** barrier conjunct with an **alternative engine‑authored cut** — **rename only**, not weaker proof.
+
+### 6.10 **Receiver recover invariants** — **`bitmap` core** (**P5**) · **WAL naive** · **race‑free arbitration**
+
+**§I P5** already requires **`bitmap`** visibility for **Wal‑claims** vs **base**. **Normative clarification**: the **`bitmap` is not an optional “parallelism tax”** detachable from recover — it is the **receiver’s single arbitration surface** for **“has a Wal touched this LBA in this session scope?”** regardless of whether base is **dense**, **sparse**, **striped workers**, or **wall‑clock overlapped** with Wal (**§6.8 item 6 / G3**). **Dropping `bitmap` in favor of naive base-only apply** is a **different product mode** (typically **serial BASE → Wal**) and **MUST** be labeled as such (**mini-plan §12 candidate “A‑serial”**).
+
+| ID | Invariant (**receiver recover path**) |
+|----|----------------------------------------|
+| **`INV‑RECV‑BITMAP‑CORE`** | **`bitmap`** is the **sole** gate that lets **recover base** mutate an LBA after **Wal** may have asserted **Wal‑truth** on that LBA. **Base apply** **`MUST`** follow a **single critical pattern**: **observe / claim “not Wal‑protected” and write base bytes in one race‑free atomic step** — e.g. **`CAS`/compare‑and‑set** style **`0→1`** on **`bitmap[lba]`** (or **`TryClaimBase(lba)`** with equivalent semantics); **winner** performs **`ApplyBaseBlock`** and sets **`claimed`**; **loser** **skips** base write. **Wal apply** **`MUST NOT`** rely on a **read‑then‑later‑write** of **`bitmap`** that can interleave with base (**§6.10 anti‑pattern** below). |
+| **`INV‑RECV‑WAL‑NAIVE`** | **Recover Wal tuples** (**`frameWALEntry`**) **`MUST`** apply with **substrate LWW** (**write payload**) **without** consulting **`bitmap`** before write **for stale‑Wal micro‑comparison** — **Wal vs Wal ordering** is **`LSN`** monotonic on the **single ingest frontier** (**§6.9 receiver-hard**, **`checkMonotonic`**, precondition **`INV‑WIRE‑WAL‑LSN‑MONOTONIC`** **§6.3** pseudocode). After successful Wal substrate write, **`MUST`** **set **`bitmap`/Wal‑claim** for **`lba`** so **later base** loses **`CAS`**. Ordering inside the implementation **`MUST`** be **Wal data durable before observable claim** (or use one **`per‑LBA` / `shipMu`‑compatible** serialization that merges data+claim — product picks; **wrong interleavings** ⇒ **NEGATIVE‑EQUITY‑class bugs**). |
+
+##### Reference pseudocode — **`ApplyWAL` / `ApplyBASE`** (**per‑LBA atomic envelope`)
+
+**Naming**: **`store.lock(lba)`** = **one race‑free critical section** **`MUST`** cover **`data write` ∪ `bitmap` transition** together — equivalent **`bitmap.CAS`** patterns — **informative** notes below.
+
+```text
+# —— (a) STATE ——
+state:
+    bitmap : array[NumLBAs] of bit, init 0      # CORE — INV-RECV-BITMAP-CORE
+    store  : substrate                          # exposes per-LBA lock OR global writer (see equivalence note)
+
+# —— WAL — precondition: ingest order ≡ strict LSN increase (INV-WIRE-WAL-LSN-MONOTONIC §6.3) ——
+def ApplyWAL(lba, lsn, data):
+    with store.lock(lba):                       # atomic envelope (INV-RECV-BITMAP-CORE + WAL-NAIVE)
+        store.write(lba, data)                  # naive LWW vs prior Wal bytes — no bitmap pre-check
+        bitmap[lba] := 1                        # claim set BEFORE releasing lock
+
+# —— BASE — may race WAL on same lba under BASE ∥ WAL (§6.8 #6) ——
+def ApplyBASE(lba, data):
+    with store.lock(lba):                       # SAME lock family as ApplyWAL
+        if bitmap[lba] == 0:
+            store.write(lba, data)
+            bitmap[lba] := 1
+        # else: Wal already authoritative for this session scope — stale base snapshot SKIP
+
+# ANTI-PATTERN (banned — same prose as §6.10 DON’T below):
+#   if bitmap[lba] == 0:
+#       with store.lock(lba): store.write(lba, data)
+#       bitmap[lba] := 1
+```
+
+**Informative equivalence**: if substrate serializes **all** **`Apply*`** via **one** goroutine, lock may degrade to **global queue** + **`bitmap` atomic** — **`CAS`**‑only formulations **remain valid** (**§9** tests **may** simulate either).
+
+**Informative (**substrate **`Write` arity**)**: **`ApplyBASE`** payloads **typically lack author Wal **`LSN`****; **synthetic frontier** for extent layer **MAY** use **session **`targetLSN` / lineage anchor** per **`RebuildSession` / §5** — **architect** pins if **`Write(lba, data, effectiveLSN)`** becomes required.
+
+**Anti-pattern (normative DON’T)** — **`read bit; compute elsewhere; later base write`** without **`CAS`/lock** vs concurrent **`Wal`** — permits **Wal data then base overwrite** (**lost update**).
+
+**Session scope**: recover **`bitmap`** state **`SHOULD`** be **scoped to `StartSession…EndSession`** (or **`RebuildSession`** lifetime) **unless** substrate definition extends Wal‑claims — **explicit** in leaf spec (**architect**) so **`streamBase`/parallel base** races cannot cross **stale boundaries**.
+
+---
 
 ### 7. Replica routing table (**P5 operationalized**)
 
@@ -186,7 +340,7 @@ If **sustained append rate > sustainable ship rate** for the session, **`head−
 | Recover `frameWALEntry` | WAL tuple | Substrate apply **+** **`bitmap` WAL-claim** |
 | Recover `frameBaseBlock` | Bytes | **`bitmap` gate** → **`ApplyBaseBlock` / synthetic frontier** |
 
-**`checkMonotonic`**: protocol defense on **recover WAL** stream (**gap / backward / dup / +1**).
+**`checkMonotonic`**: protocol defense on **recover WAL** stream (**gap / backward / dup / +1**). **Bitmap / base race atomicity** (**`INV‑RECV-*`**) — **`§6.10`**.
 
 ---
 
@@ -215,7 +369,7 @@ Bearer differs; **§7 semantic is P3**.
 | ID | Open question | Why it can bite at code time |
 |----|----------------|------------------------------|
 | **T1** | **“Caught up” / flip policy** (**refines §6.4**): strict `cursor == head` vs hysteresis **`head − cursor < ε`** vs **time-based idle**; **product** semantics when **flip races append** — serializer already required | Premature declaring **normal** ⇒ **gap** if **outside §6.4**; late flip ⇒ long session / pin |
-| **T2** | **`targetLSN` vs moving `head`**: if **`head > target`** at session start, does backlog drain stop at **target** for **barrier** only, or always emit to **head**? **Related (§6.2)**: **catch-up closes `cursor→head` gap** (operational debt), not “match **`head`’s value at an instant**”; **barrier / pin** still need an **engine-chosen cut** agreed with receiver. | **Barrier false negatives** or **double application** if sender/receiver disagree |
+| **T2** | **Close into §6.9 + explicit barrier predicate** — **`Y` never forks receiver WAL ingest** (**one LSN-monotonic stream**); **`targetLSN = Y`** is **sender enumerator / lineage freeze** only; **tail** **`LSN > Y`** ships via **WalShipper** same session (**Phase C**); **Barrier `AchievedLSN`** predicate agreed with replica (**exact tail clause** vs **moving `head`**) (**§IV T2 residual**). | Premature success, duplicate/stale apply, or **ordering chaos** if **≤Y vs >Y** modeled as **split tapes** |
 | **T3** | **Bearer choice while `cursor < head`**: **steady bearer silent vs dual-lane only** (**§II–§III** closes); **either way** obey **§6 P2 single serializer** | **P2** if two pumps both emit unconsumed prefix |
 | **T4** | **Duplicate** `lsn == applied` on recover path: **hard error** vs **idempotent no-op** | Retransmit policy vs **checkMonotonic** |
 | **T5** | **Sparse base** vs dense full-LBA — contract with **bitmap** density | Performance / correctness on huge volumes |
@@ -268,7 +422,7 @@ Controlled relaxations of **§6** prose **without** weakening **§I**. Each row
 | **Motivation (**T4a / fresh receiver**)**: Substrate‑scan WAL ship during **steady Realtime** **`NotifyAppend`** can replay **dead‑window** bytes and violate **no‑replay** session invariants asserted by tests/product. |
 | **`ModeBacklog`** (recover / catch‑up Wal path on WalShipper) | **`§6.3**(A)** `send(incoming, debt)`, **`§6.3**(B)** `send(∅, debt)` / periodic **`ShipOpportunity`**, and **§6.8**(3)(4)(9) **`MUST`** hold **in full**. Timer **`MUST`** attempt **`emit-from-cursor`** when **`cursor < head`** even if Primary append‑idle (**§6.8 item 4**). **Priority (= oldest unsent)** **`MUST`** use substrate **`ScanLBAs`** (or equivalent single‑tape authoritative read). |
 | **`ModeRealtime`** (steady per‑append **`NotifyAppend`**) | **Literal §6.3(B)** “idle timer **`MUST`”** **`MUST NOT`** apply — ship is **`NotifyAppend`**‑driven. **Hot path **`MUST NOT`** substrate‑replay** for ship byte selection (**caller `data`** is canonical on optimized tail emit). **`send(incoming, debt)` debt‑priority **`MUST NOT`** be re‑interpreted as “Realtime must drain before tail”**: gap **`cursor < head`** **`MUST`** be corrected only via **`ModeBacklog`** + **`DrainBacklog`** / coordinator **re‑anchor**, not Realtime substrate scan. **`CHK‑WALSHIPPER‑TIMER‑DRAIN`** applies to **Backlog** only (see **§12** predicate). |
-| **Safety switch** | Implementations **SHOULD** expose **`StrictRealtimeOrdering`**: **log‑warn** on **`lsn ≠ cursor + 1`** (dense WAL) **by default**; **strict / error path** optional **production** opt‑in. **Hard opt‑in** (`strict=true`): engine **SHOULD** require prior proof of **ordering discipline** (**rebuild‑on‑gap**, fresh peer policy). Operational detail **`v3-recovery-wal-shipper-mini-plan.md` §11.6**. |
+| **Safety switch** | Implementations **SHOULD** expose **`StrictRealtimeOrdering`**: **log‑warn** on dense WAL when **`NotifyAppend`** **`lsn`** **≠** **`expected_next_tail`** **by default** — **canonical** (**§6.3 **`Drive`**, **`cursor` = next emit**): **`lsn == cursor`** on the debt‑free path; **`lastEmitted`‑style** internal fields **`MUST`** compare **`lsn == lastEmitted + 1`** **equivalently** (**single contract** across shipper code, **`Drive`** prose, and tests). **Strict / error path** optional **production** opt‑in. **Hard opt‑in** (`strict=true`): engine **SHOULD** require prior proof of **ordering discipline** (**rebuild‑on‑gap**, fresh peer policy). Operational detail **`v3-recovery-wal-shipper-mini-plan.md` §11.6**. |
 | **Not relaxed** | **P2** single serializer (**§6.8(1)**); **§6.4** (**R1**); **§6.8(5)** framing≠second tape; **§6.6** (**R2**) observability hooks; **§I P1–P7**. |
 
 **Doc bridge**: **`v3-recovery-wal-shipper-mini-plan.md`** **§11.2 dual‑mode contract** ⇄ this exception.
@@ -289,18 +443,23 @@ Controlled relaxations of **§6** prose **without** weakening **§I**. Each row
 | **2026-04-30** | **v3.7**: **`§6.8` implementer checklist** (single serializer, priority, timer drain, framing≠tape, **`G3` pointer**); **§V** **`CHK-WALSHIPPER-TIMER-DRAIN`** |
 | **2026-04-30** | **v3.8**: **§6.2–6.3** — **policy vs operational debt**, **moving-target / gap→0**, **`send(incoming, debt)` / `send(∅, debt)`** strategy abstraction + **steady debt-free sends**; **§6.8** item **(9)**; **`T2`** cross-ref |
 | **2026-04-30** | **v3.9**: **§13** (**E‑WALSHIPPER‑DUAL‑MODE**); **`§14`/`§15` renumber**; **§6.3** carve‑out pointer; **`CHK‑WALSHIPPER‑TIMER‑DRAIN`** scoped per **§13** |
+| **2026-04-30** | **v3.10**: **§6.9** — **`targetLSN=Y`** as **historical WAL job bound** (`(fromLSN,Y]`) vs **WalShipper `cursor→head` stream**; phased **recover process**; **§I P7** / **P1** / **§IV T2** aligned (**`Y` is not tape end**) |
+| **2026-04-30** | **v3.11**: **§6.9** — **receiver-hard invariant**: **`Y` MUST NOT denote two WAL tapes** / **dual apply frontiers**; **one LSN order** (**frame kind ≠ second truth**) |
+| **2026-04-30** | **v3.12**: **§6.9** — **`NEGATIVE‑EQUITY`** if **`target`** read as WAL **segmentation**; **`HOPE‑SHIPPER‑MONOTONIC`**: backlog = **`send(∅, debt)`** + **`send(incoming, debt)`** (**§6.3**) |
+| **2026-04-30** | **v3.13**: **§6.10** — **`INV‑RECV‑BITMAP‑CORE`** (**`CAS`‑style base**); **`INV‑RECV‑WAL‑NAIVE`**; **`bitmap`** = **core P5 arbitration** (not optional “parallel bit” alone); session scope |
+| **2026-04-27** | **v3.14**: **§6.3** — normative **`Drive(input)`** pseudocode (**state / atomic boundary / `INV‑WIRE‑WAL‑LSN‑MONOTONIC`**); **§6.10** — **`ApplyWAL`/`ApplyBASE`** pseudocode (**`INV‑RECV‑*`**); **§6.1/§V** cursor↔rewind alignment note; **§13** **`StrictRealtimeOrdering`** keyed to **`Drive`** **`cursor`** convention |
 
 ### 15. Document map
 
 | Doc | Role |
 |-----|------|
-| **This** | **Foundation + index**; **`§6.8`** implementer checklist; **`§13`** architect-approved exceptions (**E‑WALSHIPPER‑DUAL‑MODE**) |
+| **This** | **Foundation + index**; **`§6.8`** checklist; **`§13`**; **`§6.3`/`§6.9–§6.10`** — **`Drive`/`Apply*`** pseudocode, **`INV‑WIRE‑WAL‑LSN‑MONOTONIC`**, **`NEGATIVE‑EQUITY`**, **`HOPE‑SHIPPER‑MONOTONIC`**, **`INV‑RECV‑BITMAP‑CORE`** / **`INV‑RECV‑WAL‑NAIVE`** |
 | `v3-recovery-pin-floor-wire.md` | Pin bytes |
 | `v3-recovery-wal-shipper-mini-plan.md` | **Implementation bridge** (**seaweed_block** phased PR ↔ spec §INV) |
 | `v3-recovery-wal-shipper-spec.md` | **WalShipper algorithm** (priority, **R1**, **INV-***) |
 | `v3-recovery-unified-wal-stream-*.md` | **Align to WalShipper spec** or mark superseded |
 | `v3-recovery-wiring-plan.md` | Ports / flags |
 | `v3-recovery-inv-test-map.md` | INV ↔ tests |
-| `v3-recovery-execution-institution.md` | Lifecycle + **risk envelope** / spec→delete-code ordering |
+| `v3-recovery-execution-institution.md` | Lifecycle + **risk envelope** / spec→delete-code ordering + **entity layering & assembly contract** (SW: where **attempt** / muscles may attach) + **§ Management plane vs data-plane recover** (**single index** for probe / quorum / RF>2 admission — **no parallel recovery hub**) |
 | `v3-recovery-live-line-backlog-spec.md` | Retired stub → **here** |
 | `v3-storage-logical-pin-gate.md` | **LogicalStorage substrates + `RecycleFloorGate` / pin** |
diff --git a/sw-block/design/v3-recovery-wal-shipper-mini-plan.md b/sw-block/design/v3-recovery-wal-shipper-mini-plan.md
index 283ef4a29..aae67924d 100644
--- a/sw-block/design/v3-recovery-wal-shipper-mini-plan.md
+++ b/sw-block/design/v3-recovery-wal-shipper-mini-plan.md
@@ -3,7 +3,7 @@
 **Status**: Draft — executable sequence from **`v3-recovery-wal-shipper-spec.md`** to **`seaweed_block`** concrete diffs.  
 **Supersedes narrative scope of**: **`v3-recovery-unified-wal-stream-mini-plan.md` §3.2 (#3 unified stream implementation)** — that track treated recovery `sender` as the Wal scheduler; **non-compliant** with consensus **§6** + wal-shipper-spec **INV-NO-DOUBLE-LIVE**. Architect may add formal **SUPERSEDED** banners on kickoff/unified docs; **this file does not block on that.**
 
-**Normative**: **`v3-recovery-wal-shipper-spec.md`** (**§2–§§7**) + **`v3-recovery-algorithm-consensus.md`** **§I / §II §6**.
+**Normative**: **`v3-recovery-wal-shipper-spec.md`** (**§2–§§7**) + **`v3-recovery-algorithm-consensus.md`** **§I / §II §6** (**§6.3 `Drive`**, **§6.10 `Apply*`** pseudocode).
 
 **Anti‑archive branch**: **`g7-redo/unified-wal-impl`** — **do not PR** as WalShipper truth; cherry-pick only **tests/fixtures** if still valid after refactor audit.
 
@@ -138,6 +138,9 @@ Wal-shipper-spec **§9** names coarse tests — here map **package + style**:
 | 2026-04-30 | v0.6 — **Dual-mode **`ModeBacklog`/ModeRealtime`** + consensus **`§13` E‑WALSHIPPER‑DUAL‑MODE** (**T4a carve-out**) — rewrote **§11.2**, **§11.3** `#3/#4/#9`, §11.4 anchors, §11.5 (**StrictRealtimeOrdering**, TOCTOU); **§11.6 migrations** (**replicaID**, rebuild-on-gap); CHK/timer scope = **Backlog** |
 | 2026-04-30 | v0.7 — **§11.6** + **`v3-recovery-execution-institution.md`** **Entity layering & assembly contract** (**architect → SW**); Phase 0 **replicaID** vs Phase 1 **attempt binder** guardrails |
 | 2026-04-30 | v0.8 — **§11.7** heavy integration proof (**manager-assembled session**): pillars **WalShipper / dual-line / receiver convergence**; ordering **Phase 0 → (2) fault-inject → matrix → soak** |
+| 2026-04-30 | v0.9 — **§11.7 pillar 3**: **slice-2** **`190ee56`** (`TestPillar3Slice2_EngineDriven_SameLBAArbitration`); **T2 / hardware soak** called out **open** pending §IV |
+| 2026-04-30 | v0.10 — **§12** **design candidate** — §6.9‑driven **Drive** simplification + **three receiver models** + **`bitmap`/`CAS`** (**consensus §6.10** cross-ref); **not** normative until architect promotes |
+| 2026-04-27 | v0.11 — **§12.3**: **normative `Drive` = consensus §6.3 only** (remove duplicate sketch); **§12.1–12.2** cross-ref **§6.3** |
 
 ---
 
@@ -297,9 +300,48 @@ Choice — **per-connection format dispatch**, not single-format unification. Du
 |--------|------------|---------------------|
 | **1 — WalShipper: backlog vs incoming** | **`ModeBacklog`**: timer + **`DrainBacklog`** / **`ScanLBAs`**, **`NotifyAppend`** lag-only; **`ModeRealtime`**: **`NotifyAppend`** tail + **`StrictRealtimeOrdering`**; **§13** carve-out | `core/transport`: **`TestC2_*`**, **`TestWalShipper_*`**, **`replicaid_unified_test`**; add **assembled-path** sessions (real **`RecoverySink`**, not shipper-only) |
 | **2 — Dual-line execution** | **BASE ∥ WAL** overlap, **`writeMu`**-bounded interleave; correct **profile / port**; **no corrupted frames** | **`TestC3_BaseWalParallel_FramesInterleave`**, dual-lane E2E; **item (2)**: **C3 ctx fault-injection** (**`7d051e2`** — `TestC3FaultInjection_BaseError_WalExitsViaCtx` / `_OuterCancel_BothLanesWindDown` / `_WalError_RunTerminates_NarrowVariantA`); assembled-stack lift (**`9f62ebe`** — `TestPillar2A_BaseError_AssembledStack_FailReason` / `TestPillar2B_LiveWrites_HighPressure_BarrierIntegrity` / `TestPillar2C_WireAbortMidSession_AssembledStack_RestoresEmitContext`) |
-| **3 — Receiver recover convergence** | Replica accepts **interleaved base + WAL** on recover path, **bitmap / `checkMonotonic`**, **barrier `achievedLSN`**, moves toward **idle / healthy** | **`core/recovery` E2E**, **`dual_lane_engine_test`**, **`replication/component` cluster**; stress: **live writes during session**; **T2** when §IV closed. **Slice-1 landed 2026-04-30** (**`291e652`** + polish **`3495a12`**) — `TestPillar3Slice1_ReceiverConvergence_LiveOverwritesBacklog_SameLBAs` (transport-stack only; **slice-2** lifts to engine-driven path via `dual_lane_engine_test.go`) |
+| **3 — Receiver recover convergence** | Replica accepts **interleaved base + WAL** on recover path, **bitmap / `checkMonotonic`**, **barrier `achievedLSN`**, moves toward **idle / healthy** | **`core/recovery` E2E**, **`dual_lane_engine_test`**, **`replication/component` cluster**; stress: **live writes during session**; **T2** when §IV closed (hardware soak — **still open** pending §IV). **Slice-1** (**`291e652`** + polish **`3495a12`**) — `TestPillar3Slice1_ReceiverConvergence_LiveOverwritesBacklog_SameLBAs` (transport stack). **Slice-2** (**`190ee56`**) — `TestPillar3Slice2_EngineDriven_SameLBAArbitration` (full adapter→engine→executor dispatch; **`RouteSessionLane`** on each live push). Slice-3+ / wire-tap / C3‑#2B **optional backlog** |
 
 **Order**: **(1)** Phase 0 **committed + §11.6 receipt (SHA)** → **(2)** fault-injection → **(3)** widen matrix → **hardware soak** (**T2 / T7**).
 
 **Stop rule**: Failure at **assembled-session** layer → fix **algorithm / wiring** before **Phase 1** (binder fixes **identity**, not WAL/base correctness).
 
+---
+
+## 12. Design candidate — **`§6.9`‑driven shipper/receiver simplification** (**not normative until promoted**)
+
+**Status**: **Design candidate** — for **architect decision**; **does not** replace **§11.2–§11.7** receipts or **§13** until consensus + this section are **explicitly revised** and code lands on a **named branch**.
+
+### 12.1 **Document stack** — what SW should read in what order
+
+| Layer | Doc | Role |
+|-------|-----|------|
+| **Consensus** | **`v3-recovery-algorithm-consensus.md`** **§I P5**, **§6.2–6.4**, **§6.3 `Drive`**, **§6.9**, **§6.10** (`Apply*` pseudocode), **§13**, **§IV T2** | **Normative** truth: single tape intent, **`targetLSN`** non‑segmentation, **`send(∅,·)`/`send(incoming,·)`**, **`bitmap`** CORE + **`INV‑RECV-*`** race rules. |
+| **Algorithm leaf** | **`v3-recovery-wal-shipper-spec.md`** **§7** | **Implementable sketches** (**§7.1 loop**, **receiver rewind + monotone §7.4**); **primary recover emit** = **§6.3 `Drive`** (**normative consensus**); **`Apply`/`bitmap` detail** ⇒ **§6.10**. |
+| **Bridge / receipts** | **This mini-plan §11** | What **already merged** on **`g7-redo/wal-shipper-impl`** + **pilots**. |
+| **This §12** | **Candidate refactor** | **Single normative `Drive(input)`** (**consensus §6.3** — **avoid duplicating here**); barrier‑only **`target`**, receiver **Wal naive**, **bitmap `CAS`** base — **diff** from today's **dual‑mode + bridging sink**. |
+
+### 12.2 **Receiver — three models** (clears SW confusion)
+
+| Model | WAL apply | BASE vs WAL | Typical cost |
+|-------|-----------|-------------|--------------|
+| **① Today bridging sink + ordered seal** | **Naive substrate write** | **Mostly ordered by sender buffer/seal luck** — **§6.8 #6 parallelism still risky under races** | No **per‑LBA Wal** table; **ordering not a hard invariant** without proof. |
+| **②** (**`NEGATIVE‑EQUITY`**) | Needs **per‑LBA Wal frontier** (**e.g. 64‑bit last‑LSN**) for stale compare | **Dual WAL truth** at receiver — violates **§6.9** mono‑ingest story | **Expensive** |
+| **§6.9 / §12 candidate (`HOPE‑SHIPPER‑MONOTONIC`)** | **`INV‑RECV‑WAL‑NAIVE`**: naive write; **Wal–Wal order = wire LSN order** (**sender `cursor` monotone + single apply frontier**) | **`INV‑RECV‑BITMAP‑CORE`**: **`bitmap` not optional ornament** — **sparse / dense / parallel base** all **CAS (or equiv.)‑gate** base; **Wal sets claim after write** (**§6.10**) | **Small `bitmap` + `CAS`**; **drops** brittle **dual‑mailbox Wal** story. |
+
+**Key correction for SW**: **`bitmap`** is **`P5` core arbitration for BASE vs WAL**, not “only pay 1‑bit because we chose parallel BASE.” **`§6.10`** pins **`CAS`/atomicity** so **Wal data vs lazy base check** cannot **race‑overwrite**.
+
+### 12.3 **Candidate sender** — normative reference only
+
+**Normative pseudocode** **`Drive(input)`**: **`v3-recovery-algorithm-consensus.md` §6.3** — **do not** fork a second **`Drive`** sketch in this mini‑plan (prevents **§6 ↔ §12** drift). **§12.4 #1** (**`ReadAtLSN`** vs prefetch **N**) and **`targetLSN=Y`** barrier semantics remain **architect / implementation** leaves.
+
+### 12.4 **Architect checklist** (open before implementation)
+
+| # | Topic | Decision |
+|---|-------|----------|
+| **1** | **Substrate** | **`ReadEntryByLSN`** vs **prefetch‑N inner queue** (same observable **next‑emit **`cursor`** advancement** vs **§6.3 **`Drive`**) — **WalStore/smartwal index** cost |
+| **2** | **`target`/lineage** | **Barrier admission only** + **§IV T2** sweep for **legacy hidden dependencies** |
+| **3** | **`bitmap` lifetime** | **Session‑scoped**, cleared / reset on **`EndSession`** (**exact hook** ties **receiver FSM**) |
+| **4** | **`streamBase`** | **`groupCtx`** / **fail‑fast with `Drive`** (**C3 #2B** follow‑up) |
+| **5** | **BASE vs WAL wall‑clock** | **Candidate B** (overlap + **`§6.10`**) vs **A** (serial BASE→Wal **may relax `bitmap` policy** explicitly) |
+
diff --git a/sw-block/design/v3-recovery-wal-shipper-spec.md b/sw-block/design/v3-recovery-wal-shipper-spec.md
index ee470d07b..d4ee432d4 100644
--- a/sw-block/design/v3-recovery-wal-shipper-spec.md
+++ b/sw-block/design/v3-recovery-wal-shipper-spec.md
@@ -15,6 +15,7 @@
 | In scope | Out of scope (link elsewhere) |
 |----------|--------------------------------|
 | **One ordered Wal tape** on Primary: `head`, per-peer **`cursor[P]`**, **emit** order to **P** | **Extent/base bulk** — `v3-recovery-algorithm-consensus.md` §5; bytes `v3-recovery-pin-floor-wire.md` |
+| **§7.3 — sender recover emit** (**normative = consensus **`Drive`**) · **§7.4** — illustrative **recover receive** rewind + monotone + **`bitmap`** pseudocode (**consensus §II §7 routing**) | **§7.4** **`ApplyWalWithWalClaimBitmap` / **`ApplyBaseUnderBitmapGate` **→** **`v3-recovery-algorithm-consensus.md` §6.10** pseudocode (**`INV‑RECV‑*`**). Receiver detail — **`seaweed_block`** `core/recovery` + tests; **`checkMonotonic`** |
 | **Single serializer** for “next LSN sent to P” (**P2**) | Receiver **`checkMonotonic`**, **`bitmap`** — consensus §7; replica apply |
 | **R1** transition (caught-up vs append race) | **Engine** retry / escalate after fail-close — executor / engine |
 | **R2** saturation observability hooks | **`MinPin`/recycle** full story — coordinator + substrate |
@@ -119,7 +120,9 @@ Timer **priority drain** (**§4**) remains required for **liveness** but **does
 
 ---
 
-## 7. Pseudocode (**reference shape**)
+## 7. Pseudocode (**reference shapes**)
+
+### 7.1 Primary **`WalShipper`** core loop (**steady + recover**)
 
 ```text
 // One goroutine OR all entrypoints take shipMu.
@@ -148,7 +151,89 @@ function EmitAccordingTo§4UntilBudgetOrBlocked():
         emit(head); clear pending_tail_flag  // depends on refactor; simplest: append path calls Emit once after advancing head while cursor tracked
 ```
 
-Implementations **flatten** this; the **semantic** contract is **§3–§5**, not the sketch’s loop details.
+Implementations **flatten** this sketch; **§3–§5** remain the semantic contract.
+
+### 7.2 **Recover-visible high layer** (**session** + **`backlog` pointer**)
+
+Pairs with **`v3-recovery-algorithm-consensus.md` §6.9** (**`NEGATIVE‑EQUITY`**, **`HOPE‑SHIPPER‑MONOTONIC`**). Recover adds **no** parallel “Wal ownership” beside:
+
+| Artifact | Meaning |
+|----------|---------|
+| **Recover session envelope** | **`sessionID`, epoch/ev, lineage`** (may carry optional **`targetLSN=Y`** as **frozen lineage text** — **not** a backlog pointer — **never** WAL segmentation rhetoric). |
+| **Backlog pointer** | **`cursor`** on the **same** Primary tape — **`cursor < head` ⇔ debt** (**§6.3** **`send(incoming, debt)`** / **`send(∅, debt)`**). |
+
+```text
+type RecoverSessionView = record
+    session_id : uint64
+    lineage    : opaque   // echoed on bearer + barrier; includes engine-authored fromLSN/target text
+end
+
+// cursor + head owned ONLY by WalShipper (§2). Executor/coordinator publishes RecoverSessionView + brackets.
+WalShipper.OnRecoverSessionBracket(StartSession(fromLSN), …, EndSession)
+```
+
+### 7.3 **Primary recover — monotone emit**
+
+**Normative**: **`v3-recovery-algorithm-consensus.md` §6.3 — reference pseudocode `Drive(input)`** — single **`fifo`**, **`cursor < head ⇒ ReadAtLSN(cursor)` before tail**, **`lsn > cursor` ⇒ `CursorGap`** (**no realtime scan‑fill**). **`(a)`** state, **`(b)`** **`shipMu`** atomic boundary, **`(c)`** **`INV‑WIRE‑WAL‑LSN‑MONOTONIC`**.
+
+Optional **`ScanLBAs(...,≤Y]`** emits **Backlog‑class** frames yet **still** advances **`cursor`** only **under **`shipMu`** — **INV-SINGLE** / **INV-MONOTONIC-CURSOR** unchanged.
+
+**Informative**: one lock hold often **loops** **`Drive(∅ | fifo.peek())`** until transport budget clears or **blocked** — **observable semantics remain** **`Drive`** **per step** per **§6.3**.
+
+### 7.4 Replica recover session (**monotone receive**, **one rewind**, **`bitmap` overlap**)
+
+**“One rewind”**: not an arbitrary backward LSN cascade — the session **resets** ingest expectation to **`fromLSN + 1`** (dense default; **`CHK-RECOVER-REWIND-ONCE`** in **consensus §V §12**), validates the **first lawful** recover-WAL frame, then **`monotonic_armed`** — only **strict monotone** (`checkMonotonic`) thereafter.
+
+**Normative ingest**: exactly **one** recover-WAL monotonic frontier after contractual **rewind**; **Wal-vs-base overlap** gated by **`bitmap`** (**§I P5** — operationalized **`v3-recovery-algorithm-consensus.md` §7 routing table**, **`checkMonotonic`**); substrate **Wal-vs-Wal LWW** after ingest order holds.
+
+```text
+type RecoverRcvrSession = record
+    open                : bool
+    fromLSN_exclusive   : uint64
+    expect_next_LSN     : uint64   // rewound expectation baseline
+    monotonic_armed     : bool     // after first lawful recover-WAL ingest
+end
+
+procedure OpenRecoverRcvr(s: RecoverRcvrSession*, fromLSN, lineage_blob):
+    require not s.open
+    s.open := true
+    s.fromLSN_exclusive := fromLSN
+
+    // INFORMATIVE (CHK-RECOVER-REWIND-ONCE): first post-open WAL expects fromLSN+1 on dense products
+    s.expect_next_LSN := fromLSN + 1
+    s.monotonic_armed := false
+    BITMAP_scope_for_session(lineage_blob)
+
+procedure OnRecoverWalTuple(s: RecoverRcvrSession*, frame_kind /* Backlog | SessionLive | … */, lsn, lba, data):
+    require s.open
+
+    if not s.monotonic_armed:
+        REWIND_VALIDATE(lsn, s.expect_next_LSN, s.fromLSN_exclusive)
+        // after success, ingest at lsn establishes monotonic stream
+        s.monotonic_armed := true
+    else:
+        FAIL_IF_NOT checkMonotonic(lsn, s.expect_next_LSN)   // gaps / backwards / unlawful dup vs policy
+
+    ApplyWalWithWalClaimBitmap(s, lsn, lba, data)
+
+    s.expect_next_LSN := AdvanceDenseOrProductRule(lsn)
+
+
+procedure OnRecoverBaseBlock(s: RecoverRcvrSession*, lba, bytes):
+    require s.open
+    ApplyBaseUnderBitmapGate(s, lba, bytes)                  // overlaps with Wal claims (**P5**); does NOT bypass Wal LSN frontier
+
+
+procedure CloseRecoverRcvr(s: RecoverRcvrSession*):
+    s.open := false
+```
+
+```text
+// Receiver-hard invariant (consensus §6.9): all recover WAL frames obey ONE global LSN order to this session —
+// bearer “kind” reshapes encoding only — never splits into independent tapes.
+```
+
+**`bitmap` arbitration + races** — **`INV‑RECV‑BITMAP‑CORE`** / **`INV‑RECV‑WAL‑NAIVE`**: normative **`ApplyWAL` / `ApplyBASE`** pseudocode (**(a)–(c)**) — **`v3-recovery-algorithm-consensus.md` §6.10**. This §7.4 sketch (**`OpenRecoverRcvr` / `OnRecoverWalTuple`**) is **routing glue**; **`ApplyWalWithWalClaimBitmap`** / **`ApplyBaseUnderBitmapGate`** **MUST** implement **§6.10** lock/`CAS` discipline (**not** anti‑pattern check‑outside‑lock).
 
 ---
 
@@ -183,6 +268,9 @@ Implementations **flatten** this; the **semantic** contract is **§3–§5**, no
 | **2026-04-30** | Pointer to consensus **§6.8** implementer checklist; **§V** **`CHK-WALSHIPPER-TIMER-DRAIN`** cross-ref in **§9**. |
 | **2026-04-30** | **§2** vocabulary **`incoming` / `debt` / `send(·,·)`**; **§4.1–4.2** strategy split; tests cross-ref **§6.3**; checklist **nine** items (**§6.8(9)**). |
 | **2026-04-30** | **§1** intro + **consensus §6.3(B)** cross-ref — **`ModeBacklog` vs `ModeRealtime`** (**§13** E‑WALSHIPPER‑DUAL‑MODE); mini-plan **§11.2a** bridge |
+| **2026-04-30** | **§7** split: **7.1–7.4** — recover **session/backlog pointer**, **monotone send (`send(∅,·)` / `send(incoming,·)`)**, receiver **rewind + monotone + `bitmap`** pseudocode |
+| **2026-04-30** | **§7.4** foot — **`bitmap`/`CAS`** cross-ref **consensus §6.10** (`INV‑RECV-*`) |
+| **2026-04-27** | **§7.3** — primary sender recover emit: normative **`Drive(input)` → `v3-recovery-algorithm-consensus.md` §6.3** (removed duplicate **`ShipOpportunity_RecoverMerged`** skeleton); **§7.4** note → consensus **§6.10** **`ApplyWAL`/`ApplyBASE`** pseudocode |
 
 ---
 
@@ -190,8 +278,8 @@ Implementations **flatten** this; the **semantic** contract is **§3–§5**, no
 
 | Doc | Role |
 |-----|------|
-| **`v3-recovery-algorithm-consensus.md` §6 + §6.8** | **Axioms + stability + implementer MUST checklist** |
-| **This** | **Algorithm steps + invariants for one implementation** |
+| **`v3-recovery-algorithm-consensus.md` §6, §6.3 **`Drive`**, §6.8–§6.9, §II §7** | **Axioms** + **`Drive`/`Apply*`** pseudocode (**`INV‑WIRE‑*`**, **`INV‑RECV‑*`**) + **implementer checklist** + **`targetLSN`** process + **replica routing / `checkMonotonic`** |
+| **This** | **Algorithm + §7 pseudocode** (**Primary shipper** + **recover receive sketch**) |
 | **`v3-recovery-wal-shipper-mini-plan.md`** | **Phased PR / file anchoring (**`seaweed_block`**) **↔** §INV tests** |
 | `v3-recovery-wiring-plan.md` | Bearer / port |
 | `v3-recovery-unified-wal-stream-*.md` | Historical kickoff — **align or supersede** with this spec |