Counterexample Return Index: Routing Prover Compute with Validation-Measured Witness Utility

An executable counterexample can expose the assignment, violated literal, and dependency that break a conjecture, but extracting and minimizing that witness consumes compute that could instead train the prover or extend proof search. We introduce WitnessBudget, which turns locally corrupted conjectures into checker-confirmed, attributed repair traces, and the Counterexample Return Index (CRI), which predicts their family-level return from validation-only witness yield, probe utility, timeout, cost, and compactness. In eight family-disjoint reruns of a joint three-ecosystem training protocol, all packages start from the same Llama-3.1-70B checkpoint and receive a 512 A100-hour reservation. WitnessBudget reaches 41.7$\pm$0.8 on miniF2F, 34.1$\pm$0.9 on a ProofNet-derived Isabelle/HOL evaluation, and 56.8$\pm$0.6 on DafnyBench, improving over bare counterexample augmentation and witness-free active selection by 1.5–3.1 percentage points with positive paired intervals throughout. Masking the witness narrows the advantage by 0.7–1.3 points, and permutation degrades further, localizing the gain to theorem-aligned witness content. Across 43 unique test families and 344 family–rerun cells, frozen CRI predictions rank solve-rate gain with Spearman 0.77 [0.72,0.81] and identify positive end-to-end efficiency with AUROC 0.88 [0.84,0.91]. Acting on those predictions reallocates 27.2 falsifier hours to search, raises solve rate by 0.6–1.0 points, and improves end-to-end throughput by 1.6–2.2%, while random, difficulty-only, and yield-only gates trail the joint index.