docs(vrs): written claims in the contract, and an honestly scoped cross-check

OHS-T04/OHS-R07 no longer overclaim: the probe narrows the ungraceful
window only for provably dead sessions (pidfile present, process gone),
pty kill's pidfile removal is named, and the relaunch-time written claim
is what supersedes what the probe cannot prove. The ownership bullet
carries the written-claim semantics.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Author: schickling

docs/vrs/05-harness-state/requirements.md

@@ -57,9 +57,13 @@ path reads this record.
   truthful about dwell time. `transitions` and `sinceMs` keep a later history
   additive.
 - **OHS-T04 Ungraceful-death windows:** SIGKILL cannot be caught, so an
-  external forced kill — and nothing else — can leave a live-state record
-  whose writer is gone. Same-host readers close that window with the liveness
-  cross-check (OHS-R07); cross-host readers wait out the staleness horizon.
+  external forced kill can leave a live-state record whose writer is gone.
+  Same-host readers narrow that window with the liveness cross-check
+  (OHS-R07) where the session is PROVABLY dead — pidfile present, process
+  gone — while `pty kill` removes the pidfile and leaves the probe
+  indeterminate for the rest of the window; the next session's written
+  ownership claim supersedes the orphan at relaunch, and cross-host readers
+  wait out the staleness horizon.
 
 ## Requirements
 
@@ -115,10 +119,13 @@ path reads this record.
   and a terminal record is never re-stamped.
 - **OHS-R07 Liveness cross-check:** The record names the pty session whose
   liveness vouches for its live states. A same-host reader that positively
-  proves that session dead reads the record as `unknown` even while fresh; an
-  indeterminate probe (unreadable registry) downgrades nothing — unprovable
-  evidence is never reported as death. A fresh `ended` survives the check: a
-  terminal record is supposed to outlive its writer.
+  proves that session dead — its pidfile present, its process gone — reads
+  the record as `unknown` even while fresh; an indeterminate probe (an
+  unreadable registry, or a pidfile `pty kill` already removed) downgrades
+  nothing — unprovable evidence is never reported as death. The check is a
+  narrowing, not a closure: what it cannot prove, the relaunch-time written
+  claim supersedes and the staleness horizon bounds. A fresh `ended`
+  survives the check: a terminal record is supposed to outlive its writer.
 - **OHS-R08 All-harness coverage:** Codex, Claude, pi, and OpenCode each ship
   a producer. pi's is evented through the injected extension (the positive
   idle signal root `DQ2` asks for). OpenCode reaches driver parity first —

docs/vrs/05-harness-state/spec.md

@@ -74,17 +74,25 @@ Field rules, matching `src/harness_state.rs`:
   `human` (`none` otherwise; unrecognized words decode indeterminate) — the
   axis consumers filter on, so nothing branches on diagnostic `reason`.
 - `incarnation` is the writing session's token and `seq` its monotonic
-  ownership sequence: ownership — coalescing, heartbeat eligibility, terminal
-  suppression — is token equality, and only a session claim advances the
-  sequence (to the on-disk value plus one), which gives ownership a
-  direction: a straggler from a superseded session is refused in live and
-  terminal paths alike. Sibling writer processes of one session share the
-  claimer's exported token and sequence; records from writers predating
-  either field decode with an empty token and sequence zero, which no
-  session owns and any claim supersedes. Every landed write carries a
-  strictly monotonic per-record stamp (never inherited from beyond the
-  future-skew trust bound) so it stays byte-distinct even against a
-  same-millisecond predecessor.
+  ownership sequence. A claim is a WRITTEN act under the record lock: the
+  session starting up writes an exitless `ended (superseded)` takeover
+  record carrying its token and the on-disk sequence plus one — racing
+  claimers therefore mint distinct sequences, and a predecessor's
+  still-fresh live record is superseded at relaunch, where the
+  pty-name-based probe cannot tell sessions apart; the seat reads
+  `ended (superseded)` until the session's first real observation. Ownership
+  — coalescing, heartbeat eligibility, terminal suppression (which applies
+  only to exit-bearing terminal records, never the claim placeholder) — is
+  token equality with the claim's direction: a straggler whose claim is
+  below the on-disk sequence is refused in live and terminal paths alike,
+  and a token-only writer never claims — it adopts its own session's
+  records, starts virgin ones, and is refused against foreign tokens.
+  Sibling writer processes of one session share the claimer's exported
+  token and sequence; records predating either field decode with an empty
+  token and sequence zero, which no session owns and any claim supersedes.
+  Every landed write carries a strictly monotonic per-record stamp (never
+  inherited from beyond the future-skew trust bound) so it stays
+  byte-distinct even against a same-millisecond predecessor.
 - `reason` is diagnostic only; no consumer branches on it.
 - `sinceMs` is when the current state was entered and survives heartbeat
   re-stamps; `writtenAtMs` is the heartbeat. `transitions` is a monotonic