Backport the internal rule names from the Verus model: every rule processes something; absorb R2 taskFulfillment into the coupled write

[dtornow]

The Verus abstract model (resonate-verus, branch claude/resonate-verus-handoff-hz96p6) restructured its internal step alphabet so that all five rules share one verb. This issue proposes backporting those names to spec/02-abstract/rules.lean. (It supersedes two earlier shapes proposed in this issue: dispatchExecute/dispatchUnblock, and then a mixed retryTimeout/processCallback set. The uniform naming below is the current proposal.)

Proposed names

Lean today	Proposed	What it processes
promiseTimeout (R1)	processPromiseTimeout	the promise deadline: settle to the verdict and fulfill the task pair — the coupled write
leaseExpiry (R5)	processLeaseTimeout	the lease deadline: reclaim the task to pending, arm the retry deadline
dispatch (R6)	processRetryTimeout	the retry deadline: emit the execute, re-arm at a chosen instant
resume (R4)	processCallback	one callback of a settled promise: wake the awaiter task — the work continues in the durable world
notify (R3)	processListener	one listener of a settled promise: emit its unblock — the work continues outside

Why one verb

Every rule processes something the state owes. Three process a deadline that has come due; two process an entry in a settled promise's fan-out ledger, one entry at a time, remove-and-act in one step. Naming them all process* makes the machine's internal life legible as a single idea — working off outstanding obligations — while the two families remain visible in what each one processes.

Every rule is named for its trigger, not its effect. What a rule emits is an effect: exactly two rules write the outbox, and neither deserves a name taken from the message. The retry deadline's only consequence is the dispatch, so the deadline and the execute are one event; and the unblock is simply what processing a listener does. Naming R6 dispatch hides that it is the third member of the timeout family, and naming R3 notify alongside R4 resume hides that those two are a symmetric pair over the two ledgers.

There is no sixth rule in scope, and this is checkable. The only things the state can owe work on are the three deadlines (timeoutAt, the lease deadline, the retry deadline) and the two ledgers (callbacks, listeners). A task's queued resumes are carried and delivered with the execute rather than processed, and outbox entries are transport's business, below the model. The genuine sixth is R7 scheduleFire, which would become processSchedule under the same rule — the naming already accommodates it.

The deferred model stays. The fan-out ledgers remain drained asynchronously, entry by entry, rather than inlined into the settling transitions. That keeps the spec the liberal contract: an implementation that pages through a large fan-out still refines it, and one that settles with the whole fan-out inline in a single atomic write (as resonate-on-s3 does) refines it trivially.

Absorb R2 taskFulfillment

Task fulfillment is not a separate transition: settling a promise fulfills its task pair in the same step (the coupled write). In the Verus model the settle write itself establishes fact T, so on reachable states R2 is redundant — its refinement obligations are discharged by one unconditional promise-timeout step per due id. Proposal: fold fact T's materialization into R1's write and drop taskFulfillment as a standalone rule (see also #9, which proposes declaring the coupling as a state invariant), leaving the internal alphabet at five rules:

processPromiseTimeout, processLeaseTimeout, processRetryTimeout, processCallback, processListener

The Verus side verifies with exactly this shape (413 proofs, 0 errors), so the backport is a rename-plus-deletion with no semantic change to the reachable behaviors.