Add eventual cleanup liveness and fix cancel quiescence gaps.

Encode zero-orphan intent as EventuallyNonWinnerStagingCleaned and
EventuallySystemQuiescent under recovery. Stop authorized attempts on
FinalizeCancel and do not re-publish cancel notices after terminal so fair
behaviors can reach SystemQuiescent (TLC-checked on Remora.cfg).

docs/protocol/Remora.cfg

@@ -42,3 +42,5 @@ PROPERTIES
     EventuallyDispatched
     EventuallyReaped
     EventuallyTerminal
+    EventuallyNonWinnerStagingCleaned
+    EventuallySystemQuiescent

docs/protocol/Remora.tla

@@ -471,18 +471,26 @@ RequestCancel(j) ==
 
 \* Cancelled forbids durable publication; it does not assert process stop.
 \* Progress remains until coord GC (ClearStaleLiveProgress / terminal clean).
+\* Authorized-never-activated attempts stop here so they do not block quiescence.
 FinalizeCancel(j) ==
     /\ phase[j] = Cancelling
     /\ phase'     = [phase EXCEPT ![j] = Cancelled]
     /\ authority' = [authority EXCEPT ![j] = NoAttempt]
+    /\ attemptState' =
+        [a \in AttemptIds |->
+            IF JobOf(a) = j /\ attemptState[a] = AttemptAuthorized
+            THEN AttemptStopped ELSE attemptState[a]]
     /\ UNCHANGED <<cancelRequested, currentToken, dispatchNeeded,
                     committedAttempt, checkpoint, checkpointValid>>
     /\ UNCHANGED coordinationVars
     /\ UNCHANGED workerVars
-    /\ UNCHANGED attemptVars
+    /\ UNCHANGED <<attemptWorker, attemptProgress, initialProgress,
+                    resumedFromCheckpoint, stageState, pendingOutcome>>
 
+\* In-flight cancel signal only; terminal jobs do not re-arm notice after clean.
 PublishCancelNotice(j) ==
     /\ cancelRequested[j]
+    /\ ~Terminal(j)
     /\ ~cancelNotice[j]
     /\ cancelNotice' = [cancelNotice EXCEPT ![j] = TRUE]
     /\ UNCHANGED durableVars
@@ -954,6 +962,9 @@ CommitIsFencedCAS        == [][CommitLinearizationStep]_vars
 \* EventuallyTerminal: some terminal outcome (Succeeded, Failed, or Cancelled).
 \* Permanent source/target failure may yield Failed after the retry budget; success
 \* is not guaranteed under unrestricted WantsFailure nondeterminism.
+\* EventuallyNonWinnerStagingCleaned / EventuallySystemQuiescent: model GC goal under
+\* fairness (infallible CleanupStage). Product seeks zero orphans under recovery;
+\* not a safety invariant and not a readiness gate (IF-7).
 WorkerAvailable(w) ==
     /\ workerState[w] = WorkerUp
     /\ \A s \in Services : CanReach(w, s)
@@ -970,4 +981,19 @@ EventuallyReaped ==
 EventuallyTerminal ==
     RecoveryAssumption => \A j \in Jobs : <>Terminal(j)
 
+CleanupEligible(a) ==
+    /\ stageState[a] \in {StagePartial, StageComplete}
+    /\ committedAttempt[JobOf(a)] # a
+    /\ ~CurrentAuthority(a)
+    /\ (attemptState[a] = AttemptStopped
+         \/ workerState[attemptWorker[a]] = WorkerDown)
+
+EventuallyNonWinnerStagingCleaned ==
+    RecoveryAssumption =>
+        \A a \in AttemptIds :
+            CleanupEligible(a) ~> stageState[a] = StageCleaned
+
+EventuallySystemQuiescent ==
+    RecoveryAssumption => <>SystemQuiescent
+
 =============================================================================