docs(events): record what the final matrix actually says about four guards

Final matrix: 34 mutations, 22 detected, baseline restored green. Every
survivor is now documented at its line with why it survives, and two of them
turned out to be instrument defects rather than coverage gaps.

lastProbeOK's INSTALL STAMP IS REDUNDANT and the comment claimed otherwise. It
said a zero value "would permanently disqualify a subscription from ever being
cycled" -- true of the age-based premise it was written for, false under the
ordering rule that replaced it, because a zero value fails
`lastProbeOK.After(lastSeen)` exactly as an install stamp equal to lastSeen
does. Kept, for a reason it earns: it makes the field's invariant true by
construction, so a future rule reasoning about this value's AGE gets a real
timestamp rather than 1970 -- which is the trap the age-based rule fell into
one field over.

THE TWO cycleOne ABANDON GUARDS DIE ONLY TOGETHER AND ARE NOT REDUNDANT, which
took checking rather than assuming. They catch different shapes of the same
recovery: an arrival that has not been re-probed pushes lastSeen past
lastProbeOK so the premise case fires and the freshness case is unreachable --
that is the shape the test produces, and it is why removing either alone stays
green. But the publisher runs on its own goroutine at its own cadence and can
land a successful probe between the arrival and the decision, putting
lastProbeOK ahead again; there only the freshness case stops a healthy
subscription being torn down. Deleting it on the strength of the matrix would
remove the second shape's only guard.

Close's off-the-lock PubSub.Close is UNTESTED BY DESIGN, recorded rather than
papered over. It is a contention property, and the only assertion that
separates it is a timing one, which in this suite is a flaky one.

TWO HARNESS DEFECTS, both of which produced false survivors that would have
gone into the evidence package as findings. M11a inserted its mutation AFTER
the gate it was meant to disable -- unique anchor, wrong placement, so the
early return still fired and nothing changed; with a correct anchor it is
detected. M20 left variables unused and came back BUILD-BREAK rather than
answering; in compiling form it genuinely survives, consistent with
establishSubscription's abandon path already covering it.

The lesson worth keeping: when I rewrote all 34 anchors against current source
I verified each matched exactly ONCE, and uniqueness is not placement. An
anchor can be unique and still land somewhere that changes no behaviour.

Claude-Session: https://claude.ai/code/session_01JVDBKbgn3Xt7ndW1YoYd8X

internal/events/redis_bus.go

@@ -725,9 +725,22 @@ type redisSub struct {
 	// this field the detector reads its own inability to probe as evidence
 	// that the peer is dead, and tears down a healthy connection on a schedule.
 	//
-	// Stamped at install for the same reason lastSeen is: a zero value would
-	// permanently disqualify a subscription from ever being cycled, which
-	// fails in the opposite and quieter direction.
+	// Stamped at install, and the mutation matrix says that stamp is REDUNDANT
+	// under the ordering rule — recorded rather than left as an unearned
+	// justification. An earlier version of this comment claimed a zero value
+	// would "permanently disqualify a subscription from ever being cycled".
+	// That was true of the age-based premise it was written for; it is not true
+	// now. The rule is `lastProbeOK.After(lastSeen)`, and a zero value fails
+	// that test exactly as an install stamp equal to lastSeen does — in both
+	// cases the subscription is simply not cycled until its first successful
+	// probe, which is the intended behaviour either way. Removing the stamp
+	// changes no outcome and no test.
+	//
+	// It is kept because it makes the field's invariant true by construction —
+	// an installed subscription always carries a real timestamp, so any future
+	// rule that reasons about this value's AGE rather than its order gets a
+	// sane one instead of 1970. That is the same trap the age-based rule fell
+	// into, one field over.
 	lastProbeOK time.Time
 
 	// confirmed is closed by receiveMessages when Redis acknowledges the
@@ -1397,6 +1410,14 @@ func (b *RedisBus) Close() {
 	// Subscribe contends for — with subscriber channels still open behind it.
 	// Round 12 fixed the cycle path and left this one, which is the same defect
 	// on the path that runs once per process.
+	//
+	// UNTESTED, DELIBERATELY. Moving a close off a lock is a CONTENTION
+	// property: the only assertion that distinguishes it is a timing one — how
+	// long some other goroutine waited for b.mu — and a timing assertion in
+	// this suite is a flaky assertion. The mutation matrix says so plainly
+	// (closing under the lock survives every test), and that survival is
+	// recorded here rather than papered over with a test that would pass
+	// either way.
 	closing := make([]*redis.PubSub, 0, len(b.wsSubs))
 	for wsID, sub := range b.wsSubs {
 		sub.cancel()

internal/events/redis_heartbeat.go

@@ -702,6 +702,23 @@ func (b *RedisBus) cycleOne(c idleCycle, idleTimeout time.Duration) {
 	case b.now().Sub(sub.lastSeen) < idleTimeout:
 		// It recovered while this cycle sat in the queue. Nothing to end and
 		// nothing to replace: leaving it alone is the whole point.
+		//
+		// THIS AND THE PREMISE CASE ABOVE DIE ONLY TOGETHER in the matrix, and
+		// they are NOT redundant — they catch different shapes of the same
+		// recovery, which is why removing either alone leaves the recovery test
+		// green:
+		//
+		//   - Recovered and NOT re-probed since: the arrival pushed lastSeen
+		//     past lastProbeOK, so the premise case fires and this one is never
+		//     reached. That is the common shape and the one the test produces.
+		//   - Recovered AND re-probed since: the publisher runs on its own
+		//     goroutine at its own cadence, so it can land a successful probe
+		//     between the arrival and this decision. lastProbeOK is then ahead
+		//     of lastSeen again, the premise case passes, and only this one
+		//     stops a healthy subscription being torn down.
+		//
+		// Deleting this because "the matrix says it survives" would remove the
+		// second shape's only guard.
 		b.retirePendingLocked(c.workspaceID, c.pending)
 		b.mu.Unlock()
 		close(c.pending.done)