Definition. Finite trace-selection experiment [ftip-00P8]
AGENTDRAFTED
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.