Cost-Indexed Bracketing for Checkable Search

We study hard-budget search with a sound terminal checker and a supplied finite hidden-state model. Stationary rejection-only retries reduce to completion counts; an exit-preserving phase construction extends this reduction through checkpoint creation. The resulting block success vectors are standard partially observable Markov decision process (POMDP) $\alpha$-vectors, with exact cost expressed by observable budget augmentation. We show how a cost-sliced envelope approximation composes through diagnostic and refresh decisions, and implement both rounded grids and standard $\epsilon$-pruning. The latter is substantially more compact on the strongest tested bank: 255 vectors rather than 31,083 grid records. Computed lower/upper brackets, not a loose worst-case grid rate, guide refinement. A finite-row calibration procedure produces a true-environment bracket from sampled program proposals under explicit labeled-access assumptions. Experiments include measured 10,000-prior workloads, support-size resource failures, and 64 random graph catalogs. Post-refresh diagnosis helps modestly in unchecked catalogs but remains of little benefit when refresh already checks the checkpoint; greedy residual filling explains most fixed-bank allocation gains. The contribution is an exit-preserving search specialization of established POMDP approximation tools, with an explicit model-acquisition boundary, not a new value representation or a general claim about language-model reasoning.