backlog(B-0710..B-0712): file Soraya rounds 43+44+45 hand-offs

docs/BACKLOG.md

@@ -670,6 +670,9 @@ are closed (status: closed in frontmatter)._
 - [x] **[B-0707](backlog/P2/B-0707-manifesto-citation-time-series-tracking-2026-05-23.md)** Manifesto citation time-series tracking — persistent snapshots + delta-over-time
 - [x] **[B-0708](backlog/P2/B-0708-stale-pointer-cleanup-from-razor-cadence-pass-2026-05-23.md)** Stale-pointer cleanup across `.claude/rules/` — 87 candidates surfaced by razor-cadence pass 2026-05-23
 - [ ] **[B-0709](backlog/P2/B-0709-soraya-registry-coverage-drift-register-11-unregistered-specs-2026-05-23.md)** Soraya round-42 hand-off — register 11 unregistered formal-verification specs in verification-registry.md (Class 0 drift)
+- [ ] **[B-0710](backlog/P2/B-0710-soraya-round43-dbsp-chain-rule-bp16-cross-check-fscheck-z3-2026-05-23.md)** Soraya round-43 hand-off — DBSP chain rule BP-16 cross-check (FsCheck cross-trace + Z3 pointwise lemma)
+- [ ] **[B-0711](backlog/P2/B-0711-soraya-round44-residuated-fscheck-property-file-2026-05-23.md)** Soraya round-44 hand-off — Residuated FsCheck property file (Galois + residual + retraction equivalence)
+- [ ] **[B-0712](backlog/P2/B-0712-soraya-round45-witnessdurable-commit-protocol-tla-z3-fscheck-triple-2026-05-23.md)** Soraya round-45 hand-off — WitnessDurable commit protocol (TLA+ spec + Z3 quorum-arithmetic lemma + FsCheck cross-check)
 
 ## P3 — convenience / deferred
 

docs/backlog/P2/B-0710-soraya-round43-dbsp-chain-rule-bp16-cross-check-fscheck-z3-2026-05-23.md

@@ -0,0 +1,68 @@
+---
+id: B-0710
+priority: P2
+status: open
+title: "Soraya round-43 hand-off — DBSP chain rule BP-16 cross-check (FsCheck cross-trace + Z3 pointwise lemma)"
+created: 2026-05-23
+last_updated: 2026-05-23
+classification: buildable-now
+decomposition: atomic
+assignee: kenji
+discovered_by: soraya
+owners: [kenji, formal-verification-expert]
+type: cross-check-gap
+composes_with:
+  - tools/lean4/Lean4/DbspChainRule.lean
+  - docs/research/verification-registry.md
+  - tests/Tests.FSharp/Formal/Z3.Laws.Tests.fs
+---
+
+# B-0710 — DBSP chain rule BP-16 cross-check (round-43 hand-off)
+
+## Origin
+
+Soraya's second autonomous routing tick (2026-05-23 — round 43). Highest-leverage publication-readiness gap on the DBSP chain rule artifact per Aaron's DBSP-publication arc.
+
+## Finding
+
+`tools/lean4/Lean4/DbspChainRule.lean` has **ZERO BP-16 cross-checks**. Currently A-with-CI-green-since-2026-05-17 but single-tool (Lean only). Per BP-16, P0 invariants require ≥2 cross-checks.
+
+**Empirical**:
+
+- 17 theorems/lemmas in Lean artifact
+- 0 hits for `chain_rule_proposition` / `Qdelta` / `Dop_LTI` in `tests/Tests.FSharp/Formal/Z3.Laws.Tests.fs`
+- 0 hits across all 19 TLA+ specs in `tools/tla/specs/`
+
+**Historical anchor**: April 2026 Class 1 drift catch (`chain_rule` mis-named a Theorem-3.3 corollary as Proposition 3.2) is exhibit-A that single-tool review missed the failure mode the first time. Cross-check would have caught it independently.
+
+## Routing decision (Soraya)
+
+- Cross-check 2: **FsCheck cross-trace** on `Qdelta(Q1 ∘ Q2)(s) = Qdelta Q1 (Qdelta Q2 s)` at bounded depth. Effort: S.
+- Cross-check 3: **Z3 pointwise lemma** on `D ∘ I = id` + `Dop_LTI_commute` arithmetic step (QF_LRA). Effort: S.
+
+## TLA+-hammer guard
+
+TLA+ was tempting. **REJECTED**: chain rule is a pointwise algebraic identity over operators, NOT a state-machine safety invariant. TLC would enumerate the product state space of two iterations and time out before catching the definitional-drift class. FsCheck + Z3 close the actual axes (real-code behaviour + arithmetic identity); TLA+ closes a different axis (interleaving) that nothing in the chain-rule statement depends on.
+
+## Acceptance criteria
+
+1. New FsCheck file `tests/Tests.FSharp/Formal/DbspChainRule.Properties.fs` (or extend existing Z3.Laws.Tests.fs) with property covering `chain_rule_proposition_3_2` and `Dop_LTI_commute` at bounded depth
+2. Z3 lemma covering `D ∘ I = id` + `Dop_LTI_commute` arithmetic step (QF_LRA encoding)
+3. Both cross-checks wired into CI (existing dotnet test gate is sufficient for FsCheck; Z3 may need explicit invocation)
+4. `verification-registry.md` rows for `chain_rule_proposition_3_2` + `Dop_LTI_commute` updated to reflect 3-tool cross-check status
+
+## Publication-readiness alignment
+
+Per Soraya: "Single-tool evidence does not survive Budiu-grade peer review; converting from 'A-with-CI, single-tool' to 'A-with-CI, three-tool BP-16 compliant' is the line publication crosses." **This is the gap that gets the chain-rule artifact past the publication line** (after PR #4772 closed gaps #1+#2 — README + CI badge).
+
+## Effort
+
+S + S = total S+ (one evening per cross-check). Assignee: kenji.
+
+## Composes with
+
+- [`tools/lean4/Lean4/DbspChainRule.lean`](../../../tools/lean4/Lean4/DbspChainRule.lean) — the artifact needing cross-checks
+- [`tools/lean4/README.md`](../../../tools/lean4/README.md) — landed via PR #4772; documents the artifact for reviewers
+- [`docs/research/verification-registry.md`](../../research/verification-registry.md) — registry rows for `chain_rule_proposition_3_2` + `Dop_LTI_commute`
+- [`docs/research/chain-rule-proof-log.md`](../../research/chain-rule-proof-log.md) — round-35 paper-drift audit substrate
+- `memory/persona/soraya/NOTEBOOK.md` — Round 43 entry (pending NOTEBOOK update; locate by `## Round 43` heading once landed; pruned-preserved)

docs/backlog/P2/B-0711-soraya-round44-residuated-fscheck-property-file-2026-05-23.md

@@ -0,0 +1,72 @@
+---
+id: B-0711
+priority: P2
+status: open
+title: "Soraya round-44 hand-off — Residuated FsCheck property file (Galois + residual + retraction equivalence)"
+created: 2026-05-23
+last_updated: 2026-05-23
+classification: buildable-now
+decomposition: atomic
+assignee: kenji
+discovered_by: soraya
+owners: [kenji, formal-verification-expert]
+type: cross-check-gap
+composes_with:
+  - src/Core/Residuated.fs
+  - tests/Tests.FSharp/Crdt/PNCounter.Tests.fs
+  - docs/research/proof-tool-coverage.md
+---
+
+# B-0711 — Residuated FsCheck property file (round-44 hand-off)
+
+## Origin
+
+Soraya's third autonomous routing tick (2026-05-23 — round 44). Compound option (c+d): cross-check gap + publication-readiness on a genuine framework novelty.
+
+## Finding
+
+`src/Core/Residuated.fs` (129 LoC, `ResidualMax` IVM operator for O(log k) retraction of non-invertible aggregates like `max`) has **ZERO FsCheck properties**.
+
+**Sanity-checked across CRDT/sketch family**: PNCounter, OrSet, Lww, GCounter, DeltaCrdt, Bloom, CountMin, Haar, HyperLogLog, HyperMinHash all have FsCheck tests. **Residuated.fs is the ONLY CRDT-class file with zero FsCheck coverage**.
+
+Gap named in `docs/research/proof-tool-coverage.md` §5 since 2026-04-17; 30+ rounds open.
+
+## Routing decision (Soraya)
+
+Algebraic-law identity → **FsCheck primary** (mirrors `tests/Tests.FSharp/Crdt/PNCounter.Tests.fs` template). Three properties:
+
+1. **Galois connection**: `a·x ≤ b ⇔ x ≤ a\b`
+2. **Residual under max**: `a\b = b if a≤b else a`
+3. **Retraction equivalence**: `ResidualMax(insert+retract trace) = max(positive-only trace)`
+
+## Regression-guard urgency
+
+Round-17 history: `Residuated.fs` previously advertised "O(1) amortised" retraction that was actually O(n) under adversarial retract-top. Harsh-critic caught it. Current `SortedSet` revision is the fix.
+
+**Without a property test pinning the law, a future "perf optimization" can silently re-introduce the same correctness gap.** FsCheck IS the regression guard the round-17 incident asked for.
+
+## TLA+-hammer guard
+
+TLA+ was tempting (file carries internal state `SortedSet<'K>`). **REJECTED**: state is single-thread BST holding domain values; concurrency is at the circuit-runtime layer (covered by other specs). Property IS pointwise algebraic identity — FsCheck-shape, NOT TLC-shape. TLC would enumerate BST state space and time out.
+
+## Acceptance criteria
+
+1. New file `tests/Tests.FSharp/Algebra/Residuated.Tests.fs` mirroring `PNCounter.Tests.fs` shape
+2. Three FsCheck properties covering Galois + residual + retraction equivalence
+3. Tests wired into existing dotnet test gate — `tests/Tests.FSharp/Tests.FSharp.fsproj` uses explicit `<Compile Include="..." />` registration (96 entries; not glob-based), so the new file MUST be added to the `.fsproj` in the correct compile order alongside the other Crdt/Algebra entries; `dotnet test Zeta.sln -c Release` picks it up once registered
+4. `proof-tool-coverage.md` §5 updated to mark Residuated FsCheck-covered
+
+## Publication-readiness alignment
+
+Per Soraya: "Residuated-lattice IVM is one of the framework's genuine novelties — citable if backed by a machine-checked property; currently ships with prose-only justification." SECOND publication-readiness gap alongside round-43 chain-rule.
+
+## Effort
+
+S (one evening). Assignee: kenji.
+
+## Composes with
+
+- [`src/Core/Residuated.fs`](../../../src/Core/Residuated.fs) — target needing FsCheck
+- [`tests/Tests.FSharp/Crdt/PNCounter.Tests.fs`](../../../tests/Tests.FSharp/Crdt/PNCounter.Tests.fs) — template
+- [`docs/research/proof-tool-coverage.md`](../../research/proof-tool-coverage.md) §5 — gap named since 2026-04-17
+- `memory/persona/soraya/NOTEBOOK.md` — Round 44 entry (pending NOTEBOOK update; locate by `## Round 44` heading once landed; pruned-preserved)

docs/backlog/P2/B-0712-soraya-round45-witnessdurable-commit-protocol-tla-z3-fscheck-triple-2026-05-23.md

@@ -0,0 +1,76 @@
+---
+id: B-0712
+priority: P2
+status: open
+title: "Soraya round-45 hand-off — WitnessDurable commit protocol (TLA+ spec + Z3 quorum-arithmetic lemma + FsCheck cross-check)"
+created: 2026-05-23
+last_updated: 2026-05-23
+classification: buildable-now
+decomposition: atomic
+assignee: kenji
+discovered_by: soraya
+owners: [kenji, formal-verification-expert]
+type: missing-routing-decision
+composes_with:
+  - src/Core/Durability.fs
+  - docs/research/proof-tool-coverage.md
+  - tools/tla/specs/TwoPCSink.tla
+---
+
+# B-0712 — WitnessDurable commit protocol formal verification triple (round-45 hand-off)
+
+## Origin
+
+Soraya's fourth autonomous routing tick (2026-05-23 — round 45). Option (b) missing routing decision: a property class with NO tool wired in ANY surface.
+
+## Finding
+
+`src/Core/Durability.fs:14-22` carries a **self-declared formal-verification prereq**:
+
+> "`WitnessDurable` variant is a research target — the protocol has not been specified yet and there is no in-tree paper draft. It's defined here as a skeleton so callers can type against it. The implementing `WitnessDurableBackingStore` below throws on `Save` until the paper's protocol is fully implemented and TLA+-verified."
+
+**The type itself is the gate.** Substrate-verified: zero `.tla` files match `Witness*` / `Wdc*` / `Durab*` across all 19 specs in `tools/tla/specs/`.
+
+Gap named in `docs/research/proof-tool-coverage.md` §2 line 100 since 2026-04-17 (~5 weeks ago); untouched.
+
+## Routing decision (Soraya — P0 triple per BP-16 cross-check triage)
+
+Two property classes mixed; split obligations across tools:
+
+1. **(a) State-machine safety + concurrency race**: "Every acked `Save` survives witness-quorum failures under interleavings."
+   - **Primary tool**: TLA+/TLC
+   - **Scale**: 3 witnesses × 2 writers × 4 keys (mirrors `SpineAsyncProtocol`)
+   - **Effort**: M
+2. **(b) Quorum-intersection arithmetic**: `N ≥ 2F+1`.
+   - **Primary tool**: Z3 (QF_LIA)
+   - **Effort**: S
+3. **Cross-check (third leg)**: FsCheck firing the real F# `WitnessDurableBackingStore` under simulated witness failures, asserting the TLA+ invariant on the executing code path.
+   - **Effort**: S
+
+## TLA+-hammer guard
+
+TLA+ IS the right primary for (a). The guard fires the **INVERSE** direction: do NOT bundle (b)'s quorum arithmetic into the spec. TLC would enumerate the arithmetic state-space; Z3 closes it in seconds. **Split the obligations.**
+
+## Acceptance criteria
+
+1. New file `tools/tla/specs/WitnessDurable.tla` covering state-machine safety + concurrency interleaving (3w × 2w × 4k)
+2. New Z3 lemma (either standalone or extension to existing Z3 test surface) proving quorum-intersection arithmetic `N ≥ 2F+1`
+3. New FsCheck file `tests/Tests.FSharp/Storage/WitnessDurable.Properties.fs` (sibling of existing `tests/Tests.FSharp/Storage/Durability.Tests.fs` — no `Durability/` directory in current test layout) exercising the real `WitnessDurableBackingStore` under simulated witness failures; register via explicit `<Compile Include="..." />` in `tests/Tests.FSharp/Tests.FSharp.fsproj`
+4. All 3 cross-checks land green in CI BEFORE the source-side `throw` gate in `Durability.fs:WitnessDurableBackingStore.Save` is removed
+5. `verification-registry.md` row added for `WitnessDurable` with all 3 cross-check references
+
+## Structural cousin (reviewer reference)
+
+`tools/tla/specs/TwoPCSink.tla` — same pattern (commit protocol + quorum + interleaving). Reviewers will read both.
+
+## Effort
+
+M + S + S (total ~M+). Assignee: kenji.
+
+## Composes with
+
+- [`src/Core/Durability.fs`](../../../src/Core/Durability.fs):14-22 — self-declared TLA+ prereq
+- [`docs/research/proof-tool-coverage.md`](../../research/proof-tool-coverage.md) §2 line 100 — gap named 2026-04-17
+- [`tools/tla/specs/TwoPCSink.tla`](../../../tools/tla/specs/TwoPCSink.tla) — structural cousin
+- `memory/persona/soraya/NOTEBOOK.md` — Round 45 entry (pending NOTEBOOK update; locate by `## Round 45` heading once landed; pruned-preserved)
+- B-0710 + B-0711 (sibling Soraya hand-offs from same session)