Fixed-budget trace-selection protocol [ftip-00P3]
✍️source

    The trace-selection intervention is a finite evaluation proposal. It compares horizon and selector choices at a declared retained budget while keeping the model, teacher, scaffold, task split, verifier, randomization law, and cost coordinates visible. The selective-refinement study supplies the comparison pattern; the typed interface, receipts, and estimators below are FTIP adaptations rather than source results [dang2026selecting, Sections 6-7; Tables 4-5, 10].

    The route separates the experiment interface (Definition 1), its receipt-derived quantities (Definition 2), and a finite paired calculation (Example 3). No result is claimed until an implementation supplies the declared receipts.

    Definition 1. Finite trace-selection experiment [ftip-00P8]

      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.

      Definition 2. Receipt metrics and paired contrasts [ftip-00P9]

        The source compares retained-horizon choices under declared task and evaluation boundaries [dang2026selecting, Sections 6-7; Tables 4-5, 10]. Fix an arm \(a\in \mathfrak A\) from Definition 1 and a positive run count \(N_a\). Each receipt \(R_{a,i}\) exposes a finite event sequence \((e^{\rm term},e^{\rm ev},e^{\rm pass},e^{\rm fail},e^{\rm rec}, n^{\rm prod})_{t=0}^{H_a}\), a task label \(q_{a,i}\), a strategy label \(s_{a,i}\), a measurable task-value score \(u_{a,i}(t)\), a declared saturation threshold \(u_a^{\rm sat}\), and a typed held-out outcome \(Y_{a,i}\in \mathcal Y_a\cup \{\bot \}\), final verifier outcome \(v_{a,i}\), and complete-admission indicator \(A_{a,i}\). Define \(A_{a,i}:=\mathbf 1[q_{a,i}\in Q_{\rm hold,a}\land v_{a,i}=1 \land Y_{a,i}\in \mathcal Y_a]\); when \(A_{a,i}=0\), set \(Y_{a,i}:=\bot \). The receipt contract emits a terminal event by \(H_a\); an execution that would not terminate naturally receives a timeout terminal event at \(H_a\) and \(A_{a,i}=0\). Put \(\overline {\mathbb N}:=\mathbb N\cup \{+\infty \}\) and \(\inf \varnothing :=+\infty \).

        \[ \tau ^{\rm end}_{a,i}:=\inf \{t:e^{\rm term}_{a,i}(t)=1\},\quad \tau ^{\rm ev}_{a,i}:=\inf \{t:e^{\rm ev}_{a,i}(t)=1\},\quad \tau ^{\rm pass}_{a,i}:=\inf \{t:e^{\rm pass}_{a,i}(t)=1\}, \]\[ \tau ^{\rm fail}_{a,i}:=\inf \{t:e^{\rm fail}_{a,i}(t)=1\},\quad \tau ^{\rm rec}_{a,i}:=\inf \{t:e^{\rm rec}_{a,i}(t)=1\},\quad \tau ^{\rm sat}_{a,i}:=\inf \{t:u_{a,i}(t)\geq u_a^{\rm sat}\}. \]

        Define the receipt predicates

        \[ \begin {aligned} I^{\rm pre}_{a,i}&:=\mathbf 1[\tau ^{\rm end}_{a,i}<\tau ^{\rm ev}_{a,i}],\\ I^{\rm rec}_{a,i}&:=\mathbf 1[\tau ^{\rm fail}_{a,i}<\tau ^{\rm rec}_{a,i}<\tau ^{\rm end}_{a,i}],\\ I^{\rm prod}_{a,i}&:=\mathbf 1[\tau ^{\rm ev}_{a,i}<\tau ^{\rm end}_{a,i} \land \tau ^{\rm pass}_{a,i}<\tau ^{\rm end}_{a,i} \land (\tau ^{\rm fail}_{a,i}\geq \tau ^{\rm end}_{a,i} \lor I^{\rm rec}_{a,i}=1)],\\ I^{\rm over}_{a,i}&:=\mathbf 1[\tau ^{\rm sat}_{a,i}<\tau ^{\rm end}_{a,i} \land \sum _{t=\tau ^{\rm sat}_{a,i}}^{\tau ^{\rm end}_{a,i}-1} n^{\rm prod}_{a,i}(t)=0]. \end {aligned} \]

        Here \(n^{\rm prod}_{a,i}(t)\) is a declared productive-novelty indicator in the receipt, and \(I^{\rm rec}\) is zero when no failure precedes recovery. The five run rates are functions of the receipts, with the declared denominator \(N_a\):

        \[ (\widehat p_a^{\rm pre},\widehat p_a^{\rm prod},\widehat p_a^{\rm over}, \widehat p_a^{\rm rec},\widehat p_a^{\rm pass}) :=\frac 1{N_a}\sum _{i=1}^{N_a} (I^{\rm pre}_{a,i},I^{\rm prod}_{a,i},I^{\rm over}_{a,i}, I^{\rm rec}_{a,i},\mathbf 1[\tau ^{\rm pass}_{a,i}<\tau ^{\rm end}_{a,i}]). \]

        For the finite held-out set, task and strategy coverage are

        \[ \widehat C^{\rm task}_a:= \frac {|\{q\in Q_{\rm hold,a}:\exists i,\ q_{a,i}=q,\ A_{a,i}=1\}|} {|Q_{\rm hold,a}|},\qquad \widehat C^{\rm strat}_a:= \frac {|\{s\in \mathfrak S_a:\exists i,\ s_{a,i}=s,\ A_{a,i}=1\}|} {|\mathfrak S_a|}, \]

        where \(\mathfrak S_a\) is a declared nonempty strategy-label set. Every receipt reports both positive denominators and the admission rule.

        For two paired arms \(a\) and \(a'\) that differ in one declared factor, let \(N:=\min (N_a,N_{a'})\). Define the common admitted index set \(J_{a,a'}:=\{i\leq N:A_{a,i}=A_{a',i}=1\}\) and \(N_{\rm pair}:=|J_{a,a'}|\). For \(i\in J_{a,a'}\), let \(Y_{a,i}\) and \(Y_{a',i}\) be their admitted held-out outcomes under the shared pairing law \(\Lambda _{a,a'}\), so \(q_{a,i}=q_{a',i}\). Compare their declared scalarizations \(g_a(Y_{a,i})\) and \(g_{a'}(Y_{a',i})\). When \(N_{\rm pair}\geq 2\), the primary finite contrast and its paired sample variance are

        \[ \widehat \Delta _{a,a'}:= \frac 1{N_{\rm pair}}\sum _{i\in J_{a,a'}} \bigl (g_a(Y_{a,i})-g_{a'}(Y_{a',i})\bigr ),\qquad \widehat V_{a,a'}:= \frac 1{N_{\rm pair}-1}\sum _{i\in J_{a,a'}} \bigl ((g_a(Y_{a,i})-g_{a'}(Y_{a',i}))-\widehat \Delta _{a,a'}\bigr )^2. \]

        When \(N_{\rm pair}=1\), report the single paired contrast but set \(\widehat V_{a,a'}:=\bot \); when \(N_{\rm pair}=0\), the paired contrast is undefined and the missingness is reported. These are finite estimators under the declared arm, split, admission rule, and coupling; they are not a universal selector law.

        Example 3. A paired trace-selection calculation [ftip-00PA]

          The selective-refinement comparison motivates contrasting repeatability and coverage under a fixed retained budget [dang2026selecting, Sections 6-7; Tables 4-5, 10]. Consider two arms from Definition 1 with the same P0 boundary, model, task split, verifier, budget, and paired assignment law. They differ only in the selector: \(a\) retains the highest teacher-forced scores and \(a'\) retains a coverage-stratified subset. Both have \(Q_{\rm hold}=\{q_1,q_2\}\) and \(\mathfrak S=\{s_1,s_2\}\). The paired assignment law gives the same held-out task at indices 1 and 2; arm \(a'\) has one additional admitted coverage run at index 3. Take \(g_a=g_{a'}=\operatorname {id}_{\{0,1\}}\). The receipts are

          \[ \begin {array}{c|cc|ccc} &q_{a,i}&s_{a,i}&A_{a,i}&I^{\rm prod}_{a,i}&Y_{a,i}\\\hline i=1&q_1&s_1&1&1&1\\ i=2&q_1&s_1&1&1&0 \end {array} \qquad \begin {array}{c|cc|ccc} &q_{a',i}&s_{a',i}&A_{a',i}&I^{\rm prod}_{a',i}&Y_{a',i}\\\hline i=1&q_1&s_1&1&1&1\\ i=2&q_1&s_1&1&1&1\\ i=3&q_2&s_2&1&1&1 \end {array} \]

          The first two rows are the common paired indices, so \(N_a=2\), \(N_{a'}=3\), and \(N_{\rm pair}=2\). Both arms have \(\widehat p^{\rm prod}=1\); the third row is included in arm \(a'\)'s coverage and run-rate denominators but not in the paired contrast. Thus \(\widehat C^{\rm task}_a=\widehat C^{\rm strat}_a=\tfrac 12\) and \(\widehat C^{\rm task}_{a'}=\widehat C^{\rm strat}_{a'}=1\), while \(\widehat \Delta _{a,a'}=-\tfrac 12\). The calculation shows why a repeatability rate alone cannot identify coverage: the two selectors have the same productive rate but different admitted task and strategy support. This is a finite FTIP construction using the typed receipt and pairing definitions, not a source result.

          References

            Reference. Selecting Long-Horizon Trajectories for Reliable and Efficient Terminal-Agent Training [dang2026selecting]

            @misc{dang2026selecting,
  title = {Selecting Long-Horizon Trajectories for Reliable and Efficient Terminal-Agent Training},
  author = {Dang, Cuong and Just, Hoang Anh and Jia, Ruoxi},
  year = {2026},
  eprint = {2610.05831},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2610.05831v1}
}

            Context

              Trace-quality intervention [ftip-00P4]

                Long-horizon training needs two linked questions: which events must a trace preserve, and how can a selector be tested without confusing repeatability with coverage? The first question is answered by the trace schema and behavior vocabulary; the second is answered by a fixed-budget protocol.

                The trace schema defines the record and its productive-persistence distinctions. The fixed-budget protocol defines the comparison arms, state interventions, metrics, and future-research gate.

                Trace quality and productive persistence [ftip-00P2]

                  FTIP asks which parts of a long-horizon trace remain useful to a later decision. The source horizon and selective-refinement observations are finite conditional evidence, while the trace record, persistence predicates, and build-repair example below make the retained events and state boundary explicit [dang2026selecting, Sections 3-7].

                  A useful horizon preserves the declared decision, evidence, verification, and recovery events while separating repeatability from task and strategy coverage. The fixed-budget protocol in § [ftip-00P3] supplies the finite selection, receipt, and contrast definitions needed to test that distinction.

                  Remark. Source horizon and selection hypothesis [ftip-00PB]

                    The direct observation in [dang2026selecting, Abstract; Sections 3-5 and Tables 1-4] compares 4K, 8K, 12K, and 16K supervision horizons for terminal-agent SFT. In its reported Terminal-Bench v1.0 setting, 12K reaches more tasks than 16K with about thirty percent less training time. The shorter setting under-persisted, the longest setting over-persisted, and the intermediate setting produced the best reported balance. This is a finite terminal-agent observation under one model, teacher corpus, scaffold, and benchmark family; it does not establish a universal horizon, long-term memory, or persistent identity.

                    The paper's bias-complexity account gives the FTIP hypothesis [dang2026selecting, Sections 5.2 and 6-7; Tables 4-5, 10]. Truncation can increase temporal-supervision bias by removing later decisions, while a longer continuation increases the policy complexity and finite-sample burden. The useful horizon is therefore conditional on the task law, teacher policy, model capacity, verifier, and retained state.

                    Selective refinement makes the data intervention explicit [dang2026selecting, Sections 6-7; Tables 4-5, 10]. A warm-start model is trained on a shorter horizon, continuation segments are scored by teacher-forced likelihood, and a fixed fraction is retained for longer-horizon refinement. The score measures compatibility with the warm-start policy, not intrinsic truth. High-likelihood selection can improve repeatability; the FTIP protocol tests whether low-likelihood or random selection preserves breadth, rare strategies, and recovery behavior.

                    A run is premature when it terminates before the declared evidence or recovery condition, productive when it continues through bounded evidence gathering, verification, and recovery, and over-persistent when additional work repeats or explores after task-relevant value has saturated. Record coverage loss separately: a selector can improve repeatability while deleting hard tasks or unusual recovery paths. These terms describe observable behavior; they are not claims about an agent's memory or inner objective.

                    Definition. Trace record and state boundary [ftip-00P5]

                      A long-horizon training trace should preserve the behavior that a later agent must learn: its decisions, evidence, verification, recovery, and the state boundary visible to the continuation. Fix event domains \(\mathcal O_{\rm evt}\), \(\mathcal A_{\rm evt}\), \(\mathcal Y_{\rm evt}\), \(\mathcal E_{\rm evt}\), and \(\mathcal V_{\rm evt}\), together with a termination domain \(\mathcal T_{\rm evt}\) and a boundary domain \(\mathcal S_{\rm boundary}\). The horizon comparison and selective-refinement intervention in [dang2026selecting, Sections 3-7] motivate this adaptation; the typed record below is an FTIP protocol proposal.

                      For \(H\in \mathbb N\), a trace record is

                      \[ T=(o_{0:H},a_{0:H},y_{0:H},e_{0:H},v_{0:H},\tau ,\sigma ,\kappa ) \in \mathcal O_{\rm evt}^{H+1}\times \mathcal A_{\rm evt}^{H+1} \times \mathcal Y_{\rm evt}^{H+1}\times \mathcal E_{\rm evt}^{H+1} \times \mathcal V_{\rm evt}^{H+1}\times \mathcal T_{\rm evt} \times \mathcal S_{\rm boundary}\times \mathbb N. \]

                      The components \(o\), \(a\), and \(y\) are observation, action, and outcome events; \(e\) records evidence or an environment-state reference; \(v\) records verification or recovery; \(\tau \) records termination; \(\sigma \) records the state boundary; and \(\kappa \) is token length. The horizon \(H\) and token length \(\kappa \) are separate coordinates. A task may use a declared subtype of each event domain, but it must preserve the coordinate meaning.

                      The record is a training datum only together with its declared boundary \(\sigma \): a continuation may access exactly the state coordinates allowed by that boundary. The record therefore supports a later selector or run kernel without treating token count as a proxy for the events that make continuation useful.

                      This is a protocol definition rather than a formal theorem; the event domains and transition semantics must be instantiated by the experiment that uses the record.

                      Definition. Persistence classes of a retained trace [ftip-00P6]

                        Fix a trace record \(T\) from Definition [ftip-00P5] and a declared receipt interface with event indicators \(e_{\rm term}(t)\), \(e_{\rm ev}(t)\), \(e_{\rm pass}(t)\), \(e_{\rm fail}(t)\), \(e_{\rm rec}(t)\) and a productive-novelty indicator \(n_{\rm prod}(t)\) for \(0\leq t\leq H\). Let \(u(t)\) be the declared task-value score and \(u^{\rm sat}\) its saturation threshold. The source's reported horizon tradeoff and selective refinement [dang2026selecting, Sections 5.2 and 6-7; Tables 4-5, 10] motivate these observable classes, which are an FTIP proposal. Write

                        \[ \tau _{\rm end}:=\inf \{t:e_{\rm term}(t)=1\},\quad \tau _{\rm ev}:=\inf \{t:e_{\rm ev}(t)=1\},\quad \tau _{\rm pass}:=\inf \{t:e_{\rm pass}(t)=1\}, \]\[ \tau _{\rm fail}:=\inf \{t:e_{\rm fail}(t)=1\},\quad \tau _{\rm rec}:=\inf \{t:e_{\rm rec}(t)=1\},\quad \tau _{\rm sat}:=\inf \{t:u(t)\geq u^{\rm sat}\}, \]

                        with \(\inf \varnothing :=+\infty \). The receipt declares all indicators and the score as functions of the same run, so the following classes are replayable predicates rather than impressions about an agent's inner state.

                        \[ \operatorname {Prem}(T):=\mathbf 1[\tau _{\rm end}<\tau _{\rm ev}\lor (\tau _{\rm fail}<\tau _{\rm end}\land \tau _{\rm rec}\geq \tau _{\rm end})], \]\[ \operatorname {Prod}(T):=\mathbf 1[\tau _{\rm ev}<\tau _{\rm end}\land \tau _{\rm pass}<\tau _{\rm end}\land (\tau _{\rm fail}\geq \tau _{\rm end}\lor \tau _{\rm fail}<\tau _{\rm rec}<\tau _{\rm end})], \]\[ \operatorname {Over}(T):=\mathbf 1[\tau _{\rm sat}<\tau _{\rm end}\land \sum _{t=\tau _{\rm sat}}^{\tau _{\rm end}-1}n_{\rm prod}(t)=0]. \]

                        A productive trace reaches evidence and a final verifier pass, and any failure before termination is followed by recovery. An over-persistent trace continues after saturation without another declared productive event. The experiment may refine \(n_{\rm prod}\) for a task family, but it must declare that predicate before comparing selectors.

                        Example. A retained build-repair trace [ftip-00P7]

                          The horizon and selective-refinement observations in [dang2026selecting, Sections 3-7] motivate the following finite classification. Consider a run whose task is to repair a failing build. The retained record contains the failing observation, the source edit, a test execution, and a final verifier pass. With the event interface of Definition [ftip-00P6], the test and verification steps contribute to \(e_{\rm ev}\), \(e_{\rm pass}\), and \(n_{\rm prod}\), so the record can satisfy \(\operatorname {Prod}(T)\).

                          If the test event is removed from the retained record, the same token budget can fail the productive predicate because the evidence chain is incomplete. If identical shell retries continue after \(\tau _{\rm sat}\) with no new productive event, \(\operatorname {Over}(T)\) can hold. This is a finite classification example; it does not claim that every short trace is better or that a model has an inner persistence objective.

                          Fixed-budget trace-selection protocol [ftip-00P3]
                          ✍️source

                            The trace-selection intervention is a finite evaluation proposal. It compares horizon and selector choices at a declared retained budget while keeping the model, teacher, scaffold, task split, verifier, randomization law, and cost coordinates visible. The selective-refinement study supplies the comparison pattern; the typed interface, receipts, and estimators below are FTIP adaptations rather than source results [dang2026selecting, Sections 6-7; Tables 4-5, 10].

                            The route separates the experiment interface (Definition [ftip-00P8]), its receipt-derived quantities (Definition [ftip-00P9]), and a finite paired calculation (Example [ftip-00PA]). No result is claimed until an implementation supplies the declared receipts.

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

                              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.

                              Definition. Receipt metrics and paired contrasts [ftip-00P9]

                                The source compares retained-horizon choices under declared task and evaluation boundaries [dang2026selecting, Sections 6-7; Tables 4-5, 10]. Fix an arm \(a\in \mathfrak A\) from Definition [ftip-00P8] and a positive run count \(N_a\). Each receipt \(R_{a,i}\) exposes a finite event sequence \((e^{\rm term},e^{\rm ev},e^{\rm pass},e^{\rm fail},e^{\rm rec}, n^{\rm prod})_{t=0}^{H_a}\), a task label \(q_{a,i}\), a strategy label \(s_{a,i}\), a measurable task-value score \(u_{a,i}(t)\), a declared saturation threshold \(u_a^{\rm sat}\), and a typed held-out outcome \(Y_{a,i}\in \mathcal Y_a\cup \{\bot \}\), final verifier outcome \(v_{a,i}\), and complete-admission indicator \(A_{a,i}\). Define \(A_{a,i}:=\mathbf 1[q_{a,i}\in Q_{\rm hold,a}\land v_{a,i}=1 \land Y_{a,i}\in \mathcal Y_a]\); when \(A_{a,i}=0\), set \(Y_{a,i}:=\bot \). The receipt contract emits a terminal event by \(H_a\); an execution that would not terminate naturally receives a timeout terminal event at \(H_a\) and \(A_{a,i}=0\). Put \(\overline {\mathbb N}:=\mathbb N\cup \{+\infty \}\) and \(\inf \varnothing :=+\infty \).

                                \[ \tau ^{\rm end}_{a,i}:=\inf \{t:e^{\rm term}_{a,i}(t)=1\},\quad \tau ^{\rm ev}_{a,i}:=\inf \{t:e^{\rm ev}_{a,i}(t)=1\},\quad \tau ^{\rm pass}_{a,i}:=\inf \{t:e^{\rm pass}_{a,i}(t)=1\}, \]\[ \tau ^{\rm fail}_{a,i}:=\inf \{t:e^{\rm fail}_{a,i}(t)=1\},\quad \tau ^{\rm rec}_{a,i}:=\inf \{t:e^{\rm rec}_{a,i}(t)=1\},\quad \tau ^{\rm sat}_{a,i}:=\inf \{t:u_{a,i}(t)\geq u_a^{\rm sat}\}. \]

                                Define the receipt predicates

                                \[ \begin {aligned} I^{\rm pre}_{a,i}&:=\mathbf 1[\tau ^{\rm end}_{a,i}<\tau ^{\rm ev}_{a,i}],\\ I^{\rm rec}_{a,i}&:=\mathbf 1[\tau ^{\rm fail}_{a,i}<\tau ^{\rm rec}_{a,i}<\tau ^{\rm end}_{a,i}],\\ I^{\rm prod}_{a,i}&:=\mathbf 1[\tau ^{\rm ev}_{a,i}<\tau ^{\rm end}_{a,i} \land \tau ^{\rm pass}_{a,i}<\tau ^{\rm end}_{a,i} \land (\tau ^{\rm fail}_{a,i}\geq \tau ^{\rm end}_{a,i} \lor I^{\rm rec}_{a,i}=1)],\\ I^{\rm over}_{a,i}&:=\mathbf 1[\tau ^{\rm sat}_{a,i}<\tau ^{\rm end}_{a,i} \land \sum _{t=\tau ^{\rm sat}_{a,i}}^{\tau ^{\rm end}_{a,i}-1} n^{\rm prod}_{a,i}(t)=0]. \end {aligned} \]

                                Here \(n^{\rm prod}_{a,i}(t)\) is a declared productive-novelty indicator in the receipt, and \(I^{\rm rec}\) is zero when no failure precedes recovery. The five run rates are functions of the receipts, with the declared denominator \(N_a\):

                                \[ (\widehat p_a^{\rm pre},\widehat p_a^{\rm prod},\widehat p_a^{\rm over}, \widehat p_a^{\rm rec},\widehat p_a^{\rm pass}) :=\frac 1{N_a}\sum _{i=1}^{N_a} (I^{\rm pre}_{a,i},I^{\rm prod}_{a,i},I^{\rm over}_{a,i}, I^{\rm rec}_{a,i},\mathbf 1[\tau ^{\rm pass}_{a,i}<\tau ^{\rm end}_{a,i}]). \]

                                For the finite held-out set, task and strategy coverage are

                                \[ \widehat C^{\rm task}_a:= \frac {|\{q\in Q_{\rm hold,a}:\exists i,\ q_{a,i}=q,\ A_{a,i}=1\}|} {|Q_{\rm hold,a}|},\qquad \widehat C^{\rm strat}_a:= \frac {|\{s\in \mathfrak S_a:\exists i,\ s_{a,i}=s,\ A_{a,i}=1\}|} {|\mathfrak S_a|}, \]

                                where \(\mathfrak S_a\) is a declared nonempty strategy-label set. Every receipt reports both positive denominators and the admission rule.

                                For two paired arms \(a\) and \(a'\) that differ in one declared factor, let \(N:=\min (N_a,N_{a'})\). Define the common admitted index set \(J_{a,a'}:=\{i\leq N:A_{a,i}=A_{a',i}=1\}\) and \(N_{\rm pair}:=|J_{a,a'}|\). For \(i\in J_{a,a'}\), let \(Y_{a,i}\) and \(Y_{a',i}\) be their admitted held-out outcomes under the shared pairing law \(\Lambda _{a,a'}\), so \(q_{a,i}=q_{a',i}\). Compare their declared scalarizations \(g_a(Y_{a,i})\) and \(g_{a'}(Y_{a',i})\). When \(N_{\rm pair}\geq 2\), the primary finite contrast and its paired sample variance are

                                \[ \widehat \Delta _{a,a'}:= \frac 1{N_{\rm pair}}\sum _{i\in J_{a,a'}} \bigl (g_a(Y_{a,i})-g_{a'}(Y_{a',i})\bigr ),\qquad \widehat V_{a,a'}:= \frac 1{N_{\rm pair}-1}\sum _{i\in J_{a,a'}} \bigl ((g_a(Y_{a,i})-g_{a'}(Y_{a',i}))-\widehat \Delta _{a,a'}\bigr )^2. \]

                                When \(N_{\rm pair}=1\), report the single paired contrast but set \(\widehat V_{a,a'}:=\bot \); when \(N_{\rm pair}=0\), the paired contrast is undefined and the missingness is reported. These are finite estimators under the declared arm, split, admission rule, and coupling; they are not a universal selector law.

                                Example. A paired trace-selection calculation [ftip-00PA]

                                  The selective-refinement comparison motivates contrasting repeatability and coverage under a fixed retained budget [dang2026selecting, Sections 6-7; Tables 4-5, 10]. Consider two arms from Definition [ftip-00P8] with the same P0 boundary, model, task split, verifier, budget, and paired assignment law. They differ only in the selector: \(a\) retains the highest teacher-forced scores and \(a'\) retains a coverage-stratified subset. Both have \(Q_{\rm hold}=\{q_1,q_2\}\) and \(\mathfrak S=\{s_1,s_2\}\). The paired assignment law gives the same held-out task at indices 1 and 2; arm \(a'\) has one additional admitted coverage run at index 3. Take \(g_a=g_{a'}=\operatorname {id}_{\{0,1\}}\). The receipts are

                                  \[ \begin {array}{c|cc|ccc} &q_{a,i}&s_{a,i}&A_{a,i}&I^{\rm prod}_{a,i}&Y_{a,i}\\\hline i=1&q_1&s_1&1&1&1\\ i=2&q_1&s_1&1&1&0 \end {array} \qquad \begin {array}{c|cc|ccc} &q_{a',i}&s_{a',i}&A_{a',i}&I^{\rm prod}_{a',i}&Y_{a',i}\\\hline i=1&q_1&s_1&1&1&1\\ i=2&q_1&s_1&1&1&1\\ i=3&q_2&s_2&1&1&1 \end {array} \]

                                  The first two rows are the common paired indices, so \(N_a=2\), \(N_{a'}=3\), and \(N_{\rm pair}=2\). Both arms have \(\widehat p^{\rm prod}=1\); the third row is included in arm \(a'\)'s coverage and run-rate denominators but not in the paired contrast. Thus \(\widehat C^{\rm task}_a=\widehat C^{\rm strat}_a=\tfrac 12\) and \(\widehat C^{\rm task}_{a'}=\widehat C^{\rm strat}_{a'}=1\), while \(\widehat \Delta _{a,a'}=-\tfrac 12\). The calculation shows why a repeatability rate alone cannot identify coverage: the two selectors have the same productive rate but different admitted task and strategy support. This is a finite FTIP construction using the typed receipt and pairing definitions, not a source result.

                                  With the trace schema and the fixed-budget protocol now in scope, the FTIP boundary is operational: an admitted trace must preserve the declared decision, evidence, verification, and recovery events, and every selector comparison must report the finite run rates, held-out task and strategy coverage, and charged selection/storage/restart costs defined in § [ftip-00P3]. A result may claim a selection benefit only when its immutable arm, split, seed, and randomization receipt supports that comparison.

                                  Backlinks

                                    Trace quality and productive persistence [ftip-00P2]

                                      FTIP asks which parts of a long-horizon trace remain useful to a later decision. The source horizon and selective-refinement observations are finite conditional evidence, while the trace record, persistence predicates, and build-repair example below make the retained events and state boundary explicit [dang2026selecting, Sections 3-7].

                                      A useful horizon preserves the declared decision, evidence, verification, and recovery events while separating repeatability from task and strategy coverage. The fixed-budget protocol in § [ftip-00P3] supplies the finite selection, receipt, and contrast definitions needed to test that distinction.

                                      Remark. Source horizon and selection hypothesis [ftip-00PB]

                                        The direct observation in [dang2026selecting, Abstract; Sections 3-5 and Tables 1-4] compares 4K, 8K, 12K, and 16K supervision horizons for terminal-agent SFT. In its reported Terminal-Bench v1.0 setting, 12K reaches more tasks than 16K with about thirty percent less training time. The shorter setting under-persisted, the longest setting over-persisted, and the intermediate setting produced the best reported balance. This is a finite terminal-agent observation under one model, teacher corpus, scaffold, and benchmark family; it does not establish a universal horizon, long-term memory, or persistent identity.

                                        The paper's bias-complexity account gives the FTIP hypothesis [dang2026selecting, Sections 5.2 and 6-7; Tables 4-5, 10]. Truncation can increase temporal-supervision bias by removing later decisions, while a longer continuation increases the policy complexity and finite-sample burden. The useful horizon is therefore conditional on the task law, teacher policy, model capacity, verifier, and retained state.

                                        Selective refinement makes the data intervention explicit [dang2026selecting, Sections 6-7; Tables 4-5, 10]. A warm-start model is trained on a shorter horizon, continuation segments are scored by teacher-forced likelihood, and a fixed fraction is retained for longer-horizon refinement. The score measures compatibility with the warm-start policy, not intrinsic truth. High-likelihood selection can improve repeatability; the FTIP protocol tests whether low-likelihood or random selection preserves breadth, rare strategies, and recovery behavior.

                                        A run is premature when it terminates before the declared evidence or recovery condition, productive when it continues through bounded evidence gathering, verification, and recovery, and over-persistent when additional work repeats or explores after task-relevant value has saturated. Record coverage loss separately: a selector can improve repeatability while deleting hard tasks or unusual recovery paths. These terms describe observable behavior; they are not claims about an agent's memory or inner objective.

                                        Definition. Trace record and state boundary [ftip-00P5]

                                          A long-horizon training trace should preserve the behavior that a later agent must learn: its decisions, evidence, verification, recovery, and the state boundary visible to the continuation. Fix event domains \(\mathcal O_{\rm evt}\), \(\mathcal A_{\rm evt}\), \(\mathcal Y_{\rm evt}\), \(\mathcal E_{\rm evt}\), and \(\mathcal V_{\rm evt}\), together with a termination domain \(\mathcal T_{\rm evt}\) and a boundary domain \(\mathcal S_{\rm boundary}\). The horizon comparison and selective-refinement intervention in [dang2026selecting, Sections 3-7] motivate this adaptation; the typed record below is an FTIP protocol proposal.

                                          For \(H\in \mathbb N\), a trace record is

                                          \[ T=(o_{0:H},a_{0:H},y_{0:H},e_{0:H},v_{0:H},\tau ,\sigma ,\kappa ) \in \mathcal O_{\rm evt}^{H+1}\times \mathcal A_{\rm evt}^{H+1} \times \mathcal Y_{\rm evt}^{H+1}\times \mathcal E_{\rm evt}^{H+1} \times \mathcal V_{\rm evt}^{H+1}\times \mathcal T_{\rm evt} \times \mathcal S_{\rm boundary}\times \mathbb N. \]

                                          The components \(o\), \(a\), and \(y\) are observation, action, and outcome events; \(e\) records evidence or an environment-state reference; \(v\) records verification or recovery; \(\tau \) records termination; \(\sigma \) records the state boundary; and \(\kappa \) is token length. The horizon \(H\) and token length \(\kappa \) are separate coordinates. A task may use a declared subtype of each event domain, but it must preserve the coordinate meaning.

                                          The record is a training datum only together with its declared boundary \(\sigma \): a continuation may access exactly the state coordinates allowed by that boundary. The record therefore supports a later selector or run kernel without treating token count as a proxy for the events that make continuation useful.

                                          This is a protocol definition rather than a formal theorem; the event domains and transition semantics must be instantiated by the experiment that uses the record.

                                          Definition. Persistence classes of a retained trace [ftip-00P6]

                                            Fix a trace record \(T\) from Definition [ftip-00P5] and a declared receipt interface with event indicators \(e_{\rm term}(t)\), \(e_{\rm ev}(t)\), \(e_{\rm pass}(t)\), \(e_{\rm fail}(t)\), \(e_{\rm rec}(t)\) and a productive-novelty indicator \(n_{\rm prod}(t)\) for \(0\leq t\leq H\). Let \(u(t)\) be the declared task-value score and \(u^{\rm sat}\) its saturation threshold. The source's reported horizon tradeoff and selective refinement [dang2026selecting, Sections 5.2 and 6-7; Tables 4-5, 10] motivate these observable classes, which are an FTIP proposal. Write

                                            \[ \tau _{\rm end}:=\inf \{t:e_{\rm term}(t)=1\},\quad \tau _{\rm ev}:=\inf \{t:e_{\rm ev}(t)=1\},\quad \tau _{\rm pass}:=\inf \{t:e_{\rm pass}(t)=1\}, \]\[ \tau _{\rm fail}:=\inf \{t:e_{\rm fail}(t)=1\},\quad \tau _{\rm rec}:=\inf \{t:e_{\rm rec}(t)=1\},\quad \tau _{\rm sat}:=\inf \{t:u(t)\geq u^{\rm sat}\}, \]

                                            with \(\inf \varnothing :=+\infty \). The receipt declares all indicators and the score as functions of the same run, so the following classes are replayable predicates rather than impressions about an agent's inner state.

                                            \[ \operatorname {Prem}(T):=\mathbf 1[\tau _{\rm end}<\tau _{\rm ev}\lor (\tau _{\rm fail}<\tau _{\rm end}\land \tau _{\rm rec}\geq \tau _{\rm end})], \]\[ \operatorname {Prod}(T):=\mathbf 1[\tau _{\rm ev}<\tau _{\rm end}\land \tau _{\rm pass}<\tau _{\rm end}\land (\tau _{\rm fail}\geq \tau _{\rm end}\lor \tau _{\rm fail}<\tau _{\rm rec}<\tau _{\rm end})], \]\[ \operatorname {Over}(T):=\mathbf 1[\tau _{\rm sat}<\tau _{\rm end}\land \sum _{t=\tau _{\rm sat}}^{\tau _{\rm end}-1}n_{\rm prod}(t)=0]. \]

                                            A productive trace reaches evidence and a final verifier pass, and any failure before termination is followed by recovery. An over-persistent trace continues after saturation without another declared productive event. The experiment may refine \(n_{\rm prod}\) for a task family, but it must declare that predicate before comparing selectors.

                                            Example. A retained build-repair trace [ftip-00P7]

                                              The horizon and selective-refinement observations in [dang2026selecting, Sections 3-7] motivate the following finite classification. Consider a run whose task is to repair a failing build. The retained record contains the failing observation, the source edit, a test execution, and a final verifier pass. With the event interface of Definition [ftip-00P6], the test and verification steps contribute to \(e_{\rm ev}\), \(e_{\rm pass}\), and \(n_{\rm prod}\), so the record can satisfy \(\operatorname {Prod}(T)\).

                                              If the test event is removed from the retained record, the same token budget can fail the productive predicate because the evidence chain is incomplete. If identical shell retries continue after \(\tau _{\rm sat}\) with no new productive event, \(\operatorname {Over}(T)\) can hold. This is a finite classification example; it does not claim that every short trace is better or that a model has an inner persistence objective.

                                              Trace-quality intervention [ftip-00P4]

                                                Long-horizon training needs two linked questions: which events must a trace preserve, and how can a selector be tested without confusing repeatability with coverage? The first question is answered by the trace schema and behavior vocabulary; the second is answered by a fixed-budget protocol.

                                                The trace schema defines the record and its productive-persistence distinctions. The fixed-budget protocol defines the comparison arms, state interventions, metrics, and future-research gate.

                                                Trace quality and productive persistence [ftip-00P2]

                                                  FTIP asks which parts of a long-horizon trace remain useful to a later decision. The source horizon and selective-refinement observations are finite conditional evidence, while the trace record, persistence predicates, and build-repair example below make the retained events and state boundary explicit [dang2026selecting, Sections 3-7].

                                                  A useful horizon preserves the declared decision, evidence, verification, and recovery events while separating repeatability from task and strategy coverage. The fixed-budget protocol in § [ftip-00P3] supplies the finite selection, receipt, and contrast definitions needed to test that distinction.

                                                  Remark. Source horizon and selection hypothesis [ftip-00PB]

                                                    The direct observation in [dang2026selecting, Abstract; Sections 3-5 and Tables 1-4] compares 4K, 8K, 12K, and 16K supervision horizons for terminal-agent SFT. In its reported Terminal-Bench v1.0 setting, 12K reaches more tasks than 16K with about thirty percent less training time. The shorter setting under-persisted, the longest setting over-persisted, and the intermediate setting produced the best reported balance. This is a finite terminal-agent observation under one model, teacher corpus, scaffold, and benchmark family; it does not establish a universal horizon, long-term memory, or persistent identity.

                                                    The paper's bias-complexity account gives the FTIP hypothesis [dang2026selecting, Sections 5.2 and 6-7; Tables 4-5, 10]. Truncation can increase temporal-supervision bias by removing later decisions, while a longer continuation increases the policy complexity and finite-sample burden. The useful horizon is therefore conditional on the task law, teacher policy, model capacity, verifier, and retained state.

                                                    Selective refinement makes the data intervention explicit [dang2026selecting, Sections 6-7; Tables 4-5, 10]. A warm-start model is trained on a shorter horizon, continuation segments are scored by teacher-forced likelihood, and a fixed fraction is retained for longer-horizon refinement. The score measures compatibility with the warm-start policy, not intrinsic truth. High-likelihood selection can improve repeatability; the FTIP protocol tests whether low-likelihood or random selection preserves breadth, rare strategies, and recovery behavior.

                                                    A run is premature when it terminates before the declared evidence or recovery condition, productive when it continues through bounded evidence gathering, verification, and recovery, and over-persistent when additional work repeats or explores after task-relevant value has saturated. Record coverage loss separately: a selector can improve repeatability while deleting hard tasks or unusual recovery paths. These terms describe observable behavior; they are not claims about an agent's memory or inner objective.

                                                    Definition. Trace record and state boundary [ftip-00P5]

                                                      A long-horizon training trace should preserve the behavior that a later agent must learn: its decisions, evidence, verification, recovery, and the state boundary visible to the continuation. Fix event domains \(\mathcal O_{\rm evt}\), \(\mathcal A_{\rm evt}\), \(\mathcal Y_{\rm evt}\), \(\mathcal E_{\rm evt}\), and \(\mathcal V_{\rm evt}\), together with a termination domain \(\mathcal T_{\rm evt}\) and a boundary domain \(\mathcal S_{\rm boundary}\). The horizon comparison and selective-refinement intervention in [dang2026selecting, Sections 3-7] motivate this adaptation; the typed record below is an FTIP protocol proposal.

                                                      For \(H\in \mathbb N\), a trace record is

                                                      \[ T=(o_{0:H},a_{0:H},y_{0:H},e_{0:H},v_{0:H},\tau ,\sigma ,\kappa ) \in \mathcal O_{\rm evt}^{H+1}\times \mathcal A_{\rm evt}^{H+1} \times \mathcal Y_{\rm evt}^{H+1}\times \mathcal E_{\rm evt}^{H+1} \times \mathcal V_{\rm evt}^{H+1}\times \mathcal T_{\rm evt} \times \mathcal S_{\rm boundary}\times \mathbb N. \]

                                                      The components \(o\), \(a\), and \(y\) are observation, action, and outcome events; \(e\) records evidence or an environment-state reference; \(v\) records verification or recovery; \(\tau \) records termination; \(\sigma \) records the state boundary; and \(\kappa \) is token length. The horizon \(H\) and token length \(\kappa \) are separate coordinates. A task may use a declared subtype of each event domain, but it must preserve the coordinate meaning.

                                                      The record is a training datum only together with its declared boundary \(\sigma \): a continuation may access exactly the state coordinates allowed by that boundary. The record therefore supports a later selector or run kernel without treating token count as a proxy for the events that make continuation useful.

                                                      This is a protocol definition rather than a formal theorem; the event domains and transition semantics must be instantiated by the experiment that uses the record.

                                                      Definition. Persistence classes of a retained trace [ftip-00P6]

                                                        Fix a trace record \(T\) from Definition [ftip-00P5] and a declared receipt interface with event indicators \(e_{\rm term}(t)\), \(e_{\rm ev}(t)\), \(e_{\rm pass}(t)\), \(e_{\rm fail}(t)\), \(e_{\rm rec}(t)\) and a productive-novelty indicator \(n_{\rm prod}(t)\) for \(0\leq t\leq H\). Let \(u(t)\) be the declared task-value score and \(u^{\rm sat}\) its saturation threshold. The source's reported horizon tradeoff and selective refinement [dang2026selecting, Sections 5.2 and 6-7; Tables 4-5, 10] motivate these observable classes, which are an FTIP proposal. Write

                                                        \[ \tau _{\rm end}:=\inf \{t:e_{\rm term}(t)=1\},\quad \tau _{\rm ev}:=\inf \{t:e_{\rm ev}(t)=1\},\quad \tau _{\rm pass}:=\inf \{t:e_{\rm pass}(t)=1\}, \]\[ \tau _{\rm fail}:=\inf \{t:e_{\rm fail}(t)=1\},\quad \tau _{\rm rec}:=\inf \{t:e_{\rm rec}(t)=1\},\quad \tau _{\rm sat}:=\inf \{t:u(t)\geq u^{\rm sat}\}, \]

                                                        with \(\inf \varnothing :=+\infty \). The receipt declares all indicators and the score as functions of the same run, so the following classes are replayable predicates rather than impressions about an agent's inner state.

                                                        \[ \operatorname {Prem}(T):=\mathbf 1[\tau _{\rm end}<\tau _{\rm ev}\lor (\tau _{\rm fail}<\tau _{\rm end}\land \tau _{\rm rec}\geq \tau _{\rm end})], \]\[ \operatorname {Prod}(T):=\mathbf 1[\tau _{\rm ev}<\tau _{\rm end}\land \tau _{\rm pass}<\tau _{\rm end}\land (\tau _{\rm fail}\geq \tau _{\rm end}\lor \tau _{\rm fail}<\tau _{\rm rec}<\tau _{\rm end})], \]\[ \operatorname {Over}(T):=\mathbf 1[\tau _{\rm sat}<\tau _{\rm end}\land \sum _{t=\tau _{\rm sat}}^{\tau _{\rm end}-1}n_{\rm prod}(t)=0]. \]

                                                        A productive trace reaches evidence and a final verifier pass, and any failure before termination is followed by recovery. An over-persistent trace continues after saturation without another declared productive event. The experiment may refine \(n_{\rm prod}\) for a task family, but it must declare that predicate before comparing selectors.

                                                        Example. A retained build-repair trace [ftip-00P7]

                                                          The horizon and selective-refinement observations in [dang2026selecting, Sections 3-7] motivate the following finite classification. Consider a run whose task is to repair a failing build. The retained record contains the failing observation, the source edit, a test execution, and a final verifier pass. With the event interface of Definition [ftip-00P6], the test and verification steps contribute to \(e_{\rm ev}\), \(e_{\rm pass}\), and \(n_{\rm prod}\), so the record can satisfy \(\operatorname {Prod}(T)\).

                                                          If the test event is removed from the retained record, the same token budget can fail the productive predicate because the evidence chain is incomplete. If identical shell retries continue after \(\tau _{\rm sat}\) with no new productive event, \(\operatorname {Over}(T)\) can hold. This is a finite classification example; it does not claim that every short trace is better or that a model has an inner persistence objective.

                                                          Fixed-budget trace-selection protocol [ftip-00P3]
                                                          ✍️source

                                                            The trace-selection intervention is a finite evaluation proposal. It compares horizon and selector choices at a declared retained budget while keeping the model, teacher, scaffold, task split, verifier, randomization law, and cost coordinates visible. The selective-refinement study supplies the comparison pattern; the typed interface, receipts, and estimators below are FTIP adaptations rather than source results [dang2026selecting, Sections 6-7; Tables 4-5, 10].

                                                            The route separates the experiment interface (Definition [ftip-00P8]), its receipt-derived quantities (Definition [ftip-00P9]), and a finite paired calculation (Example [ftip-00PA]). No result is claimed until an implementation supplies the declared receipts.

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

                                                              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.

                                                              Definition. Receipt metrics and paired contrasts [ftip-00P9]

                                                                The source compares retained-horizon choices under declared task and evaluation boundaries [dang2026selecting, Sections 6-7; Tables 4-5, 10]. Fix an arm \(a\in \mathfrak A\) from Definition [ftip-00P8] and a positive run count \(N_a\). Each receipt \(R_{a,i}\) exposes a finite event sequence \((e^{\rm term},e^{\rm ev},e^{\rm pass},e^{\rm fail},e^{\rm rec}, n^{\rm prod})_{t=0}^{H_a}\), a task label \(q_{a,i}\), a strategy label \(s_{a,i}\), a measurable task-value score \(u_{a,i}(t)\), a declared saturation threshold \(u_a^{\rm sat}\), and a typed held-out outcome \(Y_{a,i}\in \mathcal Y_a\cup \{\bot \}\), final verifier outcome \(v_{a,i}\), and complete-admission indicator \(A_{a,i}\). Define \(A_{a,i}:=\mathbf 1[q_{a,i}\in Q_{\rm hold,a}\land v_{a,i}=1 \land Y_{a,i}\in \mathcal Y_a]\); when \(A_{a,i}=0\), set \(Y_{a,i}:=\bot \). The receipt contract emits a terminal event by \(H_a\); an execution that would not terminate naturally receives a timeout terminal event at \(H_a\) and \(A_{a,i}=0\). Put \(\overline {\mathbb N}:=\mathbb N\cup \{+\infty \}\) and \(\inf \varnothing :=+\infty \).

                                                                \[ \tau ^{\rm end}_{a,i}:=\inf \{t:e^{\rm term}_{a,i}(t)=1\},\quad \tau ^{\rm ev}_{a,i}:=\inf \{t:e^{\rm ev}_{a,i}(t)=1\},\quad \tau ^{\rm pass}_{a,i}:=\inf \{t:e^{\rm pass}_{a,i}(t)=1\}, \]\[ \tau ^{\rm fail}_{a,i}:=\inf \{t:e^{\rm fail}_{a,i}(t)=1\},\quad \tau ^{\rm rec}_{a,i}:=\inf \{t:e^{\rm rec}_{a,i}(t)=1\},\quad \tau ^{\rm sat}_{a,i}:=\inf \{t:u_{a,i}(t)\geq u_a^{\rm sat}\}. \]

                                                                Define the receipt predicates

                                                                \[ \begin {aligned} I^{\rm pre}_{a,i}&:=\mathbf 1[\tau ^{\rm end}_{a,i}<\tau ^{\rm ev}_{a,i}],\\ I^{\rm rec}_{a,i}&:=\mathbf 1[\tau ^{\rm fail}_{a,i}<\tau ^{\rm rec}_{a,i}<\tau ^{\rm end}_{a,i}],\\ I^{\rm prod}_{a,i}&:=\mathbf 1[\tau ^{\rm ev}_{a,i}<\tau ^{\rm end}_{a,i} \land \tau ^{\rm pass}_{a,i}<\tau ^{\rm end}_{a,i} \land (\tau ^{\rm fail}_{a,i}\geq \tau ^{\rm end}_{a,i} \lor I^{\rm rec}_{a,i}=1)],\\ I^{\rm over}_{a,i}&:=\mathbf 1[\tau ^{\rm sat}_{a,i}<\tau ^{\rm end}_{a,i} \land \sum _{t=\tau ^{\rm sat}_{a,i}}^{\tau ^{\rm end}_{a,i}-1} n^{\rm prod}_{a,i}(t)=0]. \end {aligned} \]

                                                                Here \(n^{\rm prod}_{a,i}(t)\) is a declared productive-novelty indicator in the receipt, and \(I^{\rm rec}\) is zero when no failure precedes recovery. The five run rates are functions of the receipts, with the declared denominator \(N_a\):

                                                                \[ (\widehat p_a^{\rm pre},\widehat p_a^{\rm prod},\widehat p_a^{\rm over}, \widehat p_a^{\rm rec},\widehat p_a^{\rm pass}) :=\frac 1{N_a}\sum _{i=1}^{N_a} (I^{\rm pre}_{a,i},I^{\rm prod}_{a,i},I^{\rm over}_{a,i}, I^{\rm rec}_{a,i},\mathbf 1[\tau ^{\rm pass}_{a,i}<\tau ^{\rm end}_{a,i}]). \]

                                                                For the finite held-out set, task and strategy coverage are

                                                                \[ \widehat C^{\rm task}_a:= \frac {|\{q\in Q_{\rm hold,a}:\exists i,\ q_{a,i}=q,\ A_{a,i}=1\}|} {|Q_{\rm hold,a}|},\qquad \widehat C^{\rm strat}_a:= \frac {|\{s\in \mathfrak S_a:\exists i,\ s_{a,i}=s,\ A_{a,i}=1\}|} {|\mathfrak S_a|}, \]

                                                                where \(\mathfrak S_a\) is a declared nonempty strategy-label set. Every receipt reports both positive denominators and the admission rule.

                                                                For two paired arms \(a\) and \(a'\) that differ in one declared factor, let \(N:=\min (N_a,N_{a'})\). Define the common admitted index set \(J_{a,a'}:=\{i\leq N:A_{a,i}=A_{a',i}=1\}\) and \(N_{\rm pair}:=|J_{a,a'}|\). For \(i\in J_{a,a'}\), let \(Y_{a,i}\) and \(Y_{a',i}\) be their admitted held-out outcomes under the shared pairing law \(\Lambda _{a,a'}\), so \(q_{a,i}=q_{a',i}\). Compare their declared scalarizations \(g_a(Y_{a,i})\) and \(g_{a'}(Y_{a',i})\). When \(N_{\rm pair}\geq 2\), the primary finite contrast and its paired sample variance are

                                                                \[ \widehat \Delta _{a,a'}:= \frac 1{N_{\rm pair}}\sum _{i\in J_{a,a'}} \bigl (g_a(Y_{a,i})-g_{a'}(Y_{a',i})\bigr ),\qquad \widehat V_{a,a'}:= \frac 1{N_{\rm pair}-1}\sum _{i\in J_{a,a'}} \bigl ((g_a(Y_{a,i})-g_{a'}(Y_{a',i}))-\widehat \Delta _{a,a'}\bigr )^2. \]

                                                                When \(N_{\rm pair}=1\), report the single paired contrast but set \(\widehat V_{a,a'}:=\bot \); when \(N_{\rm pair}=0\), the paired contrast is undefined and the missingness is reported. These are finite estimators under the declared arm, split, admission rule, and coupling; they are not a universal selector law.

                                                                Example. A paired trace-selection calculation [ftip-00PA]

                                                                  The selective-refinement comparison motivates contrasting repeatability and coverage under a fixed retained budget [dang2026selecting, Sections 6-7; Tables 4-5, 10]. Consider two arms from Definition [ftip-00P8] with the same P0 boundary, model, task split, verifier, budget, and paired assignment law. They differ only in the selector: \(a\) retains the highest teacher-forced scores and \(a'\) retains a coverage-stratified subset. Both have \(Q_{\rm hold}=\{q_1,q_2\}\) and \(\mathfrak S=\{s_1,s_2\}\). The paired assignment law gives the same held-out task at indices 1 and 2; arm \(a'\) has one additional admitted coverage run at index 3. Take \(g_a=g_{a'}=\operatorname {id}_{\{0,1\}}\). The receipts are

                                                                  \[ \begin {array}{c|cc|ccc} &q_{a,i}&s_{a,i}&A_{a,i}&I^{\rm prod}_{a,i}&Y_{a,i}\\\hline i=1&q_1&s_1&1&1&1\\ i=2&q_1&s_1&1&1&0 \end {array} \qquad \begin {array}{c|cc|ccc} &q_{a',i}&s_{a',i}&A_{a',i}&I^{\rm prod}_{a',i}&Y_{a',i}\\\hline i=1&q_1&s_1&1&1&1\\ i=2&q_1&s_1&1&1&1\\ i=3&q_2&s_2&1&1&1 \end {array} \]

                                                                  The first two rows are the common paired indices, so \(N_a=2\), \(N_{a'}=3\), and \(N_{\rm pair}=2\). Both arms have \(\widehat p^{\rm prod}=1\); the third row is included in arm \(a'\)'s coverage and run-rate denominators but not in the paired contrast. Thus \(\widehat C^{\rm task}_a=\widehat C^{\rm strat}_a=\tfrac 12\) and \(\widehat C^{\rm task}_{a'}=\widehat C^{\rm strat}_{a'}=1\), while \(\widehat \Delta _{a,a'}=-\tfrac 12\). The calculation shows why a repeatability rate alone cannot identify coverage: the two selectors have the same productive rate but different admitted task and strategy support. This is a finite FTIP construction using the typed receipt and pairing definitions, not a source result.

                                                                  With the trace schema and the fixed-budget protocol now in scope, the FTIP boundary is operational: an admitted trace must preserve the declared decision, evidence, verification, and recovery events, and every selector comparison must report the finite run rates, held-out task and strategy coverage, and charged selection/storage/restart costs defined in § [ftip-00P3]. A result may claim a selection benefit only when its immutable arm, split, seed, and randomization receipt supports that comparison.

                                                                  Related

                                                                    Example. A paired trace-selection calculation [ftip-00PA]

                                                                      The selective-refinement comparison motivates contrasting repeatability and coverage under a fixed retained budget [dang2026selecting, Sections 6-7; Tables 4-5, 10]. Consider two arms from Definition [ftip-00P8] with the same P0 boundary, model, task split, verifier, budget, and paired assignment law. They differ only in the selector: \(a\) retains the highest teacher-forced scores and \(a'\) retains a coverage-stratified subset. Both have \(Q_{\rm hold}=\{q_1,q_2\}\) and \(\mathfrak S=\{s_1,s_2\}\). The paired assignment law gives the same held-out task at indices 1 and 2; arm \(a'\) has one additional admitted coverage run at index 3. Take \(g_a=g_{a'}=\operatorname {id}_{\{0,1\}}\). The receipts are

                                                                      \[ \begin {array}{c|cc|ccc} &q_{a,i}&s_{a,i}&A_{a,i}&I^{\rm prod}_{a,i}&Y_{a,i}\\\hline i=1&q_1&s_1&1&1&1\\ i=2&q_1&s_1&1&1&0 \end {array} \qquad \begin {array}{c|cc|ccc} &q_{a',i}&s_{a',i}&A_{a',i}&I^{\rm prod}_{a',i}&Y_{a',i}\\\hline i=1&q_1&s_1&1&1&1\\ i=2&q_1&s_1&1&1&1\\ i=3&q_2&s_2&1&1&1 \end {array} \]

                                                                      The first two rows are the common paired indices, so \(N_a=2\), \(N_{a'}=3\), and \(N_{\rm pair}=2\). Both arms have \(\widehat p^{\rm prod}=1\); the third row is included in arm \(a'\)'s coverage and run-rate denominators but not in the paired contrast. Thus \(\widehat C^{\rm task}_a=\widehat C^{\rm strat}_a=\tfrac 12\) and \(\widehat C^{\rm task}_{a'}=\widehat C^{\rm strat}_{a'}=1\), while \(\widehat \Delta _{a,a'}=-\tfrac 12\). The calculation shows why a repeatability rate alone cannot identify coverage: the two selectors have the same productive rate but different admitted task and strategy support. This is a finite FTIP construction using the typed receipt and pairing definitions, not a source result.

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

                                                                        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.

                                                                        Definition. Receipt metrics and paired contrasts [ftip-00P9]

                                                                          The source compares retained-horizon choices under declared task and evaluation boundaries [dang2026selecting, Sections 6-7; Tables 4-5, 10]. Fix an arm \(a\in \mathfrak A\) from Definition [ftip-00P8] and a positive run count \(N_a\). Each receipt \(R_{a,i}\) exposes a finite event sequence \((e^{\rm term},e^{\rm ev},e^{\rm pass},e^{\rm fail},e^{\rm rec}, n^{\rm prod})_{t=0}^{H_a}\), a task label \(q_{a,i}\), a strategy label \(s_{a,i}\), a measurable task-value score \(u_{a,i}(t)\), a declared saturation threshold \(u_a^{\rm sat}\), and a typed held-out outcome \(Y_{a,i}\in \mathcal Y_a\cup \{\bot \}\), final verifier outcome \(v_{a,i}\), and complete-admission indicator \(A_{a,i}\). Define \(A_{a,i}:=\mathbf 1[q_{a,i}\in Q_{\rm hold,a}\land v_{a,i}=1 \land Y_{a,i}\in \mathcal Y_a]\); when \(A_{a,i}=0\), set \(Y_{a,i}:=\bot \). The receipt contract emits a terminal event by \(H_a\); an execution that would not terminate naturally receives a timeout terminal event at \(H_a\) and \(A_{a,i}=0\). Put \(\overline {\mathbb N}:=\mathbb N\cup \{+\infty \}\) and \(\inf \varnothing :=+\infty \).

                                                                          \[ \tau ^{\rm end}_{a,i}:=\inf \{t:e^{\rm term}_{a,i}(t)=1\},\quad \tau ^{\rm ev}_{a,i}:=\inf \{t:e^{\rm ev}_{a,i}(t)=1\},\quad \tau ^{\rm pass}_{a,i}:=\inf \{t:e^{\rm pass}_{a,i}(t)=1\}, \]\[ \tau ^{\rm fail}_{a,i}:=\inf \{t:e^{\rm fail}_{a,i}(t)=1\},\quad \tau ^{\rm rec}_{a,i}:=\inf \{t:e^{\rm rec}_{a,i}(t)=1\},\quad \tau ^{\rm sat}_{a,i}:=\inf \{t:u_{a,i}(t)\geq u_a^{\rm sat}\}. \]

                                                                          Define the receipt predicates

                                                                          \[ \begin {aligned} I^{\rm pre}_{a,i}&:=\mathbf 1[\tau ^{\rm end}_{a,i}<\tau ^{\rm ev}_{a,i}],\\ I^{\rm rec}_{a,i}&:=\mathbf 1[\tau ^{\rm fail}_{a,i}<\tau ^{\rm rec}_{a,i}<\tau ^{\rm end}_{a,i}],\\ I^{\rm prod}_{a,i}&:=\mathbf 1[\tau ^{\rm ev}_{a,i}<\tau ^{\rm end}_{a,i} \land \tau ^{\rm pass}_{a,i}<\tau ^{\rm end}_{a,i} \land (\tau ^{\rm fail}_{a,i}\geq \tau ^{\rm end}_{a,i} \lor I^{\rm rec}_{a,i}=1)],\\ I^{\rm over}_{a,i}&:=\mathbf 1[\tau ^{\rm sat}_{a,i}<\tau ^{\rm end}_{a,i} \land \sum _{t=\tau ^{\rm sat}_{a,i}}^{\tau ^{\rm end}_{a,i}-1} n^{\rm prod}_{a,i}(t)=0]. \end {aligned} \]

                                                                          Here \(n^{\rm prod}_{a,i}(t)\) is a declared productive-novelty indicator in the receipt, and \(I^{\rm rec}\) is zero when no failure precedes recovery. The five run rates are functions of the receipts, with the declared denominator \(N_a\):

                                                                          \[ (\widehat p_a^{\rm pre},\widehat p_a^{\rm prod},\widehat p_a^{\rm over}, \widehat p_a^{\rm rec},\widehat p_a^{\rm pass}) :=\frac 1{N_a}\sum _{i=1}^{N_a} (I^{\rm pre}_{a,i},I^{\rm prod}_{a,i},I^{\rm over}_{a,i}, I^{\rm rec}_{a,i},\mathbf 1[\tau ^{\rm pass}_{a,i}<\tau ^{\rm end}_{a,i}]). \]

                                                                          For the finite held-out set, task and strategy coverage are

                                                                          \[ \widehat C^{\rm task}_a:= \frac {|\{q\in Q_{\rm hold,a}:\exists i,\ q_{a,i}=q,\ A_{a,i}=1\}|} {|Q_{\rm hold,a}|},\qquad \widehat C^{\rm strat}_a:= \frac {|\{s\in \mathfrak S_a:\exists i,\ s_{a,i}=s,\ A_{a,i}=1\}|} {|\mathfrak S_a|}, \]

                                                                          where \(\mathfrak S_a\) is a declared nonempty strategy-label set. Every receipt reports both positive denominators and the admission rule.

                                                                          For two paired arms \(a\) and \(a'\) that differ in one declared factor, let \(N:=\min (N_a,N_{a'})\). Define the common admitted index set \(J_{a,a'}:=\{i\leq N:A_{a,i}=A_{a',i}=1\}\) and \(N_{\rm pair}:=|J_{a,a'}|\). For \(i\in J_{a,a'}\), let \(Y_{a,i}\) and \(Y_{a',i}\) be their admitted held-out outcomes under the shared pairing law \(\Lambda _{a,a'}\), so \(q_{a,i}=q_{a',i}\). Compare their declared scalarizations \(g_a(Y_{a,i})\) and \(g_{a'}(Y_{a',i})\). When \(N_{\rm pair}\geq 2\), the primary finite contrast and its paired sample variance are

                                                                          \[ \widehat \Delta _{a,a'}:= \frac 1{N_{\rm pair}}\sum _{i\in J_{a,a'}} \bigl (g_a(Y_{a,i})-g_{a'}(Y_{a',i})\bigr ),\qquad \widehat V_{a,a'}:= \frac 1{N_{\rm pair}-1}\sum _{i\in J_{a,a'}} \bigl ((g_a(Y_{a,i})-g_{a'}(Y_{a',i}))-\widehat \Delta _{a,a'}\bigr )^2. \]

                                                                          When \(N_{\rm pair}=1\), report the single paired contrast but set \(\widehat V_{a,a'}:=\bot \); when \(N_{\rm pair}=0\), the paired contrast is undefined and the missingness is reported. These are finite estimators under the declared arm, split, admission rule, and coupling; they are not a universal selector law.