Definition. Finite trace-selection experiment [ftip-00P8]
✍️source

    The selective-refinement study compares fixed-horizon data interventions under a declared training and evaluation boundary [dang2026selecting, Sections 6-7; Tables 4-5, 10]. A trace-selection experiment is the following finite typed record.

    Fix the P0 lifecycle arm set \(\mathcal A\), its boundary map \(r:\mathcal A\to \mathcal J\), mask map \(M:\mathcal A\to \mathcal P(\{s,h,w\})\), and endowment \(E_0\) from § [ftip-00P0] and § [ftip-00OY]. Choose finite nonempty label sets

    \[ \mathfrak H\subset \mathbb N,\qquad \mathfrak L,\qquad \mathfrak B\subset \mathbb N_{>0},\qquad \mathfrak D,\qquad \mathfrak R. \]

    A split map returns a triple

    \[ \operatorname {split}:\mathfrak D\longrightarrow \{(Q_{\rm sel},Q_{\rm hold},Q_{\rm xb})\mid Q_{\rm sel},Q_{\rm hold},Q_{\rm xb}\subseteq \mathcal Q\text { are finite}\}, \]

    whose three outputs are pairwise disjoint and satisfy \(|Q_{\rm sel}|>0\), \(|Q_{\rm hold}|>0\); \(Q_{\rm xb}\) may be empty only when the experiment records that no cross-benchmark comparison is made. A randomization map \(\lambda _{\rm pair}:\mathfrak R\to \operatorname {Dist}(\mathcal G\times \mathcal G)\) supplies a joint source law for each paired comparison.

    The experiment declares a finite, nonempty arm set \(\mathfrak A\subseteq \mathcal A\times \mathfrak H\times \mathfrak L\times \mathfrak B\times \mathfrak D\times \mathfrak R\). For each \(a\in \mathfrak A\), write its projections as

    \[ (a_0(a),H_a,\ell _a,B_a,D_a,\eta _a),\qquad r_a:=r(a_0(a)),\quad M_a:=M(a_0(a)),\quad \mathcal R_a:=\lambda _{\rm pair}(\eta _a). \]

    The arm record additionally supplies one model, teacher, scaffold, verifier, task law, inference protocol, and componentwise budget. These objects are maps of \(a\), not implicit labels; paired arms must agree on every object except the factor named by their comparison. The split attached to \(D_a\) is written \((Q_{\rm sel,a},Q_{\rm hold,a},Q_{\rm xb,a})\); it also supplies a nonempty finite strategy-label set \(\mathfrak S_a\) and a receipt space \(\mathcal R_a^{\rm rec}\) containing a typed held-out outcome \(Y_a\in \mathcal Y_a\cup \{\bot \}\), a declared scalarization \(g_a:\mathcal Y_a\to \mathbb R\), and an admission field. For every paired comparison \((a,a')\), the record additionally declares the finite pairing space \(\mathcal P_{a,a'}:=(Q_{\rm hold,a}\cap Q_{\rm hold,a'}) \times \mathfrak S_a\times \mathfrak S_{a'}\) and a law \(\Lambda _{a,a'}\) on \(\mathcal G\times \mathcal G\times \mathcal P_{a,a'}\). The shared task coordinate in this law is the pairing key; the two strategy coordinates may differ.

    For each arm, let \(\mathcal X^{\rm sel}_a\) be the finite candidate-pool space with \(1\leq B_a\leq |\mathcal X^{\rm sel}_a|\), and let \(\mathcal F^{\rm sel}_a\) be the sigma-field generated by the selection-time prefix, teacher-forced score, data-only trace metadata, and \(Q_{\rm sel,a}\). The metadata map excludes held-out outcomes, verifier outcomes, and post-selection continuation events. The selector is a measurable kernel with respect to this sigma-field

    \[ \mathsf S_{a,\ell _a}:\mathcal X^{\rm sel}_a \longrightarrow \operatorname {Dist}\bigl (\{I\subseteq \mathcal X^{\rm sel}_a: |I|=B_a\}\bigr ). \]

    It therefore returns a retained index set of the declared size without access to held-out outcomes. Write \(\mathcal I_a:=\{I\subseteq \mathcal X^{\rm sel}_a:|I|=B_a\}\). A run kernel

    \[ \mathsf K^{\rm run}_{a,\ell _a}: \mathcal X^{\rm sel}_a\times \mathcal I_a\times \mathcal G \times \mathcal Q\times \mathfrak S_a \longrightarrow \operatorname {Dist}(\mathcal R_a^{\rm rec}) \]

    maps a candidate pool, its retained index set, one component of the paired source draw, a task, and its arm-specific strategy coordinate to a receipt with an event sequence, task and strategy labels, final verifier outcome, typed held-out outcome, admission field, state and artifact hashes, and the charged token, tool, storage, restart, discarded trace, and verification costs, with exactly \(H_a+1\) event slots and a timeout receipt at the final slot when needed. For a paired comparison, \(\Lambda _{a,a'}\) supplies a common held-out task and the two strategy coordinates, while \(\mathcal R_a\) supplies the two source components before the kernels are applied. Thus an arm defines maps and kernels that use the selector output to produce replayable receipts; it does not merely list factors whose later meaning is left implicit.

    The reset transition is \(\mathsf {Reset}_{r_a,M_a}\) from § [ftip-00P0]. Horizon, selector, budget, split, and randomization are therefore attached to a concrete P0 state boundary and a concrete run kernel. This is an empirical protocol definition, not a theorem or a claim that any selector improves behavior.