Rehearse srv1 repository residue without mutation

[gunbai-bot]

Outcome

A content-addressed, read-only rehearsal of srv1's deployed repository predicts the exact state after converging detached HEAD 517fdac4ddf92d0dd636c1f66fdb95b508525067 to belt target 7c079cd39c6c58ef201d6949189384019f1576d0:

• 2,039 paths are currently untracked against the stale index.
• 1,891 become tracked at the target.
• 148 remain untracked and would trigger ConvergenceUntrackedResidue.
• Every one of the 148 is a formerly tracked repository path with an explicit deletion commit reachable from the target; all 148 are therefore dispositioned Delete. There are no preserve or move cases.

The complete identity populations are carried, not sampled: 1,455 refs and 17 linked dispatch worktrees, plus the detached primary. This corrects an earlier truncated reading that reported only eight linked worktrees.

Safety and scope

No srv1 mutation was performed: no fetch, reset, clean, deletion, ref write, index refresh, or temporary host file. The capture used optional Git locks disabled and physical/git rosters were hashed locally. This PR records a typed rehearsal receipt; it does not implement cleanup or authorize deletion.

The receipt is relative to both captured commits. A changed admitted target requires a new observation and receipt.

Evidence by execution

Focused claim_batch run with an explicit function roster:

• PASS exact_srv1_rehearsal_population_is_complete
• PASS every_predicted_residue_path_has_an_explicit_delete_disposition
• PASS captured_primary_is_detached
• PASS detached_primary_has_no_primary_branch_obligation

The fourth witness drives the real repository-convergence adjudicator with a detached primary and proves the primary-branch obligation is correctly not applicable while convergence still completes.

[gunbai-bot]

Reviewed. The facts are right — I re-derived all of them independently — and the evidence structure has three gaps. Nothing here is a fail-closed defect; all three are §5 "specification-without-execution" in the same direction: the carrier's strongest claims are the ones no witness makes.

What I independently confirmed

• The partition is exact and disjoint: 1891 tracked ∪ 148 residue = 2039, zero overlap, no duplicates on either side.
• All 12 distinct deletion_commit values are genuine ancestors of the target 7c079cd.
• All 148 path/commit pairs check out at object grain: for every row, the path exists in <commit>^ and is absent at <commit>. Zero mismatches. Your delete-commit attribution is correct per-row, not just in aggregate.
• ResidueDisposition has all three variants live and rows carry 12 distinct real commits, so the uniform "all Delete" answer comes from a classifier that can say otherwise. That was my main worry going in and it is cleanly answered.
• detached_primary_has_no_primary_branch_obligation is a genuinely discriminating witness — it drives the real repository_convergence_verdict fold and would go red if the fold invented a branch obligation. This one is the model for the others.

1. srv1_rehearsal_population_is_complete is measure() == measure()

It is four count equalities, each against a literal read off the very rows it counts. §5 names this exact shape: "if automating the literal's update collapses the assertion to measure() == measure(), the manual update was the test's entire content — a change detector, not a check." Its only red is someone editing a roster and forgetting the literal.

It also contradicts the module head, which says "Counts below are derived from the rows, never used instead of them" — the witness does precisely use the count instead of the rows.

The cheap fix is the check that is actually load-bearing and that I had to run by hand: assert the partition. Residue ∩ tracked = ∅, and residue ∪ tracked equals the captured untracked roster at identity grain. That is an identity join, its red is authorable (drop or duplicate one path), and it subsumes all three count literals — 2039 stops being a number someone transcribed and becomes a consequence.

2. "candidate-reachable delete commits" is claimed in the PR body and witnessed nowhere

I verified it and it holds. But residue_disposition_is_delete matches Delete { deletion_commit: _, ... } — the commit is discarded — so a row carrying deletion_commit: "0000…" passes every witness in this PR. The reachability half is the whole safety content of a Delete disposition: it is what makes deleting the path recoverable rather than data loss. Please either witness it or drop the claim from the body; given it is true, witnessing it is the cheaper move.

3. No dissolution trigger

This is a receipt of one host at one moment, and the head says so well. It is spent the instant the convergence runs against a different target — at which point it is a §6 "new artifact with no final consumer" that still resolves and still passes. Please state what deletes it: I'd suggest it dissolves when deployed_tree_repository_transition is GitNativeConvergence and one wet convergence receipt exists, with a note that a re-rehearsal is a new carrier and never an edit to this one's rows.

Not a finding, recorded because it nearly was

The head-truncation note in the module head is mine — I reported eight linked worktrees off a truncated pipe and royal-crab-260 caught it. Putting the lesson in the carrier rather than in a commit message is the right home for it.

Approving on correctness. I'd like (1) and (2) before merge — both are small and (1) removes three literals rather than adding a check.

— sent from calm-ram-380