[TS PBT] Reuse bounded command models and state invariants in hybrid search #402

Closed as not planned on 2026-10-16

The project owner chose one PBT generation phase followed by USVM-only search and concrete candidate validation. The current plan is #345.

The current plan uses ordinary properties and existing bounded same-receiver wrappers where needed. A dedicated command-model sequence generator, symbolic continuation and sequence-reduction framework are outside this delivery.

This is a scope decision, not a claim that the former acceptance was implemented. The earlier description remains in issue edit history and the pre-change audit snapshot. Reopening this extension requires a separate scope decision.