Split the retiree-roster claim from #11800 into two authorable reds, and repair the file's resolve after #11762

[gunbai-bot]

Repairs a decoration that landed on main in #11800 (efe292a), found by review 69106, and — discovered while doing so — a live main breakage in the same file. Work item node://adhoc-aa9e0221-13a, parent sunny-ant-606.

1. The decoration (review 69106)

the_real_srv1_retiree_roster_reaches_one_admitted_read in test.claim.runner.runner_host_file_converge_witness_test carried two conjuncts with no authorable red:

• retired == required_retirees_for_host(host: operator_host_srv1) — f(x) == f(x): runner_host_file_subject sets retired_units to that very call.
• a test-side disjointness fold over retired and desired — both derive from the width authority on opposite sides of it, so disjoint by derivation.

Both are deleted; no count literal is restored; no assertion whose two sides come from one production call is added (exact manifest correctness stays runner_slot_retirement_witness_test's proposition).

2. Two claims, one interface each

• the_real_srv1_retiree_roster_reaches_one_admitted_read — narrowly: length(retired) > 0, the argv literal, portable_remote_words admits it. Its red lives in the cgroup read batching / argv transport.
• every_desired_srv1_unit_is_outside_the_retirement_manifest (new sibling) — plants the whole desired roster beside the real retirees as an observed surplus and requires gunbc.runner_width_transition transition_population_agreement to answer Disagrees { unexpected } with unexpected equal to exactly the desired roster (length(desired) > 0 as a conjunct; Agrees and Undecidable are false). It proves one cross-authority exclusion relation — every identity the deploy currently desires is outside the transition obligation — not that the manifest is exact.

Why its red is authorable in production. The two sides are independent producers: desired_units comes from the deploy row's runner_count via desired_runner_slot_members; the obligation from the transition row via transition_required_retirees_at. Changing production alone — slot: target + 1 → slot: target in transition_required_retirees_at (the off-by-one that counts the top desired-live slot as a retiree, the stale-38 class) — absorbs a desired unit into the manifest, it vanishes from unexpected, and the exact-list equality fails. Planting the whole roster (not one unit) means a later non-contiguous widening that absorbed any other desired unit fails it the same way. An always-Disagrees fold fails it too, since the list must name the desired roster alone.

3. The width migration — and what it is and is not load-bearing for

gunbc.runner_slot_allocation gunbc_runner_slots_per_host was deleted by #11762 in the same window that #11800 added it as an import of this file, so for a while every claim in this file refused to resolve on main and no required lane noticed (v2.workflow.required_floor required_gate_prefixes carries no dag/test/claim/runner/ row, so the file is never resolved unless a diff touches it — DESIGN §3 "the deletion is the census — but only over the population a run compiles", caught in the wild).

That import break is already cleared on main by #11871, not by this PR. This PR is therefore not load-bearing for the floor/parse chain. What it replaces is #11871's repair itself: that one returns 0 - 1 from srv1_width() on the unresolved arm — a fabricated sentinel (DESIGN §5), and one that would start srv1_retiring_names at slot 0. Here srv1_width() is Int?; the unresolved arm yields an empty listing from the four width-derived helpers, and every consumer was audited so that cannot become an absorbing fallback: five carry a positive conjunct no unit can satisfy on an empty listing (every_unit_holds, population_holds, an effective population); the two pure-refusal claims (a_declared_live_slot_missing_from_the_host_refuses, an_unread_omitted_retiree_refuses) gained a length(...) > 0 conjunct. The TransitionPopulationUndecidable arm from #11762 closes to false.

So the PR's value rests on two things: the claim-quality repair (§1–2) and replacing the 0 - 1 sentinel with the typed arm.

Evidence

claim_batch built from this exact head into a private CARGO_TARGET_DIR:

• path /tmp/nimble-swift-273-target/release/claim_batch, sha256 9c0882411376f303a92a3a8deb984eaa15598da42f301a77a79290f91b7db7a5
• build head 20a471d8de5 (main merged through 87c6658641e; zero commits behind main at build time), worktree clean, built 2026-09-20 19:56:42–19:58:58 UTC
• three earlier takes (12:10Z cba30e3b…; 15:52Z c5cea50c… at 9f7d5893f82; 17:51Z 295d7697… at 3d52ee3487d) are superseded; every re-take reproduced the same verdicts and eval-step counts exactly.

One targeted invocation per arm, GUNBC_MEMORY_BUDGET_BYTES=16GiB, the same four claims:

claim	head	production-only mutation (slot: target + 1 → slot: target in transition_required_retirees_at, test untouched)
the_real_srv1_retiree_roster_reaches_one_admitted_read	PASS (59,457 steps)	PASS (62,183)
every_desired_srv1_unit_is_outside_the_retirement_manifest	PASS (9,785)	FAIL (9,893)
a_declared_live_slot_missing_from_the_host_refuses	PASS (20,055)	PASS (20,233)
an_unread_omitted_retiree_refuses	PASS (61,508)	PASS (61,933)

The argv claim stays green under the mutation that reds the transition claim — the two controls are independent. Mutation reverted; worktree clean after.

🤖 Generated with Claude Code

[gunbai-bot]

review 69250 addressed in 7d5d27d: the authorability annotation now names the live mutation — slot: target + 1 → slot: target in transition_required_retirees_at, over gunbc_runner_committed_width's RunnerWidthDerived { slots } arm — which is the mutation the evidence run actually performed. The remaining gunbc_runner_slots_per_host mention (the historical one) is unchanged. The commit touches only // annotation lines, so the annotation-erased program the four verdicts were taken on at 9f7d589 is byte-identical (DESIGN §4c).

— sent from nimble-swift-273