docs(abf26): true-up ToVCVio staging markers against the expanded VCV-io branch

All generic ToVCVio lemmas are now staged on the VCV-io branch
feat/simulateq-routing-lemmas (c8e953c2 + a1e79b1b + 01ff338f, one-shot PR
pending): the README gains the staging-state section with the
delete-at-bump instruction and the three rename-at-deletion mappings
(OptionT.failure_bind -> Batteries failure_bind, StateT.run'_map_comm ->
StateT.run'_map', bind_liftComp_map -> Mathlib bind_map_left); the
SimulateQ.lean "ArkLib-local / NOT mirrored" header is retitled accordingly.
RbrGame.lean stays ArkLib-specific (references ProtocolSpec).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Author: alexanderlhicks

ArkLib/ToVCVio/OracleComp/SimSemantics/SimulateQ.lean

@@ -453,10 +453,14 @@ lemma simulateQ_add_add_liftM_comp_right (t : spec₂.Domain) :
 
 end QueryImpl
 
-/-! ### ArkLib-local lemmas (upstream candidates; NOT mirrored in VCV-io yet)
-
-Unlike the staged section above, nothing here exists upstream: do NOT delete these
-at the next VCVio bump unless they have been upstreamed by then. -/
+/-! ### Further staged lemmas (mirrored on the VCV-io PR branch 2026-06-12)
+
+Everything below is now ALSO staged on the VCV-io branch
+`feat/simulateq-routing-lemmas` (commit `01ff338f`), in some cases generalized
+(`ProbComp` → generic monad) — see `ArkLib/ToVCVio/README.md` for the
+disposition table and the three rename-at-deletion cases. Delete here at the
+first VCVio bump past that branch's merge, after confirming the bump carries
+them. -/
 
 /-- `OptionT` companion to `QueryImpl.simulateQ_liftM_eq_of_query`: simulating an
 `OracleComp`-computation `oa` lifted into `OptionT (OracleComp spec₂')` (the shape produced by

ArkLib/ToVCVio/README.md

@@ -9,8 +9,28 @@ Workflow: prefer landing general statements upstream in VCV-io under the same
 names and the mirrored path; on the next VCVio bump, delete the corresponding
 declaration here and let references resolve to the upstream version.
 
+## Staging state (2026-06-12)
+
+Everything generic in this directory is staged on the VCV-io branch
+`feat/simulateq-routing-lemmas` (commits `c8e953c2` + `a1e79b1b` + `01ff338f`,
+PR pending). **At the first VCVio bump past that branch's merge, delete the
+mirrored declarations here** — they were verified to be same-name drop-ins
+(some upstream versions are *generalized*: `ProbComp` → generic monad,
+`StateT σ ProbComp` → lawful target; all unify at ArkLib's instantiations).
+Before deleting, confirm the bump actually carries them.
+
+Three local names resolve to pre-existing upstream lemmas instead — at
+deletion time, **rename call sites**:
+
+| ArkLib-local name | upstream replacement |
+|---|---|
+| `OptionT.failure_bind` | `failure_bind` (Batteries, `@[simp]`) |
+| `StateT.run'_map_comm` | `StateT.run'_map'` (note: arg order differs) |
+| `OracleComp.bind_liftComp_map` | `bind_map_left` (Mathlib) |
+
+**Not staged (genuinely ArkLib-specific, keep):**
+`OracleComp/RbrGame.lean` — references ArkLib's `ProtocolSpec`
+(challenge-query resolution + the rbr/KS game master mixture lemmas).
+
 History note: `simulateQ_list_forIn` was staged here and has been deleted —
-the VCVio pin (`5f7707fb`, Lean 4.30 bump) now contains it upstream. The
-`simulateQ_addLift_add_liftM_left/right` routing pair
-(`OracleComp/SimSemantics/SimulateQ.lean`) remains ArkLib-local and is an
-upstream candidate.
+the VCVio pin (`5f7707fb`, Lean 4.30 bump) now contains it upstream.